awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
⊢ Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
have rw : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
f : (i : ι) → H i
heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f
⊢ Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
have this : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)
Tactic: have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
f : (i : ι) → H i
heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f
this :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)
⊢ Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
have h : ∀ (i : ι), f i = 1 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
f : (i : ι) → H i
heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f
this :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)
i : ι
⊢ f i = 1 i
have h : Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) ((ϕ i : (a : H i) → G) (1 i) : G)
Tactic: apply hinj
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have apply₁ : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₁ : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have apply₂ : ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f),
  Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₁ : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₂ :
  ∀ ⦃f : (i : ι) → H i⦄
    (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f),
    Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have apply₃ : ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
  (this :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)),
  Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₁ : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₂ :
  ∀ ⦃f : (i : ι) → H i⦄
    (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f),
    Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
apply₃ :
  ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
    (this :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)),
    Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have h : ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
  (this :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G))
  (i : ι), f i = 1 i
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
inst_2 : Fintype ι
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)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₁ : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
apply₂ :
  ∀ ⦃f : (i : ι) → H i⦄
    (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f),
    Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
apply₃ :
  ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
    (this :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G)),
    Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f
h :
  ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
    (this :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G))
    (i : ι), f i = 1 i
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have h₁ : ∀ ⦃f : (i : ι) → H i⦄ (heq1 : Membership.mem (γ := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker f)
  (this :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) (1 : G))
  (i : ι), Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) ((ϕ i : (a : H i) → G) (1 i) : G)
Tactic: classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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))
⊢ iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
have intro : ∀ (val : Fintype ι), iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 : ι
⊢ Disjoint.{u_1} (α := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i)
    (⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (ϕ i).range) j)
have intro : LE.le.{u_1} (α := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (ϕ i).range) j)
  ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have 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 : ι)) sorry)) :
        Set G)),
  Membership.mem (γ := Subgroup G) ⊥ f
Tactic: rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
Cleared hypotheses: hxp
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have 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)
Tactic: rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
Cleared hypotheses: hxp
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ ∀ (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)
have intro : (↑i_1 : ι) ≠ (↑j : ι)
Tactic: apply hcomm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have 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 : ι))
            sorry :
          (a : (i_1 : { j : ι // ¬j = i }) → H (↑i_1 : ι)) → G)
        g =
      f),
  Membership.mem (γ := Subgroup G) ⊥ f
Tactic: obtain ⟨g, hgf⟩ := hxp
Cleared hypotheses: hxp
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have intro : ∀ (g' : H i) (hg'f : (ϕ i : (a : H i) → G) g' = f), Membership.mem (γ := Subgroup G) ⊥ f
Tactic: obtain ⟨g', hg'f⟩ := hxi
Cleared hypotheses: hxi
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
have rw : orderOf.{u_1} (G := G) ((ϕ i : (a : H i) → G) g' : G) ∣ Fintype.card.{u_3} (H i)
Tactic: rw [← hg'f]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ Membership.mem (γ := Subgroup G) ⊥ f
have hxi : 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