From 5192777c94aec06289e492ce206d68fbbe72572c Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 1 Jan 2024 19:29:52 +0000 Subject: [PATCH] refactor: decapitalize names in `@[mk_iff]` (#9378) * `@[mk_iff] class MyPred` now generates `myPred_iff`, not `MyPred_iff` * add `Lean.Name.decapitalize` * fix indentation and a few typos in the docs/comments. Partially addresses issue #9129 --- Archive/Imo/Imo1981Q3.lean | 2 +- Mathlib/Algebra/CharP/Basic.lean | 2 +- .../Morphisms/FiniteType.lean | 2 +- .../Morphisms/QuasiCompact.lean | 2 +- .../Morphisms/QuasiSeparated.lean | 4 +- .../Morphisms/UniversallyClosed.lean | 2 +- Mathlib/Analysis/Calculus/TangentCone.lean | 2 +- .../Combinatorics/SimpleGraph/Acyclic.lean | 2 +- .../SimpleGraph/Connectivity.lean | 2 +- Mathlib/Data/Multiset/Basic.lean | 6 +- Mathlib/GroupTheory/Subsemigroup/Center.lean | 4 +- Mathlib/Lean/Name.lean | 6 + .../LinearAlgebra/Dimension/DivisionRing.lean | 2 +- Mathlib/Logic/Relation.lean | 5 +- Mathlib/Logic/UnivLE.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 22 +-- Mathlib/Order/Atoms.lean | 6 +- Mathlib/Order/PrimeIdeal.lean | 6 +- Mathlib/Order/RelClasses.lean | 2 +- Mathlib/RingTheory/Etale.lean | 5 +- Mathlib/RingTheory/Ideal/Cotangent.lean | 4 +- Mathlib/RingTheory/Nilpotent.lean | 2 +- .../Polynomial/Eisenstein/Basic.lean | 2 +- Mathlib/RingTheory/PrincipalIdealDomain.lean | 2 +- Mathlib/SetTheory/Game/PGame.lean | 2 +- Mathlib/Tactic/MkIffOfInductiveProp.lean | 136 +++++++++--------- Mathlib/Topology/Bases.lean | 2 +- Mathlib/Topology/CompletelyRegular.lean | 4 +- .../Connected/TotallyDisconnected.lean | 2 +- Mathlib/Topology/FiberBundle/Basic.lean | 2 +- Mathlib/Topology/Maps.lean | 8 +- Mathlib/Topology/NoetherianSpace.lean | 2 +- Mathlib/Topology/QuasiSeparated.lean | 3 +- Mathlib/Topology/Separation.lean | 4 +- Mathlib/Topology/Sequences.lean | 2 +- Mathlib/Topology/Sober.lean | 2 +- .../UniformSpace/UniformEmbedding.lean | 4 +- test/MkIffOfInductive.lean | 2 +- 38 files changed, 135 insertions(+), 136 deletions(-) diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean index 90b29784e58c4..16b8d382cde78 100644 --- a/Archive/Imo/Imo1981Q3.lean +++ b/Archive/Imo/Imo1981Q3.lean @@ -207,5 +207,5 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by apply this · decide · decide - · norm_num [ProblemPredicate_iff]; decide + · norm_num [problemPredicate_iff]; decide #align imo1981_q3 imo1981_q3 diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean index e312db33bddfc..5b8f1392cf593 100644 --- a/Mathlib/Algebra/CharP/Basic.lean +++ b/Mathlib/Algebra/CharP/Basic.lean @@ -103,7 +103,7 @@ For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorb `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does. This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`. -/ -@[mk_iff charP_iff] +@[mk_iff] class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where cast_eq_zero_iff' : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x #align char_p CharP diff --git a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean b/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean index 13078c9c38642..5d6a653e841f2 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean @@ -43,7 +43,7 @@ class LocallyOfFiniteType (f : X ⟶ Y) : Prop where theorem locallyOfFiniteType_eq : @LocallyOfFiniteType = affineLocally @RingHom.FiniteType := by ext X Y f - rw [LocallyOfFiniteType_iff, affineLocally_iff_affineOpens_le] + rw [locallyOfFiniteType_iff, affineLocally_iff_affineOpens_le] exact RingHom.finiteType_respectsIso #align algebraic_geometry.locally_of_finite_type_eq AlgebraicGeometry.locallyOfFiniteType_eq diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean index dc056e57db862..a5f6eb28aa967 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean @@ -96,7 +96,7 @@ theorem isCompact_open_iff_eq_basicOpen_union {X : Scheme} [IsAffine X] (U : Set theorem quasiCompact_iff_forall_affine : QuasiCompact f ↔ ∀ U : Opens Y.carrier, IsAffineOpen U → IsCompact (f.1.base ⁻¹' (U : Set Y.carrier)) := by - rw [QuasiCompact_iff] + rw [quasiCompact_iff] refine' ⟨fun H U hU => H U U.isOpen hU.isCompact, _⟩ intro H U hU hU' obtain ⟨S, hS, rfl⟩ := (isCompact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩ diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean index 9b251d3054082..3f1ebec5f544d 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean @@ -56,7 +56,7 @@ def QuasiSeparated.affineProperty : AffineTargetMorphismProperty := fun X _ _ _ theorem quasiSeparatedSpace_iff_affine (X : Scheme) : QuasiSeparatedSpace X.carrier ↔ ∀ U V : X.affineOpens, IsCompact (U ∩ V : Set X.carrier) := by - rw [QuasiSeparatedSpace_iff] + rw [quasiSeparatedSpace_iff] constructor · intro H U V; exact H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact · intro H @@ -115,7 +115,7 @@ theorem quasi_compact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsA #align algebraic_geometry.quasi_compact_affine_property_iff_quasi_separated_space AlgebraicGeometry.quasi_compact_affineProperty_iff_quasiSeparatedSpace theorem quasiSeparated_eq_diagonal_is_quasiCompact : - @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact := by ext; exact QuasiSeparated_iff _ + @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact := by ext; exact quasiSeparated_iff _ #align algebraic_geometry.quasi_separated_eq_diagonal_is_quasi_compact AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact theorem quasi_compact_affineProperty_diagonal_eq : diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean index 05339be03fc5d..b9aba7a2bb1bf 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean @@ -43,7 +43,7 @@ class UniversallyClosed (f : X ⟶ Y) : Prop where #align algebraic_geometry.universally_closed AlgebraicGeometry.UniversallyClosed theorem universallyClosed_eq : @UniversallyClosed = universally (topologically @IsClosedMap) := by - ext X Y f; rw [UniversallyClosed_iff] + ext X Y f; rw [universallyClosed_iff] #align algebraic_geometry.universally_closed_eq AlgebraicGeometry.universallyClosed_eq theorem universallyClosed_respectsIso : RespectsIso @UniversallyClosed := diff --git a/Mathlib/Analysis/Calculus/TangentCone.lean b/Mathlib/Analysis/Calculus/TangentCone.lean index 34e2f39c5bbb6..0eea4602ee8df 100644 --- a/Mathlib/Analysis/Calculus/TangentCone.lean +++ b/Mathlib/Analysis/Calculus/TangentCone.lean @@ -56,7 +56,7 @@ The main role of this property is to ensure that the differential within `s` at hence this name. The uniqueness it asserts is proved in `UniqueDiffWithinAt.eq` in `Fderiv.Basic`. To avoid pathologies in dimension 0, we also require that `x` belongs to the closure of `s` (which is automatic when `E` is not `0`-dimensional). -/ -@[mk_iff uniqueDiffWithinAt_iff] +@[mk_iff] structure UniqueDiffWithinAt (s : Set E) (x : E) : Prop where dense_tangentCone : Dense (Submodule.span 𝕜 (tangentConeAt 𝕜 s x) : Set E) mem_closure : x ∈ closure s diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index 1c02bf8f62db3..9f1601be19201 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean @@ -134,7 +134,7 @@ theorem isAcyclic_iff_path_unique : G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.P theorem isTree_iff_existsUnique_path : G.IsTree ↔ Nonempty V ∧ ∀ v w : V, ∃! p : G.Walk v w, p.IsPath := by classical - rw [IsTree_iff, isAcyclic_iff_path_unique] + rw [isTree_iff, isAcyclic_iff_path_unique] constructor · rintro ⟨hc, hu⟩ refine ⟨hc.nonempty, ?_⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean index 83c4a00358465..778bb1bad5a96 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean @@ -2037,7 +2037,7 @@ This follows the convention observed by mathlib that something is connected iff exactly one connected component. There is a `CoeFun` instance so that `h u v` can be used instead of `h.Preconnected u v`. -/ -@[mk_iff connected_iff] +@[mk_iff] structure Connected : Prop where protected preconnected : G.Preconnected protected [nonempty : Nonempty V] diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index e0b3640e52acf..b847b159bf5ca 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -2744,7 +2744,7 @@ inductive Rel (r : α → β → Prop) : Multiset α → Multiset β → Prop | zero : Rel r 0 0 | cons {a b as bs} : r a b → Rel r as bs → Rel r (a ::ₘ as) (b ::ₘ bs) #align multiset.rel Multiset.Rel -#align multiset.rel_iff Multiset.Rel_iff +#align multiset.rel_iff Multiset.rel_iff variable {δ : Type*} {r : α → β → Prop} {p : γ → δ → Prop} @@ -2796,11 +2796,11 @@ theorem rel_flip_eq {s t : Multiset α} : Rel (fun a b => b = a) s t ↔ s = t : #align multiset.rel_flip_eq Multiset.rel_flip_eq @[simp] -theorem rel_zero_left {b : Multiset β} : Rel r 0 b ↔ b = 0 := by rw [Rel_iff]; simp +theorem rel_zero_left {b : Multiset β} : Rel r 0 b ↔ b = 0 := by rw [rel_iff]; simp #align multiset.rel_zero_left Multiset.rel_zero_left @[simp] -theorem rel_zero_right {a : Multiset α} : Rel r a 0 ↔ a = 0 := by rw [Rel_iff]; simp +theorem rel_zero_right {a : Multiset α} : Rel r a 0 ↔ a = 0 := by rw [rel_iff]; simp #align multiset.rel_zero_right Multiset.rel_zero_right theorem rel_cons_left {a as bs} : diff --git a/Mathlib/GroupTheory/Subsemigroup/Center.lean b/Mathlib/GroupTheory/Subsemigroup/Center.lean index dd4c15de90db2..555e6dcfd3760 100644 --- a/Mathlib/GroupTheory/Subsemigroup/Center.lean +++ b/Mathlib/GroupTheory/Subsemigroup/Center.lean @@ -56,9 +56,7 @@ structure IsMulCentral [Mul M] (z : M) : Prop where /-- associative property for right multiplication -/ right_assoc (a b : M) : (a * b) * z = a * (b * z) --- TODO: these should have explicit arguments (mathlib4#9129) -attribute [mk_iff isMulCentral_iff] IsMulCentral -attribute [mk_iff isAddCentral_iff] IsAddCentral +attribute [mk_iff] IsMulCentral IsAddCentral attribute [to_additive existing] isMulCentral_iff namespace IsMulCentral diff --git a/Mathlib/Lean/Name.lean b/Mathlib/Lean/Name.lean index f79c010c65e1f..ee2cf29cee6b7 100644 --- a/Mathlib/Lean/Name.lean +++ b/Mathlib/Lean/Name.lean @@ -55,3 +55,9 @@ def getModule (name : Name) (s := "") : Name := | .anonymous => s | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}." | .str pre s => getModule pre s + +/-- Decapitalize the last component of a name. -/ +def Lean.Name.decapitalize (n : Name) : Name := + n.modifyBase fun + | .str p s => .str p s.decapitalize + | n => n diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index 89f7d68b6c890..ceaced347eef7 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -302,7 +302,7 @@ theorem rank_submodule_le_one_iff' (s : Submodule K V) : theorem Submodule.rank_le_one_iff_isPrincipal (W : Submodule K V) : Module.rank K W ≤ 1 ↔ W.IsPrincipal := by - simp only [rank_le_one_iff, Submodule.IsPrincipal_iff, le_antisymm_iff, le_span_singleton_iff, + simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff, span_singleton_le_iff_mem] constructor · rintro ⟨⟨m, hm⟩, hm'⟩ diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean index 544154eba73fb..6fcfb39847fdb 100644 --- a/Mathlib/Logic/Relation.lean +++ b/Mathlib/Logic/Relation.lean @@ -256,16 +256,15 @@ inductive ReflTransGen (r : α → α → Prop) (a : α) : α → Prop attribute [refl] ReflTransGen.refl /-- `ReflGen r`: reflexive closure of `r` -/ -@[mk_iff reflGen_iff] +@[mk_iff] inductive ReflGen (r : α → α → Prop) (a : α) : α → Prop | refl : ReflGen r a a | single {b} : r a b → ReflGen r a b #align relation.refl_gen Relation.ReflGen - #align relation.refl_gen_iff Relation.reflGen_iff /-- `TransGen r`: transitive closure of `r` -/ -@[mk_iff transGen_iff] +@[mk_iff] inductive TransGen (r : α → α → Prop) (a : α) : α → Prop | single {b} : r a b → TransGen r a b | tail {b c} : TransGen r a b → r b c → TransGen r a c diff --git a/Mathlib/Logic/UnivLE.lean b/Mathlib/Logic/UnivLE.lean index 022ac1934516c..aad869948aea4 100644 --- a/Mathlib/Logic/UnivLE.lean +++ b/Mathlib/Logic/UnivLE.lean @@ -59,5 +59,5 @@ instance univLE_of_max [UnivLE.{max u v, v}] : UnivLE.{u, v} := @UnivLE.trans un -- example (α : Type u) (β : Type v) [UnivLE.{u, v}] : Small.{v} (α → β) := inferInstance example : ¬ UnivLE.{u+1, u} := by - simp only [Small_iff, not_forall, not_exists, not_nonempty_iff] + simp only [small_iff, not_forall, not_exists, not_nonempty_iff] exact ⟨Type u, fun α => ⟨fun f => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩⟩ diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 072f72e49bc12..1f07282403dca 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -103,18 +103,18 @@ theorem iff_adjoin_eq_top : theorem iff_singleton : IsCyclotomicExtension {n} A B ↔ (∃ r : B, IsPrimitiveRoot r n) ∧ ∀ x, x ∈ adjoin A {b : B | b ^ (n : ℕ) = 1} := - by simp [IsCyclotomicExtension_iff] + by simp [isCyclotomicExtension_iff] #align is_cyclotomic_extension.iff_singleton IsCyclotomicExtension.iff_singleton /-- If `IsCyclotomicExtension ∅ A B`, then the image of `A` in `B` equals `B`. -/ theorem empty [h : IsCyclotomicExtension ∅ A B] : (⊥ : Subalgebra A B) = ⊤ := by - simpa [Algebra.eq_top_iff, IsCyclotomicExtension_iff] using h + simpa [Algebra.eq_top_iff, isCyclotomicExtension_iff] using h #align is_cyclotomic_extension.empty IsCyclotomicExtension.empty /-- If `IsCyclotomicExtension {1} A B`, then the image of `A` in `B` equals `B`. -/ theorem singleton_one [h : IsCyclotomicExtension {1} A B] : (⊥ : Subalgebra A B) = ⊤ := Algebra.eq_top_iff.2 fun x => by - simpa [adjoin_singleton_one] using ((IsCyclotomicExtension_iff _ _ _).1 h).2 x + simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x #align is_cyclotomic_extension.singleton_one IsCyclotomicExtension.singleton_one variable {A B} @@ -137,16 +137,16 @@ theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTow (h : Function.Injective (algebraMap B C)) : IsCyclotomicExtension (S ∪ T) A C := by refine' ⟨fun hn => _, fun x => _⟩ · cases' hn with hn hn - · obtain ⟨b, hb⟩ := ((IsCyclotomicExtension_iff _ _ _).1 hS).1 hn + · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn refine' ⟨algebraMap B C b, _⟩ exact hb.map_of_injective h - · exact ((IsCyclotomicExtension_iff _ _ _).1 hT).1 hn - · refine' adjoin_induction (((IsCyclotomicExtension_iff T B _).1 hT).2 x) + · exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn + · refine' adjoin_induction (((isCyclotomicExtension_iff T B _).1 hT).2 x) (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => _) (fun x y hx hy => Subalgebra.add_mem _ hx hy) fun x y hx hy => Subalgebra.mul_mem _ hx hy · let f := IsScalarTower.toAlgHom A B C have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}).map f := - ⟨b, ((IsCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩ + ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩ rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb refine' adjoin_mono (fun y hy => _) hb obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy @@ -185,8 +185,8 @@ theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] : · rintro x (⟨n, hn⟩ | ⟨n, hn⟩) · exact ⟨n, Or.inl hn.1, hn.2⟩ · exact ⟨n, Or.inr hn.1, hn.2⟩ - refine' ⟨fun hn => ((IsCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => _⟩ - replace h := ((IsCyclotomicExtension_iff _ _ _).1 h).2 b + refine' ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => _⟩ + replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h #align is_cyclotomic_extension.union_right IsCyclotomicExtension.union_right @@ -196,7 +196,7 @@ given by roots of unity of order in `S`. -/ theorem union_left [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) : IsCyclotomicExtension S A (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}) := by refine' ⟨@fun n hn => _, fun b => _⟩ - · obtain ⟨b, hb⟩ := ((IsCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) + · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) refine' ⟨⟨b, subset_adjoin ⟨n, hn, hb.pow_eq_one⟩⟩, _⟩ rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk] · convert mem_top (R := A) (x := b) @@ -443,7 +443,7 @@ theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) : Splits (algebraMap K L) (X ^ (n : ℕ) - 1) := by rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X] - obtain ⟨z, hz⟩ := ((IsCyclotomicExtension_iff _ _ _).1 H).1 hS + obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS exact X_pow_sub_one_splits hz set_option linter.uppercaseLean3 false in #align is_cyclotomic_extension.splits_X_pow_sub_one IsCyclotomicExtension.splits_X_pow_sub_one diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean index f967ed6d32a64..7ab1fbb46c5a0 100644 --- a/Mathlib/Order/Atoms.lean +++ b/Mathlib/Order/Atoms.lean @@ -265,7 +265,7 @@ class IsAtomic [OrderBot α] : Prop where /--Every element other than `⊥` has an atom below it. -/ eq_bot_or_exists_atom_le : ∀ b : α, b = ⊥ ∨ ∃ a : α, IsAtom a ∧ a ≤ b #align is_atomic IsAtomic -#align is_atomic_iff IsAtomic_iff +#align is_atomic_iff isAtomic_iff /-- A lattice is coatomic iff every element other than `⊤` has a coatom above it. -/ @[mk_iff] @@ -273,7 +273,7 @@ class IsCoatomic [OrderTop α] : Prop where /--Every element other than `⊤` has an atom above it. -/ eq_top_or_exists_le_coatom : ∀ b : α, b = ⊤ ∨ ∃ a : α, IsCoatom a ∧ b ≤ a #align is_coatomic IsCoatomic -#align is_coatomic_iff IsCoatomic_iff +#align is_coatomic_iff isCoatomic_iff export IsAtomic (eq_bot_or_exists_atom_le) @@ -915,7 +915,7 @@ theorem isSimpleOrder [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] protected theorem isAtomic_iff [OrderBot α] [OrderBot β] (f : α ≃o β) : IsAtomic α ↔ IsAtomic β := by - simp only [IsAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq, + simp only [isAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq, f.le_iff_le, f.isAtom_iff] #align order_iso.is_atomic_iff OrderIso.isAtomic_iff diff --git a/Mathlib/Order/PrimeIdeal.lean b/Mathlib/Order/PrimeIdeal.lean index 77096ecd3fa28..9e4166566f42c 100644 --- a/Mathlib/Order/PrimeIdeal.lean +++ b/Mathlib/Order/PrimeIdeal.lean @@ -129,10 +129,10 @@ theorem IsPrime.mem_or_mem (hI : IsPrime I) {x y : P} : x ⊓ y ∈ I → x ∈ theorem IsPrime.of_mem_or_mem [IsProper I] (hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) : IsPrime I := by - rw [IsPrime_iff] + rw [isPrime_iff] use ‹_› refine .of_def ?_ ?_ ?_ - · exact Set.nonempty_compl.2 (I.IsProper_iff.1 ‹_›) + · exact Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›) · intro x hx y hy exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩ · exact @mem_compl_of_ge _ _ _ @@ -195,7 +195,7 @@ theorem isPrime_iff_mem_or_compl_mem [IsProper I] : IsPrime I ↔ ∀ {x : P}, x #align order.ideal.is_prime_iff_mem_or_compl_mem Order.Ideal.isPrime_iff_mem_or_compl_mem instance (priority := 100) IsPrime.isMaximal [IsPrime I] : IsMaximal I := by - simp only [IsMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and] + simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and] intro J hIJ x rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩ suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean index f8b22f2e4d7cd..d6cc4a85990a6 100644 --- a/Mathlib/Order/RelClasses.lean +++ b/Mathlib/Order/RelClasses.lean @@ -276,7 +276,7 @@ instance (priority := 100) isStrictTotalOrder_of_isStrictTotalOrder [IsStrictTot /-- The relation is `WellFounded`, as a proposition. -/ wf : WellFounded r #align is_well_founded IsWellFounded -#align is_well_founded_iff IsWellFounded_iff +#align is_well_founded_iff isWellFounded_iff #align has_well_founded WellFoundedRelation set_option linter.uppercaseLean3 false in diff --git a/Mathlib/RingTheory/Etale.lean b/Mathlib/RingTheory/Etale.lean index d6ba0d8dbd727..69ff6654b6149 100644 --- a/Mathlib/RingTheory/Etale.lean +++ b/Mathlib/RingTheory/Etale.lean @@ -71,9 +71,8 @@ variable {R A} theorem FormallyEtale.iff_unramified_and_smooth : FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A := by - rw [FormallyUnramified_iff, FormallySmooth_iff, FormallyEtale_iff] - simp_rw [← forall_and] - rfl + rw [formallyUnramified_iff, formallySmooth_iff, formallyEtale_iff] + simp_rw [← forall_and, Function.Bijective] #align algebra.formally_etale.iff_unramified_and_smooth Algebra.FormallyEtale.iff_unramified_and_smooth instance (priority := 100) FormallyEtale.to_unramified [h : FormallyEtale R A] : diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 981529c976a68..0a447594eab0a 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -252,8 +252,8 @@ lemma finrank_cotangentSpace_eq_zero (R) [Field R] : open Submodule in theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ (maximalIdeal R).IsPrincipal := by - rw [Module.finrank_le_one_iff_top_isPrincipal, IsPrincipal_iff, - (maximalIdeal R).toCotangent_surjective.exists, IsPrincipal_iff] + rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff, + (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff] simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff, ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton, Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)] diff --git a/Mathlib/RingTheory/Nilpotent.lean b/Mathlib/RingTheory/Nilpotent.lean index d2a26a7c3269b..afa8f15e32a98 100644 --- a/Mathlib/RingTheory/Nilpotent.lean +++ b/Mathlib/RingTheory/Nilpotent.lean @@ -122,7 +122,7 @@ theorem Commute.IsNilpotent.add_isUnit [Ring R] {r : R} {u : Rˣ} (hnil : IsNilp simp /-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements. -/ -@[mk_iff isReduced_iff] +@[mk_iff] class IsReduced (R : Type*) [Zero R] [Pow R ℕ] : Prop where /-- A reduced structure has no nonzero nilpotent elements. -/ eq_zero : ∀ x : R, IsNilpotent x → x = 0 diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean index 6c91a6536646e..697588e732457 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean @@ -64,7 +64,7 @@ variable [CommSemiring R] {𝓟 : Ideal R} {f : R[X]} (hf : f.IsWeaklyEisenstein theorem map {A : Type v} [CommRing A] (φ : R →+* A) : (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ) := by - refine' (IsWeaklyEisensteinAt_iff _ _).2 fun hn => _ + refine' (isWeaklyEisensteinAt_iff _ _).2 fun hn => _ rw [coeff_map] exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (natDegree_map_le _ _))) #align polynomial.is_weakly_eisenstein_at.map Polynomial.IsWeaklyEisensteinAt.map diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean index d5b05d9da86d0..3a1dbeaa435c4 100644 --- a/Mathlib/RingTheory/PrincipalIdealDomain.lean +++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean @@ -69,7 +69,7 @@ instance top_isPrincipal : (⊤ : Submodule R R).IsPrincipal := variable (R) /-- A ring is a principal ideal ring if all (left) ideals are principal. -/ -@[mk_iff isPrincipalIdealRing_iff] +@[mk_iff] class IsPrincipalIdealRing (R : Type u) [Ring R] : Prop where principal : ∀ S : Ideal R, S.IsPrincipal #align is_principal_ideal_ring IsPrincipalIdealRing diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 3695f3b348232..03db93db84227 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -1256,7 +1256,7 @@ theorem neg_ofLists (L R : List PGame) : #align pgame.neg_of_lists SetTheory.PGame.neg_ofLists theorem isOption_neg {x y : PGame} : IsOption x (-y) ↔ IsOption (-x) y := by - rw [IsOption_iff, IsOption_iff, or_comm] + rw [isOption_iff, isOption_iff, or_comm] cases y; apply or_congr <;> · apply exists_congr diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean index c28374a2d10db..6efae87acb7bc 100644 --- a/Mathlib/Tactic/MkIffOfInductiveProp.lean +++ b/Mathlib/Tactic/MkIffOfInductiveProp.lean @@ -6,6 +6,7 @@ Authors: Johannes Hölzl, David Renshaw import Lean import Std.Tactic.LeftRight import Mathlib.Lean.Meta +import Mathlib.Lean.Name import Mathlib.Tactic.Basic /-! @@ -17,20 +18,18 @@ the following type: ```lean ∀ {α : Type*} (R : α → α → Prop) (a : α) (l : List α), - Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l' + Chain R a l ↔ l = [] ∨ ∃ (b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l' ``` This tactic can be called using either the `mk_iff_of_inductive_prop` user command or the `mk_iff` attribute. -/ -set_option autoImplicit true - namespace Mathlib.Tactic.MkIff open Lean Meta Elab -/-- `select m n` runs `right` `m` times, and then `left` `(n-m)` times. +/-- `select m n` runs `right` `m` times; if `m < n`, then it also runs `left` once. Fails if `n < m`. -/ private def select (m n : Nat) (goal : MVarId) : MetaM MVarId := match m,n with @@ -47,7 +46,7 @@ private def select (m n : Nat) (goal : MVarId) : MetaM MVarId := /-- `compactRelation bs as_ps`: Produce a relation of the form: ```lean -R := λ as ∃ bs, Λ_i a_i = p_i[bs] +R := fun as ↦ ∃ bs, ⋀_i a_i = p_i[bs] ``` This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`. @@ -56,13 +55,14 @@ partial def compactRelation : List Expr → List (Expr × Expr) → List (Option Expr) × List (Expr × Expr) × (Expr → Expr) | [], as_ps => ([], as_ps, id) | b::bs, as_ps => - match as_ps.span (λ⟨_,p⟩ => ¬ p == b) with + match as_ps.span (fun ⟨_, p⟩ ↦ p != b) with | (_, []) => -- found nothing in ps equal to b - let (bs, as_ps', subst) := compactRelation bs as_ps - (b::bs, as_ps', subst) + let (bs, as_ps', subst) := compactRelation bs as_ps + (b::bs, as_ps', subst) | (ps₁, (a, _) :: ps₂) => -- found one that matches b. Remove it. let i := fun e ↦ e.replaceFVar b a - let (bs, as_ps', subst) := compactRelation (bs.map i) ((ps₁ ++ ps₂).map (λ⟨a, p⟩ => (a, i p))) + let (bs, as_ps', subst) := + compactRelation (bs.map i) ((ps₁ ++ ps₂).map (fun ⟨a, p⟩ ↦ (a, i p))) (none :: bs, as_ps', i ∘ subst) private def updateLambdaBinderInfoD! (e : Expr) : Expr := @@ -70,24 +70,25 @@ private def updateLambdaBinderInfoD! (e : Expr) : Expr := | .lam n domain body _ => .lam n domain body .default | _ => panic! "lambda expected" -/-- Generates an expression of the form `∃(args), inner`. `args` is assumed to be a list of fvars. -When possible, `p ∧ q` is used instead of `∃(_ : p), q`. -/ +/-- Generates an expression of the form `∃ (args), inner`. `args` is assumed to be a list of fvars. +When possible, `p ∧ q` is used instead of `∃ (_ : p), q`. -/ def mkExistsList (args : List Expr) (inner : Expr) : MetaM Expr := -args.foldrM (λarg i:Expr => do - let t ← inferType arg - let l := (← inferType t).sortLevel! - if arg.occurs i || l != Level.zero - then pure (mkApp2 (mkConst `Exists [l] : Expr) t - (updateLambdaBinderInfoD! <| ← mkLambdaFVars #[arg] i)) - else pure <| mkApp2 (mkConst `And [] : Expr) t i) - inner + args.foldrM + (fun arg i:Expr => do + let t ← inferType arg + let l := (← inferType t).sortLevel! + if arg.occurs i || l != Level.zero + then pure (mkApp2 (.const `Exists [l]) t + (updateLambdaBinderInfoD! <| ← mkLambdaFVars #[arg] i)) + else pure <| mkApp2 (mkConst `And) t i) + inner /-- `mkOpList op empty [x1, x2, ...]` is defined as `op x1 (op x2 ...)`. Returns `empty` if the list is empty. -/ def mkOpList (op : Expr) (empty : Expr) : List Expr → Expr | [] => empty | [e] => e - | (e :: es) => mkApp2 op e $ mkOpList op empty es + | (e :: es) => mkApp2 op e <| mkOpList op empty es /-- `mkAndList [x1, x2, ...]` is defined as `x1 ∧ (x2 ∧ ...)`, or `True` if the list is empty. -/ def mkAndList : List Expr → Expr := mkOpList (mkConst `And) (mkConst `True) @@ -96,7 +97,7 @@ def mkAndList : List Expr → Expr := mkOpList (mkConst `And) (mkConst `True) def mkOrList : List Expr → Expr := mkOpList (mkConst `Or) (mkConst `False) /-- Drops the final element of a list. -/ -def List.init : List α → List α +def List.init {α : Type*} : List α → List α | [] => [] | [_] => [] | a::l => a::init l @@ -120,7 +121,7 @@ structure Shape : Type where ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, R a b → List.Chain R b l → List.Chain R a (b :: l) ``` - and the `a : α` gets eliminated, so `compactRelation = [false,true,true,true,true]`. + and the `a : α` gets eliminated, so `variablesKept = [false,true,true,true,true]`. -/ variablesKept : List Bool @@ -133,37 +134,36 @@ structure Shape : Type where while proving the iff theorem, and a proposition representing the constructor. -/ def constrToProp (univs : List Level) (params : List Expr) (idxs : List Expr) (c : Name) : - MetaM (Shape × Expr) := -do let type := (← getConstInfo c).instantiateTypeLevelParams univs - let type' ← Meta.forallBoundedTelescope type (params.length) fun fvars ty ↦ do - pure $ ty.replaceFVars fvars params.toArray - - Meta.forallTelescope type' fun fvars ty ↦ do - let idxs_inst := ty.getAppArgs.toList.drop params.length - let (bs, eqs, subst) := compactRelation fvars.toList (idxs.zip idxs_inst) - let eqs ← eqs.mapM (λ⟨idx, inst⟩ => do - let ty ← idx.fvarId!.getType - let instTy ← inferType inst - let u := (← inferType ty).sortLevel! - if ← isDefEq ty instTy - then pure (mkApp3 (mkConst `Eq [u]) ty idx inst) - else pure (mkApp4 (mkConst `HEq [u]) ty idx instTy inst)) - let (n, r) ← match bs.filterMap id, eqs with - | [], [] => do - pure (some 0, (mkConst `True)) - | bs', [] => do - let t : Expr ← bs'.getLast!.fvarId!.getType - let l := (← inferType t).sortLevel! - if l == Level.zero then do - let r ← mkExistsList (List.init bs') t - pure (none, subst r) - else do - let r ← mkExistsList bs' (mkConst `True) - pure (some 0, subst r) - | bs', _ => do - let r ← mkExistsList bs' (mkAndList eqs) - pure (some eqs.length, subst r) - pure (⟨bs.map Option.isSome, n⟩, r) + MetaM (Shape × Expr) := do + let type := (← getConstInfo c).instantiateTypeLevelParams univs + let type' ← Meta.forallBoundedTelescope type (params.length) fun fvars ty ↦ do + pure <| ty.replaceFVars fvars params.toArray + Meta.forallTelescope type' fun fvars ty ↦ do + let idxs_inst := ty.getAppArgs.toList.drop params.length + let (bs, eqs, subst) := compactRelation fvars.toList (idxs.zip idxs_inst) + let eqs ← eqs.mapM (fun ⟨idx, inst⟩ ↦ do + let ty ← idx.fvarId!.getType + let instTy ← inferType inst + let u := (← inferType ty).sortLevel! + if ← isDefEq ty instTy + then pure (mkApp3 (.const `Eq [u]) ty idx inst) + else pure (mkApp4 (.const `HEq [u]) ty idx instTy inst)) + let (n, r) ← match bs.filterMap id, eqs with + | [], [] => do + pure (some 0, (mkConst `True)) + | bs', [] => do + let t : Expr ← bs'.getLast!.fvarId!.getType + let l := (← inferType t).sortLevel! + if l == Level.zero then do + let r ← mkExistsList (List.init bs') t + pure (none, subst r) + else do + let r ← mkExistsList bs' (mkConst `True) + pure (some 0, subst r) + | bs', _ => do + let r ← mkExistsList bs' (mkAndList eqs) + pure (some eqs.length, subst r) + pure (⟨bs.map Option.isSome, n⟩, r) /-- Splits the goal `n` times via `refine ⟨?_,?_⟩`, and then applies `constructor` to close the resulting subgoals. @@ -171,15 +171,15 @@ close the resulting subgoals. def splitThenConstructor (mvar : MVarId) (n : Nat) : MetaM Unit := match n with | 0 => do - let (subgoals',_) ← Term.TermElabM.run $ Tactic.run mvar do + let (subgoals',_) ← Term.TermElabM.run <| Tactic.run mvar do Tactic.evalTactic (← `(tactic| constructor)) let [] := subgoals' | throwError "expected no subgoals" pure () | n + 1 => do - let (subgoals,_) ← Term.TermElabM.run $ Tactic.run mvar do + let (subgoals,_) ← Term.TermElabM.run <| Tactic.run mvar do Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩)) let [sg1, sg2] := subgoals | throwError "expected two subgoals" - let (subgoals',_) ← Term.TermElabM.run $ Tactic.run sg1 do + let (subgoals',_) ← Term.TermElabM.run <| Tactic.run sg1 do Tactic.evalTactic (← `(tactic| constructor)) let [] := subgoals' | throwError "expected no subgoals" splitThenConstructor sg2 n @@ -193,7 +193,7 @@ do let subgoals ← mvar'.cases h let _ ← (shape.zip subgoals.toList).enum.mapM fun ⟨p, ⟨⟨shape, t⟩, subgoal⟩⟩ ↦ do let vars := subgoal.fields - let si := (shape.zip vars.toList).filterMap (λ ⟨c,v⟩ => if c then some v else none) + let si := (shape.zip vars.toList).filterMap (fun ⟨c,v⟩ ↦ if c then some v else none) let mvar'' ← select p (subgoals.size - 1) subgoal.mvarId match t with | none => do @@ -256,7 +256,7 @@ def toInductive (mvar : MVarId) (cs : List Name) pure () | (n + 1) => do let subgoals ← nCasesSum n mvar h - let _ ← (cs.zip (subgoals.zip s)).mapM $ λ⟨constr_name, ⟨h, mv⟩, bs, e⟩ => do + let _ ← (cs.zip (subgoals.zip s)).mapM fun ⟨constr_name, ⟨h, mv⟩, bs, e⟩ ↦ do let n := (bs.filter id).length let (mvar', _fvars) ← match e with | none => nCasesProd (n-1) mv h @@ -272,18 +272,17 @@ def toInductive (mvar : MVarId) (cs : List Name) `subst` will change the dependent hypotheses, so that the `uniq` local names are wrong afterwards. Instead we revert them and pull them out one-by-one. -/ let (_, mv3) ← mv2.revert fvars'.toArray - let mv4 ← fvars'.foldlM (λ mv _ => do let ⟨fv, mv'⟩ ← mv.intro1 - subst mv' fv - ) mv3 + let mv4 ← fvars'.foldlM (fun mv _ ↦ do let ⟨fv, mv'⟩ ← mv.intro1; subst mv' fv) mv3 pure (mv4, fvars) mvar'.withContext do let fvarIds := (← getLCtx).getFVarIds.toList let gs := fvarIds.take gs.length let hs := (fvarIds.reverse.take n).reverse let m := gs.map some ++ listBoolMerge bs hs - let args ← m.mapM (λa => match a with - | some v => pure $ mkFVar v - | none => mkFreshExprMVar none) + let args ← m.mapM fun a ↦ + match a with + | some v => pure (mkFVar v) + | none => mkFreshExprMVar none let c ← mkConstWithFreshMVarLevels constr_name let e := mkAppN c args.toArray let t ← inferType e @@ -305,14 +304,13 @@ def mkIffOfInductivePropImpl (ind : Name) (rel : Name) (relStx : Syntax) : MetaM /- we use these names for our universe parameters, maybe we should construct a copy of them using `uniq_name` -/ - let (thmTy,shape) ← Meta.forallTelescope type fun fvars ty ↦ do + let (thmTy, shape) ← Meta.forallTelescope type fun fvars ty ↦ do if !ty.isProp then throwError "mk_iff only applies to prop-valued declarations" let lhs := mkAppN (mkConst ind univs) fvars let fvars' := fvars.toList let shape_rhss ← constrs.mapM (constrToProp univs (fvars'.take params) (fvars'.drop params)) let (shape, rhss) := shape_rhss.unzip - pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)), - shape) + pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)), shape) let mvar ← mkFreshExprMVar (some thmTy) let mvarId := mvar.mvarId! @@ -324,7 +322,7 @@ def mkIffOfInductivePropImpl (ind : Name) (rel : Name) (relStx : Syntax) : MetaM let ⟨mprFvar, mpr'⟩ ← mpr.intro1 toInductive mpr' constrs ((fvars.toList.take params).map .fvar) shape mprFvar - addDecl $ .thmDecl { + addDecl <| .thmDecl { name := rel levelParams := univNames type := thmTy @@ -410,7 +408,7 @@ initialize Lean.registerBuiltinAttribute { let (tgt, idStx) ← match stx with | `(attr| mk_iff $tgt:ident) => pure ((← mkDeclName (← getCurrNamespace) {} tgt.getId).1, tgt.raw) - | `(attr| mk_iff) => pure (decl.appendAfter "_iff", stx) + | `(attr| mk_iff) => pure (decl.decapitalize.appendAfter "_iff", stx) | _ => throwError "unrecognized syntax" mkIffOfInductivePropImpl decl tgt idStx } diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 7cd5f90c3210d..552be4211a378 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -411,7 +411,7 @@ instance [SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s) := /-- A topological space with discrete topology is separable iff it is countable. -/ theorem separableSpace_iff_countable [DiscreteTopology α] : SeparableSpace α ↔ Countable α := by - simp [SeparableSpace_iff, countable_univ_iff] + simp [separableSpace_iff, countable_univ_iff] /-- In a separable space, a family of nonempty disjoint open sets is countable. -/ theorem _root_.Set.PairwiseDisjoint.countable_of_isOpen [SeparableSpace α] {ι : Type*} diff --git a/Mathlib/Topology/CompletelyRegular.lean b/Mathlib/Topology/CompletelyRegular.lean index 54bbdfd4a5b76..2d3a61b59fe76 100644 --- a/Mathlib/Topology/CompletelyRegular.lean +++ b/Mathlib/Topology/CompletelyRegular.lean @@ -57,7 +57,7 @@ variable {X : Type u} [TopologicalSpace X] [T1Space X] /-- A space is completely regular if points can be separated from closed sets via continuous functions to the unit interval. -/ -@[mk_iff completelyRegularSpace_iff] +@[mk_iff] class CompletelyRegularSpace (X : Type u) [TopologicalSpace X] : Prop where completely_regular : ∀ (x : X), ∀ K : Set X, IsClosed K → x ∉ K → ∃ f : X → I, Continuous f ∧ f x = 0 ∧ EqOn f 1 K @@ -83,7 +83,7 @@ instance NormalSpace.instCompletelyRegularSpace [NormalSpace X] : CompletelyRegu exact ⟨g, cg, hgx, hgK⟩ /-- A T₃.₅ space is a completely regular space that is also T1. -/ -@[mk_iff t35Space_iff] +@[mk_iff] class T35Space (X : Type u) [TopologicalSpace X] extends T1Space X, CompletelyRegularSpace X : Prop instance T35Space.instT3space [T35Space X] : T3Space X := by diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index 850230f42c47c..db4bc6f348fdb 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -170,7 +170,7 @@ lemma Embedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β lemma Embedding.isTotallyDisconnected_range [TopologicalSpace β] {f : α → β} (hf : Embedding f) : IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α := by - rw [TotallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image] + rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image] lemma totallyDisconnectedSpace_subtype_iff {s : Set α} : TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s := by diff --git a/Mathlib/Topology/FiberBundle/Basic.lean b/Mathlib/Topology/FiberBundle/Basic.lean index 7a7b1ea958d91..b251e404f5359 100644 --- a/Mathlib/Topology/FiberBundle/Basic.lean +++ b/Mathlib/Topology/FiberBundle/Basic.lean @@ -216,7 +216,7 @@ for trivializations of `E`, expressing that a trivialization is in the designate bundle. This is needed because lemmas about the linearity of trivializations or the continuity (as functions to `F →L[R] F`, where `F` is the model fiber) of the transition functions are only expected to hold for trivializations in the designated atlas. -/ -@[mk_iff memTrivializationAtlas_iff] +@[mk_iff] class MemTrivializationAtlas [FiberBundle F E] (e : Trivialization F (π F E)) : Prop where out : e ∈ trivializationAtlas F E #align mem_trivialization_atlas MemTrivializationAtlas diff --git a/Mathlib/Topology/Maps.lean b/Mathlib/Topology/Maps.lean index 4eb13edccc84d..8929f76e94585 100644 --- a/Mathlib/Topology/Maps.lean +++ b/Mathlib/Topology/Maps.lean @@ -56,7 +56,7 @@ section Inducing /-- A function `f : α → β` between topological spaces is inducing if the topology on `α` is induced by the topology on `β` through `f`, meaning that a set `s : Set α` is open iff it is the preimage under `f` of some open set `t : Set β`. -/ -@[mk_iff inducing_iff] +@[mk_iff] structure Inducing [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : α → β) : Prop where /-- The topology on the domain is equal to the induced topology. -/ induced : tα = tβ.induced f @@ -187,7 +187,7 @@ section Embedding /-- A function between topological spaces is an embedding if it is injective, and for all `s : Set α`, `s` is open iff it is the preimage of an open set. -/ -@[mk_iff embedding_iff] +@[mk_iff] structure Embedding [TopologicalSpace α] [TopologicalSpace β] (f : α → β) extends Inducing f : Prop where /-- A topological embedding is injective. -/ @@ -571,7 +571,7 @@ section OpenEmbedding variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] /-- An open embedding is an embedding with open image. -/ -@[mk_iff openEmbedding_iff] +@[mk_iff] structure OpenEmbedding (f : α → β) extends Embedding f : Prop where /-- The range of an open embedding is an open set. -/ open_range : IsOpen <| range f @@ -677,7 +677,7 @@ section ClosedEmbedding variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] /-- A closed embedding is an embedding with closed image. -/ -@[mk_iff closedEmbedding_iff] +@[mk_iff] structure ClosedEmbedding (f : α → β) extends Embedding f : Prop where /-- The range of a closed embedding is a closed set. -/ closed_range : IsClosed <| range f diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean index b2af7c38c7dc0..9bc598546cb29 100644 --- a/Mathlib/Topology/NoetherianSpace.lean +++ b/Mathlib/Topology/NoetherianSpace.lean @@ -45,7 +45,7 @@ variable (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] namespace TopologicalSpace /-- Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC. -/ -@[mk_iff noetherianSpace_iff] +@[mk_iff] class NoetherianSpace : Prop where wellFounded_opens : WellFounded ((· > ·) : Opens α → Opens α → Prop) #align topological_space.noetherian_space TopologicalSpace.NoetherianSpace diff --git a/Mathlib/Topology/QuasiSeparated.lean b/Mathlib/Topology/QuasiSeparated.lean index 8394b101eeca5..467f3dad7a4d1 100644 --- a/Mathlib/Topology/QuasiSeparated.lean +++ b/Mathlib/Topology/QuasiSeparated.lean @@ -43,7 +43,6 @@ def IsQuasiSeparated (s : Set α) : Prop := /-- A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact. -/ --- Porting note: mk_iff currently generates `QuasiSeparatedSpace_iff`. Undesirable capitalization? @[mk_iff] class QuasiSeparatedSpace (α : Type*) [TopologicalSpace α] : Prop where /-- The intersection of two open compact subsets of a quasi-separated space is compact.-/ @@ -53,7 +52,7 @@ class QuasiSeparatedSpace (α : Type*) [TopologicalSpace α] : Prop where theorem isQuasiSeparated_univ_iff {α : Type*} [TopologicalSpace α] : IsQuasiSeparated (Set.univ : Set α) ↔ QuasiSeparatedSpace α := by - rw [QuasiSeparatedSpace_iff] + rw [quasiSeparatedSpace_iff] simp [IsQuasiSeparated] #align is_quasi_separated_univ_iff isQuasiSeparated_univ_iff diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 66319310d70d6..f48b19e899032 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -916,7 +916,7 @@ theorem TopologicalSpace.subset_trans {s t : Set X} (ts : t ⊆ s) : /-- A T₂ space, also known as a Hausdorff space, is one in which for every `x ≠ y` there exists disjoint open sets around `x` and `y`. This is the most widely used of the separation axioms. -/ -@[mk_iff t2Space_iff] +@[mk_iff] class T2Space (X : Type u) [TopologicalSpace X] : Prop where /-- Every two points in a Hausdorff space admit disjoint open neighbourhoods. -/ t2 : Pairwise fun x y => ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v @@ -1568,7 +1568,7 @@ section RegularSpace /-- A topological space is called a *regular space* if for any closed set `s` and `a ∉ s`, there exist disjoint open sets `U ⊇ s` and `V ∋ a`. We formulate this condition in terms of `Disjoint`ness of filters `𝓝ˢ s` and `𝓝 a`. -/ -@[mk_iff regularSpace_iff] +@[mk_iff] class RegularSpace (X : Type u) [TopologicalSpace X] : Prop where /-- If `a` is a point that does not belong to a closed set `s`, then `a` and `s` admit disjoint neighborhoods. -/ diff --git a/Mathlib/Topology/Sequences.lean b/Mathlib/Topology/Sequences.lean index 89c87c6a4a56c..ed829d43e719e 100644 --- a/Mathlib/Topology/Sequences.lean +++ b/Mathlib/Topology/Sequences.lean @@ -255,7 +255,7 @@ def IsSeqCompact (s : Set X) := /-- A space `X` is sequentially compact if every sequence in `X` has a converging subsequence. -/ -@[mk_iff seqCompactSpace_iff] +@[mk_iff] class SeqCompactSpace (X : Type*) [TopologicalSpace X] : Prop where seq_compact_univ : IsSeqCompact (univ : Set X) #align seq_compact_space SeqCompactSpace diff --git a/Mathlib/Topology/Sober.lean b/Mathlib/Topology/Sober.lean index db367bd092239..efc29ef2d7623 100644 --- a/Mathlib/Topology/Sober.lean +++ b/Mathlib/Topology/Sober.lean @@ -116,7 +116,7 @@ end genericPoint section Sober /-- A space is sober if every irreducible closed subset has a generic point. -/ -@[mk_iff quasiSober_iff] +@[mk_iff] class QuasiSober (α : Type*) [TopologicalSpace α] : Prop where sober : ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S #align quasi_sober QuasiSober diff --git a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean index 71243a4599240..98ed716fff993 100644 --- a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean +++ b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean @@ -30,7 +30,7 @@ variable {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpa /-- A map `f : α → β` between uniform spaces is called *uniform inducing* if the uniformity filter on `α` is the pullback of the uniformity filter on `β` under `Prod.map f f`. If `α` is a separated space, then this implies that `f` is injective, hence it is a `UniformEmbedding`. -/ -@[mk_iff uniformInducing_iff] +@[mk_iff] structure UniformInducing (f : α → β) : Prop where /-- The uniformity filter on the domain is the pullback of the uniformity filter on the codomain under `Prod.map f f`. -/ @@ -131,7 +131,7 @@ protected theorem UniformInducing.injective [T0Space α] {f : α → β} (h : Un /-- A map `f : α → β` between uniform spaces is a *uniform embedding* if it is uniform inducing and injective. If `α` is a separated space, then the latter assumption follows from the former. -/ -@[mk_iff uniformEmbedding_iff] +@[mk_iff] structure UniformEmbedding (f : α → β) extends UniformInducing f : Prop where /-- A uniform embedding is injective. -/ inj : Function.Injective f diff --git a/test/MkIffOfInductive.lean b/test/MkIffOfInductive.lean index fee05d654b82c..fe6972aa3ca46 100644 --- a/test/MkIffOfInductive.lean +++ b/test/MkIffOfInductive.lean @@ -79,4 +79,4 @@ inductive ReflTransGen {α : Type _} (r : α → α → Prop) (a : α) : α → example {α : Type} (r: α → α → Prop) (a c : α) : ReflTransGen r a c ↔ c = a ∨ ∃ b : α, ReflTransGen r a b ∧ r b c := - ReflTransGen_iff r a c + reflTransGen_iff r a c