case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
⊢ CompleteLattice.Independent fun i => range (ϕ i)
cases nonempty_fintype ι
case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ Disjoint ((fun i => range (ϕ i)) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j)
case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
rintro i
case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ ((fun i => range (ϕ i)) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j) ≤ ⊥
case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ Disjoint ((fun i => range (ϕ i)) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j)
rw [disjoint_iff_inf_le]
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ ↑((fun i => range (ϕ i)) i).toSubmonoid
hxp : f ∈ ↑(⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j).toSubmonoid
⊢ f ∈ ⊥
case intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ ((fun i => range (ϕ i)) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j) ≤ ⊥
rintro f ⟨hxi, hxp⟩
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (j : ι) (_ : ¬j = i), range (ϕ j))
⊢ f ∈ ⊥
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ ↑((fun i => range (ϕ i)) i).toSubmonoid
hxp : f ∈ ↑(⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j).toSubmonoid
⊢ f ∈ ⊥
dsimp at hxi hxp
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp : f ∈ ↑(range (noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm))
⊢ f ∈ ⊥

case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (j : ι) (_ : ¬j = i), range (ϕ j))
⊢ f ∈ ⊥
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)

case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp : f ∈ ↑(range (noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm))
⊢ f ∈ ⊥
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp : f ∈ ↑(range (noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm))
⊢ f ∈ ⊥

case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
rotate_left
case intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
⊢ f ∈ ⊥
case intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp :
  f ∈
    ↑(range
        (noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y))))
⊢ f ∈ ⊥
cases' hxp with g hgf
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ f ∈ ⊥
case intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
⊢ f ∈ ⊥
cases' hxi with g' hg'f
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ f ∈ ⊥
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ f ∈ ⊥
have hxi : orderOf f ∣ Fintype.card (H i) := by
  rw [← hg'f]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ f ∈ ⊥
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ f ∈ ⊥
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) := by
  rw [← hgf, ← Fintype.card_pi]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ f = 1
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ f ∈ ⊥
change f = 1
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ orderOf f ∣ 1
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ f = 1
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ orderOf f ∣ 1
case intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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)
⊢ orderOf f ∣ 1
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ orderOf f ∣ 1
use c
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c
rw [← hc]
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = 1
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
symm
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.coprime (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = 1
rw [← Nat.coprime_iff_gcd_eq_one]
case intro.intro.intro.intro.intro.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (i_1 : { j // j ≠ i }), i_1 ∈ Finset.univ → Nat.coprime (Fintype.card (H ↑i_1)) (Fintype.card (H i))
case intro.intro.intro.intro.intro
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.coprime (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
apply Nat.coprime_prod_left
case intro.intro.intro.intro.intro.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ Nat.coprime (Fintype.card (H ↑j)) (Fintype.card (H i))
case intro.intro.intro.intro.intro.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (i_1 : { j // j ≠ i }), i_1 ∈ Finset.univ → Nat.coprime (Fintype.card (H ↑i_1)) (Fintype.card (H i))
intro j _
case intro.intro.intro.intro.intro.a.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ ↑j ≠ i
case intro.intro.intro.intro.intro.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ Nat.coprime (Fintype.card (H ↑j)) (Fintype.card (H i))
apply hcoprime
no goals
case intro.intro.intro.intro.intro.a.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      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 : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ ↑j ≠ i
exact j.2
case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute (↑(ϕ ↑i✝) x) (↑(ϕ ↑j✝) y)
case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
intro _ _ hj
case intro.intro.hcomm.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝
case intro.intro.hcomm
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute (↑(ϕ ↑i✝) x) (↑(ϕ ↑j✝) y)
apply hcomm
no goals
case intro.intro.hcomm.a
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝
exact hj ∘ Subtype.ext
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf (↑(ϕ i) g') ∣ Fintype.card (H i)
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf f ∣ Fintype.card (H i)
rw [← hg'f]
no goals
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf (↑(ϕ i) g') ∣ Fintype.card (H i)
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf
      (↑(noncommPiCoprod (fun x => ϕ ↑x)
            (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
        g) ∣
    Fintype.card ((a : { j // j ≠ i }) → H ↑a)
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
rw [← hgf, ← Fintype.card_pi]
no goals
G : Type u_3
inst✝³ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_2
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf
      (↑(noncommPiCoprod (fun x => ϕ ↑x)
            (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
        g) ∣
    Fintype.card ((a : { j // j ≠ i }) → H ↑a)
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ