no goals
G : Type u_2
inst✝² : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype { x // x ∈ H i }
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card { x // x ∈ H i }) (Fintype.card { x // x ∈ H j })
⊢ CompleteLattice.Independent H
simpa using
  MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
    (commute_subtype_of_commute hcomm) hcoprime