case inl
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#ι)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1

case inr
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : ∃ i, 3 ≤ (#H i)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
cases' hcard with hcard hcard
case inl.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i✝ j : ι
w : NeWord H i✝ j
hcard : 3 ≤ (#ι)
i : ι
h1 : i ≠ i✝
h2 : i ≠ j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case inl
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#ι)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
obtain ⟨i, h1, h2⟩ := Cardinal.three_le hcard i j
no goals
case inl.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i✝ j : ι
w : NeWord H i✝ j
hcard : 3 ≤ (#ι)
i : ι
h1 : i ≠ i✝
h2 : i ≠ j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2
case inr.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case inr
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : ∃ i, 3 ≤ (#H i)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
cases' hcard with k hcard
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i = k
hl : j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1

case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i = k
hl : ¬j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1

case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : ¬i = k
hl : j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1

case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : ¬i = k
hl : ¬j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case inr.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
by_cases hh : i = k <;> by_cases hl : j = k
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : j = i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i = k
hl : j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
subst hh
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
j : ι
w : NeWord H j j
hcard : 3 ≤ (#H j)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : j = i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
subst hl
no goals
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
j : ι
w : NeWord H j j
hcard : 3 ≤ (#H j)
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : ¬j = i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i = k
hl : ¬j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
subst hh
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : j ≠ i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : ¬j = i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
change j ≠ i at hl
no goals
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H i)
hl : j ≠ i
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : ¬i = j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : ¬i = k
hl : j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
subst hl
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : ¬i = j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
change i ≠ j at hh
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
have : lift f w.inv.prod ≠ 1 :=
  lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
heq : ↑(↑lift f) (NeWord.prod w) = 1
⊢ False
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
intro heq
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
heq : ↑(↑lift f) (NeWord.prod w) = 1
⊢ ↑(↑lift f) (NeWord.prod (NeWord.inv w)) = 1
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
heq : ↑(↑lift f) (NeWord.prod w) = 1
⊢ False
apply this
no goals
case pos
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
hcard : 3 ≤ (#H j)
hh : i ≠ j
this : ↑(↑lift f) (NeWord.prod (NeWord.inv w)) ≠ 1
heq : ↑(↑lift f) (NeWord.prod w) = 1
⊢ ↑(↑lift f) (NeWord.prod (NeWord.inv w)) = 1
simpa using heq
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hl : ¬j = k
hh : i ≠ k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : ¬i = k
hl : ¬j = k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
change i ≠ k at hh
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hl : ¬j = k
hh : i ≠ k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
change j ≠ k at hl
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
obtain ⟨h, hn1, -⟩ := Cardinal.three_le hcard 1 1
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
let w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) hh.symm w) hl
    (NeWord.singleton h⁻¹ (inv_ne_one.mpr hn1))
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
have hw' : lift f w'.prod ≠ 1 :=
  lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w'
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
heq1 : ↑(↑lift f) (NeWord.prod w) = 1
⊢ False
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
⊢ ↑(↑lift f) (NeWord.prod w) ≠ 1
intro heq1
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
heq1 : ↑(↑lift f) (NeWord.prod w) = 1
⊢ ↑(↑lift f) (NeWord.prod w') = 1
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
heq1 : ↑(↑lift f) (NeWord.prod w) = 1
⊢ False
apply hw'
no goals
case neg.intro.intro
ι : Type u_1
M : ι → Type ?u.842716
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.842727
inst✝³ : Monoid N
hnontriv : Nontrivial ι
G : Type u_3
inst✝² : Group G
H : ι → Type u_2
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type ?u.843508
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X j ⊆ X i
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ (#H k)
hh : i ≠ k
hl : j ≠ k
h : H k
hn1 : h ≠ 1
w' : NeWord H k k :=
  NeWord.append (NeWord.append (NeWord.singleton h hn1) (_ : k ≠ i) w) hl (NeWord.singleton h⁻¹ (_ : h⁻¹ ≠ 1))
hw' : ↑(↑lift f) (NeWord.prod w') ≠ 1
heq1 : ↑(↑lift f) (NeWord.prod w) = 1
⊢ ↑(↑lift f) (NeWord.prod w') = 1
simp [heq1]