-- Mathlib/GroupTheory/NoncommPiCoprod.lean
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))) :
    iSupIndep fun i => (ϕ i).range

Proof state:
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute ((ϕ ↑i✝) x) ((ϕ ↑j✝) y)

Tactic:
apply hcomm

Result:
case intro.intro.hcomm.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝

Proof state:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = 1

Tactic:
rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]

Result:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (a : ι) (b : a ≠ i), (Fintype.card (H ↑⟨a, b⟩)).Coprime (Fintype.card (H i))

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
⊢ (fun i => (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i => (ϕ i).range) j ≤ ⊥

Tactic:
rintro f ⟨hxi, hxp⟩

Result:
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ ↑((fun i => (ϕ i).range) i).toSubmonoid
hxp : f ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i => (ϕ i).range) j).toSubmonoid
⊢ f ∈ ⊥

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
⊢ iSupIndep fun i => (ϕ i).range

Tactic:
letI := Classical.decEq ι

Result:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ iSupIndep fun i => (ϕ i).range

Proof state:
case intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f
⊢ f ∈ ⊥

Tactic:
obtain ⟨g', hg'f⟩ := hxi

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
⊢ f ∈ ⊥

Proof state:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
j : ι
h : j ≠ i
⊢ (Fintype.card (H ↑⟨j, h⟩)).Coprime (Fintype.card (H i))

Tactic:
exact hcoprime h

Result:
no goals