Commit 2024-06-04 05:31 dafacac8

View on Github →

chore: remove some refine' replacing refine_struct (#13490) Split from #13385. In these cases the line count either stays the same or decreases. Also remove references to refine_struct.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Pi.lean

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/PUnitInstances.lean

Modified Mathlib/Algebra/Ring/Aut.lean

modified def RingAut.toAddAut

modified def RingAut.toMulAut

modified def RingAut.toPerm

Modified Mathlib/Algebra/Ring/Pi.lean

Modified Mathlib/Algebra/Ring/ULift.lean

Modified Mathlib/Control/Applicative.lean

Modified Mathlib/Data/DList/Instances.lean

modified def Batteries.DList.listEquivDList

Modified Mathlib/Data/Holor.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Deprecated/Subgroup.lean

modified theorem IsSubgroup.trivial_normal

modified theorem IsSubgroup.univ_subgroup

Modified Mathlib/NumberTheory/Dioph.lean