Commit 2025-05-14 16:58 2ab0f2d9

View on Github →

style: fix bad tactic indentation (#24890)

Estimated changes

Modified Mathlib/Algebra/Star/Pointwise.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/CategoryTheory/Comma/Final.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/Monad/Comonadicity.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Sums/Products.lean

Modified Mathlib/Combinatorics/Colex.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean

modified theorem SimpleGraph.TripartiteFromTriangles.graph_triple

Modified Mathlib/Control/EquivFunctor.lean

Modified Mathlib/Data/Complex/Norm.lean

Modified Mathlib/Data/EReal/Operations.lean

Modified Mathlib/Data/Finset/Lattice/Prod.lean

Modified Mathlib/Data/Finset/Slice.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Matroid/Loop.lean

Modified Mathlib/Data/Nat/BitIndices.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

modified theorem Nat.Prime.sub_one_mul_multiplicity_factorial

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/MeasureTheory/Group/LIntegral.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

modified theorem ProbabilityTheory.stronglyMeasurable_exponentialPDFReal

Modified Mathlib/Probability/Distributions/Gamma.lean

modified theorem ProbabilityTheory.stronglyMeasurable_gammaPDFReal

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

Modified MathlibTest/ImplicitUniverses.lean