chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep

Counterexamples/DirectSumIsInternal.lean

@@ -12,7 +12,7 @@ import Mathlib.Tactic.FinCases
 # Not all complementary decompositions of a module over a semiring make up a direct sum
 
 This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
-implies as a collection they are `CompleteLattice.Independent` and that they span all of `ℤ`, they
+implies as a collection they are `iSupIndep` and that they span all of `ℤ`, they
 do not form a decomposition into a direct sum.
 
 This file demonstrates why `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top` must
@@ -57,9 +57,9 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
     · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
     · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 
-def withSign.independent : CompleteLattice.Independent withSign := by
+def withSign.independent : iSupIndep withSign := by
   apply
-    (CompleteLattice.independent_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
+    (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i
   fin_cases i <;> simp
 

Mathlib/Algebra/DirectSum/Internal.lean

@@ -28,7 +28,7 @@ to represent this case, `(h : DirectSum.IsInternal A) [SetLike.GradedMonoid A]`
 needed. In the future there will likely be a data-carrying, constructive, typeclass version of
 `DirectSum.IsInternal` for providing an explicit decomposition function.
 
-When `CompleteLattice.Independent (Set.range A)` (a weaker condition than
+When `iSupIndep (Set.range A)` (a weaker condition than
 `DirectSum.IsInternal A`), these provide a grading of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
 `DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)`.

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -82,8 +82,8 @@ lemma trace_eq_zero_of_mapsTo_ne (h : IsInternal N) [IsNoetherian R M]
     (σ : ι → ι) (hσ : ∀ i, σ i ≠ i) {f : Module.End R M}
     (hf : ∀ i, MapsTo f (N i) (N <| σ i)) :
     trace R M f = 0 := by
-  have hN : {i | N i ≠ ⊥}.Finite := CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent
-    h.submodule_independent
+  have hN : {i | N i ≠ ⊥}.Finite := CompleteLattice.WellFoundedGT.finite_ne_bot_of_iSupIndep
+    h.iSupIndep
   let s := hN.toFinset
   let κ := fun i ↦ Module.Free.ChooseBasisIndex R (N i)
   let b : (i : s) → Basis (κ i) R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)
@@ -112,7 +112,7 @@ lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
     have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
       f.independent_maxGenEigenspace hf
     have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
-      CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent f.independent_maxGenEigenspace
+      CompleteLattice.WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
     simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
   intro μ
   replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
@@ -136,14 +136,14 @@ Note that it is important the statement gives the user definitional control over
 _type_ of the term `trace R p (f.restrict hp')` depends on `p`. -/
 lemma trace_eq_sum_trace_restrict_of_eq_biSup
     [∀ i, Module.Finite R (N i)] [∀ i, Module.Free R (N i)]
-    (s : Finset ι) (h : CompleteLattice.Independent <| fun i : s ↦ N i)
+    (s : Finset ι) (h : iSupIndep <| fun i : s ↦ N i)
     {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i))
     (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
     (hp' : MapsTo f p p := hp ▸ mapsTo_biSup_of_mapsTo (s : Set ι) hf) :
     trace R p (f.restrict hp') = ∑ i ∈ s, trace R (N i) (f.restrict (hf i)) := by
   classical
   let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
-  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_independent (s : Set ι) h
+  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
   have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
   let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
   have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm

Mathlib/Algebra/DirectSum/Module.lean

@@ -319,8 +319,8 @@ theorem IsInternal.submodule_iSup_eq_top (h : IsInternal A) : iSup A = ⊤ := by
   exact Function.Bijective.surjective h
 
 /-- If a direct sum of submodules is internal then the submodules are independent. -/
-theorem IsInternal.submodule_independent (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_lsum_injective _ h.injective
+protected theorem IsInternal.iSupIndep (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_lsum_injective _ h.injective
 
 /-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
 components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
@@ -374,7 +374,7 @@ the two submodules are complementary. Over a `Ring R`, this is true as an iff, a
 `DirectSum.isInternal_submodule_iff_isCompl`. -/
 theorem IsInternal.isCompl {A : ι → Submodule R M} {i j : ι} (hij : i ≠ j)
     (h : (Set.univ : Set ι) = {i, j}) (hi : IsInternal A) : IsCompl (A i) (A j) :=
-  ⟨hi.submodule_independent.pairwiseDisjoint hij,
+  ⟨hi.iSupIndep.pairwiseDisjoint hij,
     codisjoint_iff.mpr <| Eq.symm <| hi.submodule_iSup_eq_top.symm.trans <| by
       rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]⟩
 
@@ -387,19 +387,19 @@ variable {ι : Type v} [dec_ι : DecidableEq ι]
 variable {M : Type*} [AddCommGroup M] [Module R M]
 
 /-- Note that this is not generally true for `[Semiring R]`; see
-`CompleteLattice.Independent.dfinsupp_lsum_injective` for details. -/
+`iSupIndep.dfinsupp_lsum_injective` for details. -/
 theorem isInternal_submodule_of_independent_of_iSup_eq_top {A : ι → Submodule R M}
-    (hi : CompleteLattice.Independent A) (hs : iSup A = ⊤) : IsInternal A :=
+    (hi : iSupIndep A) (hs : iSup A = ⊤) : IsInternal A :=
   ⟨hi.dfinsupp_lsum_injective,
     -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify value of `f`
     (LinearMap.range_eq_top (f := DFinsupp.lsum _ _)).1 <|
       (Submodule.iSup_eq_range_dfinsupp_lsum _).symm.trans hs⟩
 
 /-- `iff` version of `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top`,
-`DirectSum.IsInternal.submodule_independent`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
+`DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
 theorem isInternal_submodule_iff_independent_and_iSup_eq_top (A : ι → Submodule R M) :
-    IsInternal A ↔ CompleteLattice.Independent A ∧ iSup A = ⊤ :=
-  ⟨fun i ↦ ⟨i.submodule_independent, i.submodule_iSup_eq_top⟩,
+    IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤ :=
+  ⟨fun i ↦ ⟨i.iSupIndep, i.submodule_iSup_eq_top⟩,
     And.rec isInternal_submodule_of_independent_of_iSup_eq_top⟩
 
 /-- If a collection of submodules has just two indices, `i` and `j`, then
@@ -408,25 +408,25 @@ theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (
     (h : (Set.univ : Set ι) = {i, j}) : IsInternal A ↔ IsCompl (A i) (A j) := by
   have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
   rw [isInternal_submodule_iff_independent_and_iSup_eq_top, iSup, ← Set.image_univ, h,
-    Set.image_insert_eq, Set.image_singleton, sSup_pair, CompleteLattice.independent_pair hij this]
+    Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]
   exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
 
 @[simp]
 theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
     IsInternal (fun i : {i // A i ≠ ⊥} ↦ A i) ↔ IsInternal A := by
   simp only [isInternal_submodule_iff_independent_and_iSup_eq_top]
-  exact Iff.and CompleteLattice.independent_ne_bot_iff_independent <| by simp
+  exact Iff.and iSupIndep_ne_bot_iff_independent <| by simp
 
-lemma isInternal_biSup_submodule_of_independent {A : ι → Submodule R M} (s : Set ι)
-    (h : CompleteLattice.Independent <| fun i : s ↦ A i) :
+lemma isInternal_biSup_submodule_of_iSupIndep {A : ι → Submodule R M} (s : Set ι)
+    (h : iSupIndep <| fun i : s ↦ A i) :
     IsInternal <| fun (i : s) ↦ (A i).comap (⨆ i ∈ s, A i).subtype := by
   refine (isInternal_submodule_iff_independent_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
   let p := ⨆ i ∈ s, A i
   have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
   let e : Submodule R p ≃o Set.Iic p := p.mapIic
   suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
-    rw [← CompleteLattice.independent_map_orderIso_iff e, this]
-    exact CompleteLattice.independent_of_independent_coe_Iic_comp h
+    rw [← iSupIndep_map_orderIso_iff e, this]
+    exact .of_coe_Iic_comp h
   ext i m
   change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
   rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
@@ -435,12 +435,12 @@ lemma isInternal_biSup_submodule_of_independent {A : ι → Submodule R M} (s :
 
 
 theorem IsInternal.addSubmonoid_independent {M : Type*} [AddCommMonoid M] {A : ι → AddSubmonoid M}
-    (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_sumAddHom_injective _ h.injective
+    (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_sumAddHom_injective _ h.injective
 
 theorem IsInternal.addSubgroup_independent {M : Type*} [AddCommGroup M] {A : ι → AddSubgroup M}
-    (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_sumAddHom_injective' _ h.injective
+    (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_sumAddHom_injective' _ h.injective
 
 end Ring
 

Mathlib/Algebra/DirectSum/Ring.lean

@@ -63,7 +63,7 @@ instances for:
 * `A : ι → Submodule S`:
   `DirectSum.GSemiring.ofSubmodules`, `DirectSum.GCommSemiring.ofSubmodules`.
 
-If `CompleteLattice.independent (Set.range A)`, these provide a gradation of `⨆ i, A i`, and the
+If `iSupIndep (Set.range A)`, these provide a gradation of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
 `DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)`.
 

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -292,7 +292,7 @@ instance (priority := 100) IsSimple.instIsSemisimple [IsSimple R L] :
     IsSemisimple R L := by
   constructor
   · simp
-  · simpa using CompleteLattice.setIndependent_singleton _
+  · simpa using sSupIndep_singleton _
   · intro I hI₁ hI₂
     apply IsSimple.non_abelian (R := R) (L := L)
     rw [IsSimple.isAtom_iff_eq_top] at hI₁

Mathlib/Algebra/Lie/Semisimple/Defs.lean

@@ -72,7 +72,7 @@ class IsSemisimple : Prop where
   /-- In a semisimple Lie algebra, the supremum of the atoms is the whole Lie algebra. -/
   sSup_atoms_eq_top : sSup {I : LieIdeal R L | IsAtom I} = ⊤
   /-- In a semisimple Lie algebra, the atoms are independent. -/
-  setIndependent_isAtom : CompleteLattice.SetIndependent {I : LieIdeal R L | IsAtom I}
+  setIndependent_isAtom : sSupIndep {I : LieIdeal R L | IsAtom I}
   /-- In a semisimple Lie algebra, the atoms are non-abelian. -/
   non_abelian_of_isAtom : ∀ I : LieIdeal R L, IsAtom I → ¬ IsLieAbelian I
 

Mathlib/Algebra/Lie/Submodule.lean

@@ -515,8 +515,8 @@ theorem isCompl_iff_coe_toSubmodule :
   simp only [isCompl_iff, disjoint_iff_coe_toSubmodule, codisjoint_iff_coe_toSubmodule]
 
 theorem independent_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
-    CompleteLattice.Independent N ↔ CompleteLattice.Independent fun i ↦ (N i : Submodule R M) := by
-  simp [CompleteLattice.independent_def, disjoint_iff_coe_toSubmodule]
+    iSupIndep N ↔ iSupIndep fun i ↦ (N i : Submodule R M) := by
+  simp [iSupIndep_def, disjoint_iff_coe_toSubmodule]
 
 theorem iSup_eq_top_iff_coe_toSubmodule {ι : Sort*} {N : ι → LieSubmodule R L M} :
     ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ := by

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -668,30 +668,30 @@ lemma injOn_genWeightSpace [NoZeroSMulDivisors R M] :
 
 See also `LieModule.independent_genWeightSpace'`. -/
 lemma independent_genWeightSpace [NoZeroSMulDivisors R M] :
-    CompleteLattice.Independent fun χ : L → R ↦ genWeightSpace M χ := by
+    iSupIndep fun χ : L → R ↦ genWeightSpace M χ := by
   simp only [LieSubmodule.independent_iff_coe_toSubmodule, genWeightSpace,
     LieSubmodule.iInf_coe_toSubmodule]
   exact Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
     (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)
 
 lemma independent_genWeightSpace' [NoZeroSMulDivisors R M] :
-    CompleteLattice.Independent fun χ : Weight R L M ↦ genWeightSpace M χ :=
+    iSupIndep fun χ : Weight R L M ↦ genWeightSpace M χ :=
   (independent_genWeightSpace R L M).comp <|
     Subtype.val_injective.comp (Weight.equivSetOf R L M).injective
 
 lemma independent_genWeightSpaceOf [NoZeroSMulDivisors R M] (x : L) :
-    CompleteLattice.Independent fun (χ : R) ↦ genWeightSpaceOf M χ x := by
+    iSupIndep fun (χ : R) ↦ genWeightSpaceOf M χ x := by
   rw [LieSubmodule.independent_iff_coe_toSubmodule]
   dsimp [genWeightSpaceOf]
   exact (toEnd R L M x).independent_genEigenspace _
 
 lemma finite_genWeightSpaceOf_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
     {χ : R | genWeightSpaceOf M χ x ≠ ⊥}.Finite :=
-  CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent (independent_genWeightSpaceOf R L M x)
+  CompleteLattice.WellFoundedGT.finite_ne_bot_of_iSupIndep (independent_genWeightSpaceOf R L M x)
 
 lemma finite_genWeightSpace_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] :
     {χ : L → R | genWeightSpace M χ ≠ ⊥}.Finite :=
-  CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent (independent_genWeightSpace R L M)
+  CompleteLattice.WellFoundedGT.finite_ne_bot_of_iSupIndep (independent_genWeightSpace R L M)
 
 instance Weight.instFinite [NoZeroSMulDivisors R M] [IsNoetherian R M] :
     Finite (Weight R L M) := by

Mathlib/Algebra/Lie/Weights/Chain.lean

@@ -204,7 +204,7 @@ lemma exists_forall_mem_corootSpace_smul_add_eq_zero
     exact finrank_pos
   refine ⟨a, b, Int.ofNat_pos.mpr hb, fun x hx ↦ ?_⟩
   let N : ℤ → Submodule R M := fun k ↦ genWeightSpace M (k • α + χ)
-  have h₁ : CompleteLattice.Independent fun (i : Finset.Ioo p q) ↦ N i := by
+  have h₁ : iSupIndep fun (i : Finset.Ioo p q) ↦ N i := by
     rw [← LieSubmodule.independent_iff_coe_toSubmodule]
     refine (independent_genWeightSpace R H M).comp fun i j hij ↦ ?_
     exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij

Mathlib/Algebra/Module/Torsion.lean

@@ -96,13 +96,13 @@ theorem torsionOf_eq_bot_iff_of_noZeroSMulDivisors [Nontrivial R] [NoZeroSMulDiv
   · rw [mem_torsionOf_iff, smul_eq_zero] at hr
     tauto
 
-/-- See also `CompleteLattice.Independent.linearIndependent` which provides the same conclusion
+/-- See also `iSupIndep.linearIndependent` which provides the same conclusion
 but requires the stronger hypothesis `NoZeroSMulDivisors R M`. -/
-theorem CompleteLattice.Independent.linear_independent' {ι R M : Type*} {v : ι → M} [Ring R]
-    [AddCommGroup M] [Module R M] (hv : CompleteLattice.Independent fun i => R ∙ v i)
+theorem iSupIndep.linear_independent' {ι R M : Type*} {v : ι → M} [Ring R]
+    [AddCommGroup M] [Module R M] (hv : iSupIndep fun i => R ∙ v i)
     (h_ne_zero : ∀ i, Ideal.torsionOf R M (v i) = ⊥) : LinearIndependent R v := by
   refine linearIndependent_iff_not_smul_mem_span.mpr fun i r hi => ?_
-  replace hv := CompleteLattice.independent_def.mp hv i
+  replace hv := iSupIndep_def.mp hv i
   simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv
   have : r • v i ∈ (⊥ : Submodule R M) := by
     rw [← hv, Submodule.mem_inf]
@@ -444,7 +444,7 @@ theorem torsionBySet_isInternal {p : ι → Ideal R}
     (hM : Module.IsTorsionBySet R M (⨅ i ∈ S, p i : Ideal R)) :
     DirectSum.IsInternal fun i : S => torsionBySet R M <| p i :=
   DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
-    (CompleteLattice.independent_iff_supIndep.mpr <| supIndep_torsionBySet_ideal hp)
+    (iSupIndep_iff_supIndep.mpr <| supIndep_torsionBySet_ideal hp)
     (by
       apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
       -- Porting note: times out if we change apply below to <|

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -2197,9 +2197,9 @@ elements each from a different subspace in the family is linearly independent. I
 pairwise intersections of elements of the family are 0. -/
 theorem OrthogonalFamily.independent {V : ι → Submodule 𝕜 E}
     (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) :
-    CompleteLattice.Independent V := by
+    iSupIndep V := by
   classical
-  apply CompleteLattice.independent_of_dfinsupp_lsum_injective
+  apply iSupIndep_of_dfinsupp_lsum_injective
   refine LinearMap.ker_eq_bot.mp ?_
   rw [Submodule.eq_bot_iff]
   intro v hv

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -49,7 +49,7 @@ generalizes (one direction of) `Subgroup.disjoint_iff_mul_eq_one`. -/
 @[to_additive "`Finset.noncommSum` is “injective” in `f` if `f` maps into independent subgroups.
 This generalizes (one direction of) `AddSubgroup.disjoint_iff_add_eq_zero`. "]
 theorem eq_one_of_noncommProd_eq_one_of_independent {ι : Type*} (s : Finset ι) (f : ι → G) (comm)
-    (K : ι → Subgroup G) (hind : CompleteLattice.Independent K) (hmem : ∀ x ∈ s, f x ∈ K x)
+    (K : ι → Subgroup G) (hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x)
     (heq1 : s.noncommProd f comm = 1) : ∀ i ∈ s, f i = 1 := by
   classical
     revert heq1
@@ -202,7 +202,7 @@ theorem noncommPiCoprod_range [Fintype ι]
 @[to_additive]
 theorem injective_noncommPiCoprod_of_independent [Fintype ι]
     {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)}
-    (hind : CompleteLattice.Independent fun i => (ϕ i).range)
+    (hind : iSupIndep fun i => (ϕ i).range)
     (hinj : ∀ i, Function.Injective (ϕ i)) : Function.Injective (noncommPiCoprod ϕ hcomm) := by
   classical
     apply (MonoidHom.ker_eq_bot_iff _).mp
@@ -220,7 +220,7 @@ theorem independent_range_of_coprime_order
     (hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y))
     [Finite ι] [∀ i, Fintype (H i)]
     (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
-    CompleteLattice.Independent fun i => (ϕ i).range := by
+    iSupIndep fun i => (ϕ i).range := by
   cases nonempty_fintype ι
   letI := Classical.decEq ι
   rintro i
@@ -279,7 +279,7 @@ theorem independent_of_coprime_order
     (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
     [Finite ι] [∀ i, Fintype (H i)]
     (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
-    CompleteLattice.Independent H := by
+    iSupIndep H := by
   simpa using
     MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
       (commute_subtype_of_commute hcomm) hcoprime
@@ -308,7 +308,7 @@ theorem noncommPiCoprod_range
 @[to_additive]
 theorem injective_noncommPiCoprod_of_independent
     {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}
-    (hind : CompleteLattice.Independent H) :
+    (hind : iSupIndep H) :
     Function.Injective (noncommPiCoprod hcomm) := by
   apply MonoidHom.injective_noncommPiCoprod_of_independent
   · simpa using hind