Commit 2023-09-12 23:50 fc200859

View on Github →

chore: bump Std for #251 (#7126) Some minor renaming:

  • Sum.not_isLeft becomes Sum.bnot_isLeft
  • Sum.Not_isLeft becomes Sum.not_isLeft A few explicit arguments also became implicit.

Estimated changes

deleted theorem Sum.Lex.mono
deleted theorem Sum.Lex.mono_left
deleted theorem Sum.Lex.mono_right
deleted inductive Sum.Lex
deleted theorem Sum.LiftRel.mono
deleted theorem Sum.LiftRel.mono_left
deleted theorem Sum.LiftRel.mono_right
deleted inductive Sum.LiftRel
deleted theorem Sum.Not_isLeft
deleted theorem Sum.Not_isRight
deleted theorem Sum.comp_elim
deleted theorem Sum.elim_comp_inl
deleted theorem Sum.elim_comp_inl_inr
deleted theorem Sum.elim_comp_inr
deleted theorem Sum.elim_comp_map
deleted theorem Sum.elim_const_const
deleted theorem Sum.elim_inl
deleted theorem Sum.elim_inl_inr
deleted theorem Sum.elim_inr
deleted theorem Sum.elim_map
added theorem Sum.exists_sum
deleted theorem Sum.exists_sum_pi
deleted theorem Sum.forall_sum_pi
deleted def Sum.getLeft
deleted def Sum.getLeft?
deleted theorem Sum.getLeft?_eq_none_iff
deleted theorem Sum.getLeft?_eq_some_iff
deleted theorem Sum.getLeft?_inl
deleted theorem Sum.getLeft?_inr
deleted theorem Sum.getLeft?_map
deleted theorem Sum.getLeft?_swap
deleted theorem Sum.getLeft_eq_iff
deleted theorem Sum.getLeft_inl
deleted def Sum.getRight
deleted def Sum.getRight?
deleted theorem Sum.getRight?_eq_none_iff
deleted theorem Sum.getRight?_eq_some_iff
deleted theorem Sum.getRight?_inl
deleted theorem Sum.getRight?_inr
deleted theorem Sum.getRight?_map
deleted theorem Sum.getRight?_swap
deleted theorem Sum.getRight_eq_iff
deleted theorem Sum.getRight_inr
deleted theorem Sum.inl.inj_iff
deleted theorem Sum.inl_getLeft
deleted theorem Sum.inl_ne_inr
deleted theorem Sum.inr.inj_iff
deleted theorem Sum.inr_getRight
deleted theorem Sum.inr_ne_inl
deleted def Sum.isLeft
deleted theorem Sum.isLeft_eq_false
deleted theorem Sum.isLeft_iff
deleted theorem Sum.isLeft_inl
deleted theorem Sum.isLeft_inr
deleted theorem Sum.isLeft_map
deleted theorem Sum.isLeft_swap
deleted def Sum.isRight
deleted theorem Sum.isRight_eq_false
deleted theorem Sum.isRight_iff
deleted theorem Sum.isRight_inl
deleted theorem Sum.isRight_inr
deleted theorem Sum.isRight_map
deleted theorem Sum.isRight_swap
deleted theorem Sum.lex_acc_inl
deleted theorem Sum.lex_acc_inr
deleted theorem Sum.lex_inl_inl
deleted theorem Sum.lex_inr_inl
deleted theorem Sum.lex_inr_inr
deleted theorem Sum.lex_wf
deleted theorem Sum.liftRel_inl_inl
deleted theorem Sum.liftRel_inr_inr
deleted theorem Sum.liftRel_swap_iff
deleted theorem Sum.map_comp_map
deleted theorem Sum.map_id_id
deleted theorem Sum.map_inl
deleted theorem Sum.map_inr
deleted theorem Sum.map_map
deleted theorem Sum.not_isLeft
deleted theorem Sum.not_isRight
deleted theorem Sum.not_liftRel_inl_inr
deleted theorem Sum.not_liftRel_inr_inl
deleted def Sum.swap
deleted theorem Sum.swap_inl
deleted theorem Sum.swap_inr
deleted theorem Sum.swap_swap
deleted theorem Sum.swap_swap_eq
deleted theorem Sum.«exists»
deleted theorem Sum.«forall»