awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : N i
⊢ Membership.mem (α := M) (γ := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) ((ϕ i : (a : N i) → M) y : M)

Tactic:
exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
dsimp : Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯)
⊢ Commute m ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) h)

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: OneHom.coe_mk, MonoidHom.coe_mk, MonoidHom.noncommPiCoprod
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
hom : ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)
unit : Commute m 1
base : ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → Commute m ((ϕ x : (a : N x) → M) (h x))
⊢ Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯)

Tactic:
apply Finset.noncommProd_induction

Premises used: Finset.noncommProd_induction
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)

Tactic:
fun x y ↦ Commute.mul_right

Premises used: Commute.mul_right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)

Tactic:
exact fun x y ↦ Commute.mul_right

Premises used: Commute.mul_right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ Commute m 1

Tactic:
Commute.one_right _

Premises used: Commute.one_right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ Commute m 1

Tactic:
exact Commute.one_right _

Premises used: Commute.one_right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → Commute m ((ϕ x : (a : N x) → M) (h x))

Tactic:
fun x _ ↦ comm x (h x)
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → Commute m ((ϕ x : (a : N x) → M) (h x))

Tactic:
exact fun x _ ↦ comm x (h x)
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
h : (i : ι) → N i
⊢ Eq.{u_1 + 1} (α := M) ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) h : M)
    (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯ : M)

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: OneHom.coe_mk, MonoidHom.coe_mk, MonoidHom.noncommPiCoprod
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
P : Type u_4
inst_3 : Monoid P
f : M →* P
i j : ι
x : N i
h : ∀ (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
y : N j
⊢ Commute.{u_4} (S := P) ((f.comp (ϕ i) : (a : N i) → P) x : P) ((f.comp (ϕ j) : (a : N j) → P) y : P)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, Commute.map (h y) f]

Premises used: MonoidHom.coe_comp, Commute.map, Function.comp_apply
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
P : Type u_4
inst_3 : Monoid P
f : M →* P
hcomm' :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j),
      Commute.{u_4} (S := P) ((f.comp (ϕ i) : (a : N i) → P) x : P) ((f.comp (ϕ j) : (a : N j) → P) y : P)
x : (i : ι) → N i
⊢ Eq.{u_4 + 1} (α := P) ((f.comp (noncommPiCoprod (N := N) ϕ hcomm) : (a : (i : ι) → N i) → P) x : P)
    ((noncommPiCoprod (N := N) (fun (i : ι) ↦ f.comp (ϕ i)) hcomm' : (a : (i : ι) → N i) → P) x : P)

Tactic:
simp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk,
      Function.comp_apply, Finset.map_noncommProd]

Premises used: MonoidHom.coe_comp, OneHom.coe_mk, MonoidHom.coe_mk, Finset.map_noncommProd, MonoidHom.noncommPiCoprod, Function.comp_apply
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
a :
  LE.le.{u_1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i)) (⨆ (i : ι), (ϕ i).range)
a₁ :
  LE.le.{u_1} (α := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
    (⨆ (i : ι), (ϕ i).range)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range)
    ((noncommPiCoprod (N := H) ϕ hcomm : (a : (i : ι) → H i) → G) f : G)

Tactic:
Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_

Premises used: Multiset.foldr, Multiset.map, Set.Mem, Multiset.noncommFoldr, Multiset.noncommFold, Finset.noncommProd, Subgroup.noncommProd_mem, Multiset.noncommProd
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
a :
  ∀ (c : ι),
    Membership.mem (γ := Finset ι) Finset.univ c →
      Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ c : (a : H c) → G) (f c) : G)
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range)
    ((noncommPiCoprod (N := H) ϕ hcomm : (a : (i : ι) → H i) → G) f : G)

Tactic:
refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_

Premises used: Subgroup.noncommProd_mem
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
a : Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)
a₁ :
  Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((ϕ i : (a : H i) → G) (f i) : G)
a₂ : Subgroup G
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ i : (a : H i) → G) (f i) : G)

Tactic:
apply Subgroup.mem_sSup_of_mem

Premises used: Subgroup.mem_sSup_of_mem
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
w : ι
h : Eq.{u_1 + 1} (α := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((fun (i : ι) ↦ (ϕ i).range) i)
⊢ Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)

Tactic:
use i
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((ϕ i : (a : H i) → G) (f i) : G)

Tactic:
simp
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
⊢ LE.le.{u_1} (α := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))

Tactic:
iSup_le ?_

Premises used: Set.Mem, iSup_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
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)
this : DecidableEq ι := Classical.decEq ι
a : ∀ (i : ι), (ϕ i).range ≤ (noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i)
⊢ LE.le.{u_1} (α := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))

Tactic:
refine iSup_le ?_

Premises used: iSup_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
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)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : H i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
    ((ϕ i : (a : H i) → G) y : G)

Tactic:
⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Premises used: Set.Mem, setOf, MonoidHom.noncommPiCoprod_mulSingle, Exists.intro, Set.range, Pi.mulSingle
-- 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
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)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : H i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
    ((ϕ i : (a : H i) → G) y : G)

Tactic:
exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
-- 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
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)

Tactic:
apply (MonoidHom.ker_eq_bot_iff _).mp

Premises used: MonoidHom.ker_eq_bot_iff, Iff.mp
-- 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
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)
rw : LE.le (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
⊢ Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- 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
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
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x → Membership.mem (α := G) (ϕ x).range ((ϕ x : (a : H x) → G) (f x) : G)

Tactic:
simp
-- 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
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
⊢ ∀ (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
-- 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
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)
h : ∀ (i : ι), f i = 1 i
⊢ Membership.mem (γ := Subgroup ((i : ι) → H i)) ⊥ f

Tactic:
ext i
-- 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
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 : ι
h : Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) ((ϕ i : (a : H i) → G) (1 i) : G)
⊢ f i = 1 i

Tactic:
apply hinj
-- 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
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 : ι
⊢ Eq.{u_1 + 1} (α := G) ((ϕ i : (a : H i) → G) (f i) : G) ((ϕ i : (a : H i) → G) (1 i) : G)

Tactic:
simp [this i (Finset.mem_univ i)]

Premises used: Finset.mem_univ
-- 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
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
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)
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H 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)]

Premises used: MonoidHom.ker_eq_bot_iff, Iff.mp, eq_bot_iff
-- 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))
intro : ∀ (val : Fintype ι), iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
⊢ iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype