Commit 2024-08-27 13:20 45264925

View on Github →

chore: remove autoImplicit from Logic.Equiv.Basic (#16172) Split from #16154.

Estimated changes

modified theorem heq_rec_iff_heq
modified theorem rec_heq_iff_heq
modified theorem rec_heq_of_heq
modified theorem Equiv.Perm.sumCongr_apply
modified theorem Equiv.Perm.sumCongr_refl
modified theorem Equiv.Perm.sumCongr_symm
modified theorem Equiv.Perm.sumCongr_trans
modified theorem Equiv.coe_prodUnique
modified theorem Equiv.coe_sigmaUnique
modified theorem Equiv.coe_uniqueProd
modified theorem Equiv.emptySum_apply_inr
modified def Equiv.ofFiberEquiv
modified theorem Equiv.piCongrLeft_sum_inl
modified theorem Equiv.piCongrLeft_sum_inr
modified def Equiv.piCurry
modified theorem Equiv.piCurry_apply
modified theorem Equiv.piCurry_symm_apply
modified def Equiv.pprodEquivProd
modified def Equiv.pprodProd
modified theorem Equiv.prodComm_apply
modified def Equiv.prodCongr
modified theorem Equiv.prodCongr_symm
modified def Equiv.prodPProd
modified theorem Equiv.prodProdProdComm_symm
modified def Equiv.prodSumDistrib
modified theorem Equiv.prodUnique_apply
modified theorem Equiv.prodUnique_symm_apply
modified def Equiv.psumSum
modified def Equiv.sigmaSumDistrib
modified theorem Equiv.sigmaUnique_apply
modified def Equiv.subtypeCongr
modified def Equiv.subtypeSum
modified theorem Equiv.sumAssoc_apply_inr
modified theorem Equiv.sumCompl_apply_inl
modified theorem Equiv.sumCompl_apply_inr
modified def Equiv.sumCongr
modified theorem Equiv.sumCongr_refl
modified theorem Equiv.sumCongr_symm
modified theorem Equiv.sumCongr_trans
modified theorem Equiv.sumEmpty_apply_inl
modified def Equiv.sumPSum
modified theorem Equiv.ulift_symm_down
modified theorem Equiv.uniqueProd_apply
modified theorem Equiv.uniqueProd_symm_apply