-- Mathlib/GroupTheory/CoprodI.lean
theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeGroup.lift a)

Proof state:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Tactic:
clear hnne0 hlt

Result:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Proof state:
case refine_2
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ n ≤ -1, (fun n => a i ^ n • (X i)ᶜ ⊆ Y i) n → (fun n => a i ^ n • (X i)ᶜ ⊆ Y i) (n - 1)

Tactic:
dsimp

Result:
case refine_2
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ n ≤ -1, a i ^ n • (X i)ᶜ ⊆ Y i → a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

Proof state:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i => FreeGroup.lift fun x => a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective ⇑(FreeGroup.lift a)

Tactic:
rw [this, MonoidHom.coe_comp]

Result:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i => FreeGroup.lift fun x => a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective (⇑(lift fun i => FreeGroup.lift fun x => a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)

Proof state:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
⊢ Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)

Tactic:
let X' : ι → Set α := fun i => X i ∪ Y i

Result:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)

Proof state:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
hnne0 : n✝ ≠ 0
hgt : n✝ < 0
h1n : n✝ ≤ -1
n : ℤ
a✝ : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ

Tactic:
rw [zpow_sub, zpow_one]

Result:
no goals

Proof state:
case hXdisj
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ (Disjoint on X') i j

Tactic:
simp only [X']

Result:
case hXdisj
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => X i ∪ Y i) i j

Proof state:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
⊢ Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)

Tactic:
let H : ι → Type _ := fun _i => FreeGroup Unit

Result:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
⊢ Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)