-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_injective_of_ping_pong : Function.Injective (lift f)

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ ∀ (b : Word H), (lift f) (Word.equiv.symm b) = 1 → Word.equiv.symm b = 1

Tactic:
intro w Heq

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
Heq : (lift f) (Word.equiv.symm w) = 1
⊢ Word.equiv.symm w = 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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
Heq : (lift f) (Word.equiv.symm w) = 1
⊢ Word.equiv.symm w = 1

Tactic:
dsimp [Word.equiv] at *

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
Heq : (lift f) w.prod = 1
⊢ 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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ Function.Injective ⇑(lift f)

Tactic:
classical
  apply (injective_iff_map_eq_one (lift f)).mpr
  rw [(CoprodI.Word.equiv).forall_congr_left]
  intro w Heq
  dsimp [Word.equiv] at *
  rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]

Result:
no goals

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ ∀ (a : CoprodI H), (lift f) a = 1 → a = 1

Tactic:
rw [(CoprodI.Word.equiv).forall_congr_left]

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ ∀ (b : Word H), (lift f) (Word.equiv.symm b) = 1 → Word.equiv.symm b = 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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
Heq : (lift f) w.prod = 1
⊢ w.prod = 1

Tactic:
rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]

Result:
no goals

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ Function.Injective ⇑(lift f)

Tactic:
apply (injective_iff_map_eq_one (lift f)).mpr

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
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ ∀ (a : CoprodI H), (lift f) a = 1 → a = 1