awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
pos :
  ∀ (hh : i = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
neg :
  ∀ (hh : ¬i = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
by_cases hh : i = k
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
pos :
  ∀ (hl : j = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
neg :
  ∀ (hl : ¬j = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
by_cases hl : j = k
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
pos :
  ∀ (hl : j = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
neg :
  ∀ (hl : ¬j = k),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
by_cases hl : j = k
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : j = k
⊢ 3 ≤ #(H i)

Tactic:
subst hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : j = k
hcard₁ : 3 ≤ #(H i)
⊢ j = i

Tactic:
subst hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : j = i
pos :
  ∀ (w : NeWord H j j) (hcard : 3 ≤ #(H j)),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
subst hl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
j : ι
w : NeWord H j j
hcard : 3 ≤ #(H j)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w

Premises used: Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
j : ι
w : NeWord H j j
hcard : 3 ≤ #(H j)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w

Premises used: Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
⊢ 3 ≤ #(H i)

Tactic:
subst hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
hcard₁ : 3 ≤ #(H i)
⊢ ¬j = i

Tactic:
subst hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : ¬j = i
⊢ j ≠ i

Tactic:
change j ≠ i at hl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : j ≠ i
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm

Premises used: Ne.symm, Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : j ≠ i
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm

Premises used: Ne.symm, Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : j = k
⊢ 3 ≤ #(H j)

Tactic:
subst hl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : j = k
hcard₁ : 3 ≤ #(H j)
⊢ ¬i = j

Tactic:
subst hl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : ¬i = j
⊢ i ≠ j

Tactic:
change i ≠ j at hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.inv (G := H).prod (M := H)) :
      G)
    (1 : G)

Tactic:
have : lift f w.inv.prod ≠ 1 :=
          lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this :
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.inv (G := H).prod (M := H)) :
      G)
    (1 : G)
heq :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
pos :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.inv (G := H).prod (M := H)) :
      G)
    (1 : G)
⊢ False

Tactic:
apply this
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this :
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.inv (G := H).prod (M := H)) :
      G)
    (1 : G)
heq :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.inv (G := H).prod (M := H)) :
      G)
    (1 : G)

Tactic:
simpa using heq
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : ¬j = k
⊢ i ≠ k

Tactic:
change i ≠ k at hh
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hl : ¬j = k
hh : i ≠ k
⊢ j ≠ k

Tactic:
change j ≠ k at hl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i ≠ k
hl : j ≠ k
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm

Premises used: Ne.symm, Monoid.CoprodI.lift_word_prod_nontrivial_of_other_i
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i ≠ k
hl : j ≠ k
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm

Premises used: Ne.symm, Monoid.CoprodI.lift_word_prod_nontrivial_of_other_i
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
inl :
  ∀ (hcard : 3 ≤ #ι),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
inr inr₁ :
  ∀ (hcard : ∃ (i : ι), 3 ≤ #(H i)),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)

Tactic:
classical
    rcases hcard with hcard | hcard
    · obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j
      exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2
    · obtain ⟨k, hcard⟩ := hcard
      by_cases hh : i = k <;> by_cases hl : j = k
      · subst hh
        subst hl
        exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w
      · subst hh
        change j ≠ i at hl
        exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm
      · subst hl
        change i ≠ j at hh
        have : lift f w.inv.prod ≠ 1 :=
          lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
        intro heq
        apply this
        simpa using heq
      · change i ≠ k at hh
        change j ≠ k at hl
        exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm

Premises used: Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
h :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
by_contra : ∀ (hnotempty : ¬w = Word.empty (M := H)), False
⊢ w = Word.empty (M := H)

Tactic:
by_contra hnotempty
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
h :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
hnotempty : ¬w = Word.empty (M := H)
obtain :
  ∀ (i j : ι) (w : NeWord H i j)
    (h :
      Eq.{u_4 + 1} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w.toWord (M := H).prod (M := H)) :
          G)
        (1 : G))
    (hnotempty : ¬w.toWord (M := H) = Word.empty (M := H)), False
⊢ False

Tactic:
obtain ⟨i, j, w, rfl⟩ := NeWord.of_word w hnotempty

Premises used: Monoid.CoprodI.NeWord.of_word, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
h :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.toWord (M := H).prod (M := H)) :
      G)
    (1 : G)
hnotempty : ¬w.toWord (M := H) = Word.empty (M := H)
⊢ False

Tactic:
lift_word_prod_nontrivial_of_not_empty f hcard X hXnonempty hXdisj hpp w h

Premises used: Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty