ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
⊢ ∀ (a : FreeProduct fun i => H i), ↑(↑lift f) a = 1 → a = 1
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
⊢ Function.Injective ↑(↑lift f)
apply (injective_iff_map_eq_one (lift f)).mpr
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
⊢ ∀ (y : Word fun i => H i), ↑(↑lift f) (↑Word.equiv.symm y) = 1 → ↑Word.equiv.symm y = 1
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
⊢ ∀ (a : FreeProduct fun i => H i), ↑(↑lift f) a = 1 → a = 1
rw [(FreeProduct.Word.equiv).forall_congr_left']
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (↑Word.equiv.symm w) = 1
⊢ ↑Word.equiv.symm w = 1
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
⊢ ∀ (y : Word fun i => H i), ↑(↑lift f) (↑Word.equiv.symm y) = 1 → ↑Word.equiv.symm y = 1
intro w Heq
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (Word.prod w) = 1
⊢ Word.prod w = 1
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (↑Word.equiv.symm w) = 1
⊢ ↑Word.equiv.symm w = 1
dsimp [Word.equiv] at *
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (Word.prod w) = 1
⊢ Word.prod Word.empty = 1
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (Word.prod w) = 1
⊢ Word.prod w = 1
rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq]
no goals
ι : Type u_1
M : ι → Type ?u.925901
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.925912
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.926693
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
w : Word fun i => H i
Heq : ↑(↑lift f) (Word.prod w) = 1
⊢ Word.prod Word.empty = 1
rfl