awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
intro :
  LE.le.{u_1} (α := Subgroup G)
    ((fun (i : ι) ↦ (ϕ i).range) i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (ϕ i).range) j) ⊥
⊢ Disjoint.{u_1} (α := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i)
    (⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (ϕ i).range) j)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (j : ι), ⨆ (_ : ¬j = i), (ϕ j).range) : Set G)
intro :
  ∀ (hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G))
    (hxp :
      f ∈
        (↑(range (G := (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι))
              (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
                (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯)) :
          Set G)),
    Membership.mem (γ := Subgroup G) ⊥ f
intro₁ :
  ∀ (hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)),
    Pairwise fun (i_1 j : { j : ι // ¬j = i }) ↦
      ∀ (x : H (↑i_1 : ι)) (y : H (↑j : ι)),
        Commute.{u_1} (S := G) ((ϕ (↑i_1 : ι) : (a : H (↑i_1 : ι)) → G) x : G)
          ((ϕ (↑j : ι) : (a : H (↑j : ι)) → G) y : G)
⊢ Membership.mem (γ := Subgroup G) ⊥ f

Tactic:
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp

Premises used: iSup_subtype', MonoidHom.noncommPiCoprod_range
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
i_1 : { j : ι // ¬j = i }
intro :
  ∀ ⦃j : { j : ι // ¬j = i }⦄,
    i_1 ≠ j →
      (fun (i_2 j : { j : ι // ¬j = i }) ↦
          ∀ (x : H (↑i_2 : ι)) (y : H (↑j : ι)),
            Commute.{u_1} (S := G) ((ϕ (↑i_2 : ι) : (a : H (↑i_2 : ι)) → G) x : G)
              ((ϕ (↑j : ι) : (a : H (↑j : ι)) → G) y : G))
        i_1 j
⊢ ∀ ⦃j : { j : ι // ¬j = i }⦄,
    i_1 ≠ j →
      (fun (i_2 j : { j : ι // ¬j = i }) ↦
          ∀ (x : H (↑i_2 : ι)) (y : H (↑j : ι)),
            Commute.{u_1} (S := G) ((ϕ (↑i_2 : ι) : (a : H (↑i_2 : ι)) → G) x : G)
              ((ϕ (↑j : ι) : (a : H (↑j : ι)) → G) y : G))
        i_1 j

Tactic:
_
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
i_1 j : { j : ι // ¬j = i }
hj : i_1 ≠ j
intro : (↑i_1 : ι) ≠ (↑j : ι)
⊢ ∀ (x : H (↑i_1 : ι)) (y : H (↑j : ι)),
    Commute.{u_1} (S := G) ((ϕ (↑i_1 : ι) : (a : H (↑i_1 : ι)) → G) x : G) ((ϕ (↑j : ι) : (a : H (↑j : ι)) → G) y : G)

Tactic:
apply hcomm
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
i_1 j : { j : ι // ¬j = i }
hj : i_1 ≠ j
⊢ (↑i_1 : ι) ≠ (↑j : ι)

Tactic:
hj ∘ Subtype.ext

Premises used: Function.comp, Not, Subtype.ext
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
i_1 j : { j : ι // ¬j = i }
hj : i_1 ≠ j
⊢ (↑i_1 : ι) ≠ (↑j : ι)

Tactic:
exact hj ∘ Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
hxp :
  f ∈
    (↑(range (G := (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι))
          (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
            (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯)) :
      Set G)
intro :
  ∀ (g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι))
    (hgf :
      (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
              (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯ :
            (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
          g =
        f),
    Membership.mem (γ := Subgroup G) ⊥ f
⊢ Membership.mem (γ := Subgroup G) ⊥ f

Tactic:
obtain ⟨g, hgf⟩ := hxp
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : Membership.mem (γ := Set G) (Set.range.{u_1, u_3 + 1} (ι := H i) (⇑(ϕ i) : (a : H i) → G)) f
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
intro : ∀ (g' : H i) (hg'f : (ϕ i : (a : H i) → G) g' = f), Membership.mem (γ := Subgroup G) ⊥ f
⊢ Membership.mem (γ := Subgroup G) ⊥ f

Tactic:
obtain ⟨g', hg'f⟩ := hxi
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
rw : orderOf.{u_1} (G := G) ((ϕ i : (a : H i) → G) g' : G) ∣ Fintype.card.{u_3} (H i)
⊢ orderOf f ∣ Fintype.card.{u_3} (H i)

Tactic:
rw [← hg'f]
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
⊢ orderOf.{u_1} (G := G) ((ϕ i : (a : H i) → G) g' : G) ∣ Fintype.card.{u_3} (H i)

Tactic:
(orderOf_map_dvd _ _).trans orderOf_dvd_card

Premises used: orderOf_map_dvd, orderOf_dvd_card, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
⊢ orderOf.{u_1} (G := G) ((ϕ i : (a : H i) → G) g' : G) ∣ Fintype.card.{u_3} (H i)

Tactic:
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card

Premises used: orderOf_map_dvd, orderOf_dvd_card, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
⊢ orderOf f ∣ Fintype.card.{u_3} (H i)

Tactic:
have hxi : orderOf f ∣ Fintype.card (H i) := by
    rw [← hg'f]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
rw :
  orderOf.{u_1} (G := G)
      ((noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
              (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯ :
            (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
          g :
        G) ∣
    Fintype.card ((i_1 : { j : ι // j ≠ i }) → H (↑i_1 : ι))
⊢ orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))

Tactic:
rw [← hgf, ← Fintype.card_pi]

Premises used: Fintype.card_pi
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
⊢ orderOf.{u_1} (G := G)
      ((noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
              (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯ :
            (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
          g :
        G) ∣
    Fintype.card ((i_1 : { j : ι // j ≠ i }) → H (↑i_1 : ι))

Tactic:
(orderOf_map_dvd _ _).trans orderOf_dvd_card

Premises used: orderOf_map_dvd, orderOf_dvd_card, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
⊢ orderOf.{u_1} (G := G)
      ((noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι))
              (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι)) ⋯ :
            (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
          g :
        G) ∣
    Fintype.card ((i_1 : { j : ι // j ≠ i }) → H (↑i_1 : ι))

Tactic:
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card

Premises used: orderOf_map_dvd, orderOf_dvd_card, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
⊢ orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))

Tactic:
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
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
intro : f = 1
⊢ Membership.mem (γ := Subgroup G) ⊥ f

Tactic:
change f = 1
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
intro : orderOf f ∣ 1
⊢ f = 1

Tactic:
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]

Premises used: pow_one, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
intro :
  ∀ (c : ℕ)
    (hc :
      Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c),
    orderOf f ∣ 1
⊢ orderOf f ∣ 1

Tactic:
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi

Premises used: Nat.dvd_gcd
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
inst_2 : Finite ι
inst_3 : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun (i j : ι) ↦ (Fintype.card.{u_3} (H i)).Coprime (Fintype.card.{u_3} (H j))
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp_1 : f ∈ (↑(⨆ (x : { j : ι // ¬j = i }), range (G := H (↑x : ι)) (ϕ (↑x : ι))) : Set G)
g : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)
hgf :
  (noncommPiCoprod (N := fun (i_1 : { j : ι // ¬j = i }) ↦ H (↑i_1 : ι)) (fun (x : { j : ι // ¬j = i }) ↦ ϕ (↑x : ι))
          ⋯ :
        (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
      g =
    f
g' : H i
hg'f : (ϕ i : (a : H i) → G) g' = f
hxi : orderOf f ∣ Fintype.card.{u_3} (H i)
hxp : orderOf f ∣ ∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))
c : ℕ
hc : Nat.gcd (∏ j : { j : ι // j ≠ i }, Fintype.card.{u_3} (H (↑j : ι))) (Fintype.card.{u_3} (H i)) = orderOf f * c
h : 1 = orderOf f * c
⊢ orderOf f ∣ 1

Tactic:
use c