Commit 2024-03-13 11:52 ee18bf38

View on Github →

chore: remove useless tactics (#11333) The removal of some pointless tactics flagged by #11308.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/CategoryTheory/Action.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Images.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

modified theorem CategoryTheory.Limits.cokernel_not_iso_of_nonzero

modified theorem CategoryTheory.Limits.kernel_not_iso_of_nonzero

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/Computability/Halting.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

modified theorem DFinsupp.eq_mk_support

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/Seq/WSeq.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Matrix/Symmetric.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Divisibility.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Game/Basic.lean

Modified Mathlib/SetTheory/Game/Short.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/Topology/StoneCech.lean