refactor: make Set into a one-field structure

Author: YaelDillies

Mathlib/Algebra/DirectSum/Module.lean

@@ -140,7 +140,7 @@ theorem linearMap_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄
 /-- The inclusion of a subset of the direct summands
 into a larger subset of the direct summands, as a linear map. -/
 def lsetToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, M i) →ₗ[R] ⨁ i : T, M i :=
-  toModule R _ _ fun i ↦ lof R T (fun i : Subtype T ↦ M i) ⟨i, H i.prop⟩
+  toModule R _ _ fun i ↦ lof R T (fun i : T ↦ M i) ⟨i, H i.prop⟩
 
 variable (ι M)
 

Mathlib/Algebra/FreeAlgebra.lean

@@ -548,7 +548,7 @@ theorem induction {motive : FreeAlgebra R X → Prop}
     (a : FreeAlgebra R X) : motive a := by
   -- the arguments are enough to construct a subalgebra, and a mapping into it from X
   let s : Subalgebra R (FreeAlgebra R X) :=
-    { carrier := motive
+    { carrier := {x | motive x}
       mul_mem' := mul _ _
       add_mem' := add _ _
       algebraMap_mem' := grade0 }

Mathlib/Algebra/Group/Action/Equidecomp.lean

@@ -163,7 +163,7 @@ open scoped Classical in
 theorem IsDecompOn.comp {g f : X → X} {B A : Set X} {T S : Finset G}
     (hg : IsDecompOn g B T) (hf : IsDecompOn f A S) (h : MapsTo f A B) :
     IsDecompOn (g ∘ f) A (T * S) := by
-  rw [left_eq_inter.mpr h]
+  rw [left_eq_inter.mpr h.subset_preimage]
   exact hg.comp' hf
 
 /-- The composition of two equidecompositions as an equidecomposition. -/

Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

@@ -32,8 +32,7 @@ def IsMulIndecomposable (v : ι → M) (s : Set ι) (i : ι) : Prop :=
 
 @[to_additive]
 protected lemma IsMulIndecomposable.subset (v : ι → M) (s : Set ι) :
-    {i | IsMulIndecomposable v s i} ⊆ s := by
-  aesop
+    {i | IsMulIndecomposable v s i} ⊆ s := fun _ hi ↦ hi.1
 
 @[to_additive]
 lemma isMulIndecomposable_id_univ [Subsingleton Mˣ] {x : M} (hx : x ≠ 1) :

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -55,7 +55,7 @@ lemma mem_nonZeroDivisorsLeft_iff : x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, x
 
 lemma notMem_nonZeroDivisorsLeft_iff :
     x ∉ nonZeroDivisorsLeft M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty := by
-  simpa [mem_nonZeroDivisorsLeft_iff] using! Set.nonempty_def.symm
+  simp [mem_nonZeroDivisorsLeft_iff, Set.Nonempty]
 
 /-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
 `Submonoid`. -/
@@ -69,7 +69,7 @@ lemma mem_nonZeroDivisorsRight_iff : x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y,
 
 lemma notMem_nonZeroDivisorsRight_iff :
     x ∉ nonZeroDivisorsRight M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty := by
-  simpa [mem_nonZeroDivisorsRight_iff] using! Set.nonempty_def.symm
+  simp [mem_nonZeroDivisorsRight_iff, Set.Nonempty]
 
 lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
     nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -171,7 +171,7 @@ lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M
   obtain ⟨t, ht⟩ := hl'
   have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
     LinearMap.range_eq_top.mp
-      (by rw [range_linearCombination, Subtype.range_val, ← hs])
+      (by rw [range_linearCombination, Subtype.range_coe_subtype, ← hs]; rfl)
   apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
     (hl.comp H)
   choose σ hσ using (show _ from H)
@@ -188,7 +188,7 @@ lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
   obtain ⟨s, hs, hs'⟩ := h
   have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
     LinearMap.range_eq_top.mp
-      (by rw [range_linearCombination, Subtype.range_val, ← hs])
+      (by rw [range_linearCombination, Subtype.range_coe_subtype, ← hs]; rfl)
   obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
     choose f hf using show _ from hl
     exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
@@ -221,7 +221,7 @@ lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
   let π := Finsupp.linearCombination R ((↑) : s → M)
   have H : Function.Surjective π :=
     LinearMap.range_eq_top.mp
-      (by rw [range_linearCombination, Subtype.range_val, ← hs])
+      (by rw [range_linearCombination, Subtype.range_coe_subtype, ← hs]; rfl)
   have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
     .of_fg <| Module.FinitePresentation.fg_ker _ (hl.comp H)
   let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)
@@ -365,7 +365,7 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
   let π := Finsupp.linearCombination R ((↑) : σ → M)
   have hπ : Function.Surjective π :=
     LinearMap.range_eq_top.mp
-      (by rw [range_linearCombination, Subtype.range_val, ← hσ])
+      (by rw [range_linearCombination, Subtype.range_coe_subtype, ← hσ]; rfl)
   classical
   choose s hs using IsLocalizedModule.surj S f
   let i : σ → N :=

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -399,7 +399,7 @@ theorem volume_real_fundamentalDomain [Fintype ι] [DecidableEq ι] (b : Basis 
 
 theorem fundamentalDomain_ae_parallelepiped [Fintype ι] [MeasurableSpace E] (μ : Measure E)
     [BorelSpace E] [Measure.IsAddHaarMeasure μ] :
-    fundamentalDomain b =ᵐ[μ] parallelepiped b := by
+    fundamentalDomain b =ᵐˢ[μ] parallelepiped b := by
   classical
   have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
   rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -52,7 +52,7 @@ abbrev gradeBy (f : M → ι) (i : ι) : Submodule R R[M] where
   zero_mem' m h := by cases h
   add_mem' {a b} ha hb m h := by
     classical exact (Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)
-  smul_mem' _ _ h := Set.Subset.trans Finsupp.support_smul h
+  smul_mem' _ _ h m hm := h m (Finsupp.support_smul hm)
 
 /-- The submodule corresponding to each grade. -/
 abbrev grade (m : M) : Submodule R R[M] :=
@@ -61,11 +61,11 @@ abbrev grade (m : M) : Submodule R R[M] :=
 theorem gradeBy_id : gradeBy R (id : M → M) = grade R := rfl
 
 theorem mem_gradeBy_iff (f : M → ι) (i : ι) (a : R[M]) :
-    a ∈ gradeBy R f i ↔ (a.coeff.support : Set M) ⊆ f ⁻¹' {i} := by rfl
+    a ∈ gradeBy R f i ↔ (a.coeff.support : Set M) ⊆ f ⁻¹' {i} :=
+  ⟨fun h m hm => h m hm, fun h _ hm => h hm⟩
 
 theorem mem_grade_iff (m : M) (a : R[M]) : a ∈ grade R m ↔ a.coeff.support ⊆ {m} := by
-  rw [← Finset.coe_subset, Finset.coe_singleton]
-  rfl
+  simp [← Finset.coe_subset]
 
 theorem mem_grade_iff' (m : M) (a : R[M]) :
     a ∈ grade R m ↔ a ∈ LinearMap.range (lsingle (R := R) m) := by

Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -259,6 +259,11 @@ theorem mk_mabs (a : M) : mk |a|ₘ = mk a :=
 instance [Subsingleton M] : Subsingleton (MulArchimedeanClass M) :=
   inferInstanceAs (Subsingleton (Antisymmetrization ..))
 
+-- Shortcut instance for computability
+@[to_additive]
+instance : PartialOrder (MulArchimedeanClass M) :=
+  inferInstanceAs <| PartialOrder (Antisymmetrization (MulArchimedeanOrder M) (· ≤ ·))
+
 @[to_additive]
 noncomputable
 instance : LinearOrder (MulArchimedeanClass M) :=

Mathlib/Algebra/Order/Ring/StandardPart.lean

@@ -460,13 +460,8 @@ theorem stdPart_eq_sInf (f : ℝ →+*o K) (x : K) : stdPart x = sInf {r | x < f
       exact hs.le.trans (f.monotone' hs'.le)
   · rw [stdPart_of_mk_ne_zero hx.ne]
     have hr {r} := hx.trans_le (mk_map_nonneg_of_archimedean f r)
-    obtain h | h := le_or_gt 0 x
-    · convert! Real.sInf_empty.symm
-      rw [Set.eq_empty_iff_forall_notMem]
-      exact fun r ↦ (lt_of_mk_lt_mk_of_nonneg hr h).not_gt
-    · convert! Real.sInf_univ.symm
-      rw [Set.eq_univ_iff_forall]
-      exact fun r ↦ lt_of_mk_lt_mk_of_nonpos hr h.le
+    obtain hx | hx := le_total 0 x <;>
+      simp [(lt_of_mk_lt_mk_of_nonneg hr _).not_gt, lt_of_mk_lt_mk_of_nonpos hr, *]
 
 theorem stdPart_eq_sSup (f : ℝ →+*o K) (x : K) : stdPart x = sSup {r | f r < x} := by
   rw [← neg_inj, ← stdPart_neg, stdPart_eq_sInf f, ← Real.sInf_neg]