Commit 2024-04-19 20:51 f2658009

View on Github →

chore(Logic): reduce use of autoImplicit (#12135) In one case, replacing this naively errored, so I just merged the single declaration using it. Delete two unused variables in Logic/Basic.

Estimated changes

modified theorem Decidable.eq_or_ne
modified theorem Decidable.ne_or_eq
modified def Function.swap₂
modified theorem Imp.swap
modified theorem Or.elim3
modified theorem Or.imp3
modified theorem PLift.down_inj
modified theorem PLift.down_injective
modified theorem and_or_imp
modified theorem and_symm_left
modified theorem and_symm_right
modified theorem apply_dite₂
modified theorem apply_ite₂
modified theorem beq_eq_decide
modified theorem beq_ext
modified theorem by_cases
modified theorem by_contradiction
modified theorem congr_arg_heq
modified theorem congr_arg_refl
modified theorem congr_fun_congr_arg
modified theorem congr_fun_rfl
modified theorem congr_refl_left
modified theorem congr_refl_right
modified theorem eqRec_heq'
modified theorem eq_equivalence
modified theorem eq_false_intro
modified theorem eq_or_ne
modified theorem eq_true_intro
modified theorem exists_unique_const
modified theorem exists₂_comm
modified theorem forall_imp_iff_exists_imp
modified theorem forall_or_of_or_forall
modified theorem forall₂_swap
modified theorem iff_eq_eq
modified theorem iff_mpr_iff_true_intro
modified theorem imp_iff_or_not
modified theorem imp_iff_right_iff
modified theorem imp_or'
modified theorem lawful_beq_subsingleton
modified theorem ne_and_eq_iff_right
modified theorem ne_of_eq_of_ne
modified theorem ne_of_ne_of_eq
modified theorem ne_or_eq
modified theorem not_beq_of_ne
modified theorem not_ne_iff
modified theorem of_not_imp
modified theorem of_not_not
modified theorem or_congr_left'
modified theorem or_congr_right'
modified theorem or_of_or_of_imp_left
modified theorem or_of_or_of_imp_of_imp
modified theorem or_of_or_of_imp_right
modified theorem xor_comm
modified def Equiv.asEmbedding
modified theorem Equiv.arrowCongr'_symm
modified theorem Equiv.arrowCongr'_trans
modified theorem Equiv.arrowCongr_symm
modified theorem Equiv.arrowCongr_trans
modified def Equiv.equivCongr
modified def Equiv.sigmaCongrLeft
modified def Function.Injective2
modified theorem Function.apply_invFun_apply
modified theorem IsSymmOp.flip_eq
modified theorem eq_rec_inj
modified theorem eq_rec_on_bijective
modified theorem eq_const_of_subsingleton
modified theorem eq_const_of_unique
modified theorem uniqueElim_const