Commit 2023-09-08 21:07 8908a0a5

View on Github →

chore: simplify by rfl (#7039)

Estimated changes

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Lie/CartanMatrix.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

modified theorem AddMonoidAlgebra.gradeBy_id

Modified Mathlib/Algebra/Symmetrized.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

modified theorem CategoryTheory.Idempotents.Karoubi.coe_X

modified theorem CategoryTheory.Idempotents.Karoubi.coe_p

modified theorem CategoryTheory.Idempotents.Karoubi.comp_f

modified theorem CategoryTheory.Idempotents.Karoubi.id_eq

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/PathCategory.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/MvPolynomial/Equiv.lean

Modified Mathlib/Data/Nat/PartENat.lean

modified theorem PartENat.ofENat_none

modified theorem PartENat.ofENat_some

Modified Mathlib/Data/PFunctor/Multivariate/Basic.lean

modified theorem MvPFunctor.const.get_mk

Modified Mathlib/Data/PFunctor/Univariate/M.lean

modified theorem PFunctor.M.dest_mk

Modified Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/LinearAlgebra/BilinearForm.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

modified theorem Valuation.toFun_eq_coe

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified test/toAdditive.lean

modified theorem Test.bar10_works

modified theorem Test.bar11_works