-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_word_prod_nontrivial_of_head_card {i j} (w : NeWord H i j)
    (hcard : 3 ≤ #(H i)) (hheadtail : i ≠ j) : lift f w.prod ≠ 1

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
⊢ (lift f) w.prod ≠ 1

Tactic:
obtain ⟨h, hn1, hnh⟩ := Cardinal.three_le hcard 1 w.head⁻¹

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
⊢ (lift f) w.prod ≠ 1

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
⊢ h * w.head ≠ 1

Tactic:
rw [← div_inv_eq_mul]

Result:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
⊢ h / w.head⁻¹ ≠ 1

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
⊢ h / w.head⁻¹ ≠ 1

Tactic:
exact div_ne_one_of_ne hnh

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
⊢ (lift f) w.prod ≠ 1

Tactic:
have hw' : lift f w'.prod ≠ 1 :=
  lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w'

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
⊢ (lift f) w.prod ≠ 1

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
⊢ (lift f) w.prod ≠ 1

Tactic:
let w' : NeWord H i i :=
  NeWord.append (NeWord.mulHead w h hnot1) hheadtail.symm
    (NeWord.singleton h⁻¹ (inv_ne_one.mpr hn1))

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
⊢ (lift f) w.prod ≠ 1

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ False

Tactic:
apply hw'

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ (lift f) w'.prod = 1

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
⊢ (lift f) w.prod ≠ 1

Tactic:
have hnot1 : h * w.head ≠ 1 := by
  rw [← div_inv_eq_mul]
  exact div_ne_one_of_ne hnh

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : 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⁻¹
hnot1 : h * w.head ≠ 1
⊢ (lift f) w.prod ≠ 1