Commit 2023-10-03 10:19 20cc2dcd

View on Github →

feat: lemmas about equiv and logic (#7338)

From the marginal project

Estimated changes

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.elim_apply

added theorem Option.elim_comp

added theorem Option.elim_comp₂

Modified Mathlib/Data/Set/Prod.lean

added theorem Equiv.piCongrLeft_preimage_pi

added theorem Equiv.piCongrLeft_preimage_univ_pi

added theorem Equiv.piCongrLeft_symm_preimage_pi

added theorem Equiv.piCongrLeft_symm_preimage_univ_pi

added theorem Equiv.sumPiEquivProdPi_symm_preimage_univ_pi

added theorem Set.pi_univ_ite

Modified Mathlib/Data/Sum/Basic.lean

added theorem Sum.sum_rec_congr

Modified Mathlib/Logic/Basic.lean

added theorem Eq.rec_eq_cast

added theorem imp_and_neg_imp_iff

Modified Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.piCongrLeft_apply_eq_cast

added theorem Equiv.piCongrLeft_sum_inl

added theorem Equiv.piCongrLeft_sum_inr

added def Equiv.prodPiEquivSumPi

added theorem Equiv.subtypeEquivRight_apply

added theorem Equiv.subtypeEquivRight_symm_apply

added def Equiv.sumPiEquivProdPi