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 α
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
i_1 j_1 i j k_1 l : ι
w₁ : NeWord H i j
hne : j ≠ k_1
w₂ : NeWord H k_1 l
hIw₁ :
  ∀ {k : ι} (hk : j ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) :
              (a : CoprodI H) → G)
            (w₁.prod (M := H)) :
          G)
        (X k) ⊆
      X i
hIw₂ :
  ∀ {k : ι} (hk : l ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) :
              (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k) ⊆
      X k_1
k : ι
hk : l ≠ k
lift :
  HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((w₁.append (M := H) hne w₂).prod (M := H)) :
        G)
      (X k) =
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₁.prod (M := H)) :
        G)
      (HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) :
              (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k))
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((CoprodI.lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((w₁.append (M := H) hne w₂).prod (M := H)) :
        G)
      (X k) ⊆
    X i

Tactic:
calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne

Premises used: Iff.mpr, Monoid.CoprodI.lift, Monoid.CoprodI.NeWord.append, Monoid.CoprodI.NeWord.prod, Set.smul_set_subset_smul_set_iff, DFunLike.coe
-- 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 α
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
i j k : ι
w : NeWord H i j
hk : j ≠ k
singleton :
  ∀ {i : ι} (x : H i) (hne_one : x ≠ 1) {k : ι} (hk : i ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (NeWord.prod (M := H) (NeWord.singleton (M := H) x hne_one)) :
          G)
        (X k) ⊆
      X i
append :
  ∀ {i j k l : ι} (w₁ : NeWord H i j) (hne : j ≠ k) (w₂ : NeWord H k l)
    (hIw₁ :
      ∀ {k : ι} (hk : j ≠ k),
        HSMul.hSMul.{u_4, u_6, u_6} (α := 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)
            (X k) ⊆
          X i)
    (hIw₂ :
      ∀ {k_1 : ι} (hk : l ≠ k_1),
        HSMul.hSMul.{u_4, u_6, u_6} (α := 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)
            (X k_1) ⊆
          X k)
    {k_1 : ι} (hk : l ≠ k_1),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            ((w₁.append (M := H) hne w₂).prod (M := H)) :
          G)
        (X k_1) ⊆
      X i
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := 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)
      (X k) ⊆
    X i

Tactic:
induction w generalizing k with
  | singleton x hne_one => simpa using hpp hk _ hne_one
  | @append i j k l w₁ hne w₂ hIw₁ hIw₂ =>
    calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne

Premises used: Singleton.singleton
-- 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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  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)
⊢ X k ⊆ X i

Tactic:
simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm

Premises used: Ne.symm, Monoid.CoprodI.lift_word_ping_pong
-- 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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  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)
⊢ X k ⊆ X i

Tactic:
have : X k ⊆ X i := by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  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)
this : X k ⊆ X i
obtain : ∀ (x : α) (hx : x ∈ X k), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := hXnonempty 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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  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)
this : X k ⊆ X i
x : α
hx : x ∈ X k
⊢ False

Tactic:
(hXdisj hhead).le_bot ⟨hx, this hx⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- 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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  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)
this : X k ⊆ X i
x : α
hx : x ∈ X k
⊢ False

Tactic:
exact (hXdisj hhead).le_bot ⟨hx, this hx⟩

Premises used: Disjoint.le_bot, And.intro
-- 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 : ι
w : NeWord H i i
obtain :
  ∀ (k : ι) (hk : k ≠ 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:
obtain ⟨k, hk⟩ := exists_ne i

Premises used: exists_ne
-- 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 : ι
w : NeWord H i i
k : ι
hk : k ≠ 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_other_i f X hXnonempty hXdisj hpp w hk hk

Premises used: 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 : ι
w : NeWord H i i
k : ι
hk : k ≠ 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_other_i f X hXnonempty hXdisj hpp w hk hk

Premises used: 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
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
obtain :
  ∀ (h : H i) (hn1 : h ≠ 1) (hnh : h ≠ (w.head (M := H))⁻¹),
    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:
obtain ⟨h, hn1, hnh⟩ := Cardinal.exists_ne_ne_of_three_le hcard 1 w.head⁻¹

Premises used: Cardinal.exists_ne_ne_of_three_le, Inv.inv, Monoid.CoprodI.NeWord.head, OfNat.ofNat
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
rw : h / (w.head (M := H))⁻¹ ≠ 1
⊢ h * w.head (M := H) ≠ 1

Tactic:
rw [← div_inv_eq_mul]

Premises used: div_inv_eq_mul
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
⊢ h / (w.head (M := H))⁻¹ ≠ 1

Tactic:
div_ne_one_of_ne hnh

Premises used: div_ne_one_of_ne
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
⊢ h / (w.head (M := H))⁻¹ ≠ 1

Tactic:
exact div_ne_one_of_ne hnh

Premises used: div_ne_one_of_ne
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
⊢ h * w.head (M := H) ≠ 1

Tactic:
have hnot1 : h * w.head ≠ 1 := by
    rw [← div_inv_eq_mul]
    exact div_ne_one_of_ne hnh
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
hnot1 : h * w.head (M := H) ≠ 1
w' : NeWord H i i := (w.mulHead (M := H) h hnot1).append (M := H) ⋯ (NeWord.singleton (M := H) h⁻¹ ⋯)
⊢ 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:
have hw' : lift f w'.prod ≠ 1 :=
    lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w'
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
hnot1 : h * w.head (M := H) ≠ 1
w' : NeWord H i i := (w.mulHead (M := H) h hnot1).append (M := H) ⋯ (NeWord.singleton (M := H) h⁻¹ ⋯)
hw' :
  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)
heq1 :
  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)
apply :
  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)
⊢ False

Tactic:
apply hw'
-- 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)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
hnot1 : h * w.head (M := H) ≠ 1
w' : NeWord H i i := (w.mulHead (M := H) h hnot1).append (M := H) ⋯ (NeWord.singleton (M := H) h⁻¹ ⋯)
hw' :
  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)
heq1 :
  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'.prod (M := H)) :
      G)
    (1 : G)

Tactic:
simp [w', heq1]
-- 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 :
  ∀ (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:
rcases hcard with hcard | hcard
-- 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 ≤ #ι
inl :
  ∀ (i_1 : ι) (h1 : i_1 ≠ i) (h2 : i_1 ≠ 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:
obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j

Premises used: Cardinal.exists_ne_ne_of_three_le
-- 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_1 j : ι
w : NeWord H i_1 j
hcard : 3 ≤ #ι
i : ι
h1 : i ≠ i_1
h2 : 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.prod (M := H)) :
      G)
    (1 : G)

Tactic:
lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2

Premises used: 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_1 j : ι
w : NeWord H i_1 j
hcard : 3 ≤ #ι
i : ι
h1 : i ≠ i_1
h2 : 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.prod (M := H)) :
      G)
    (1 : G)

Tactic:
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2

Premises used: 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
hcard : ∃ (i : ι), 3 ≤ #(H i)
inr :
  ∀ (k : ι) (hcard : 3 ≤ #(H 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:
obtain ⟨k, hcard⟩ := hcard