-- Mathlib/GroupTheory/PushoutI.lean
theorem Reduced.eq_empty_of_mem_range
    (hφ : ∀ i, Injective (φ i)) {w : Word G} (hw : Reduced φ w)
    (h : ofCoprodI w.prod ∈ (base φ).range) : w = .empty

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
⊢ w = Word.empty

Tactic:
rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩

Result:
case intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ w = Word.empty

Proof state:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty

Tactic:
rw [← hw'prod, ← this] at heq

Result:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
⊢ w = Word.empty

Tactic:
simp [this, @eq_comm _ []] at hw'map

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
⊢ w = Word.empty

Proof state:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w'.toWord = Word.empty

Tactic:
rw [← prod_injective heq]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
⊢ { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h

Tactic:
simp [NormalWord.prod]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
⊢ ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ Word.empty.toList → g ∈ d.set i

Tactic:
simp

Result:
no goals

Proof state:
case toList.h.a
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
i✝ : ℕ
a✝ : (i : ι) × G i
⊢ a✝ ∈ w.toList[i✝]? ↔ a✝ ∈ Word.empty.toList[i✝]?

Tactic:
simp [hw'map]

Result:
no goals

Proof state:
case intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ w = Word.empty

Tactic:
rcases h with ⟨h, heq⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
⊢ w = Word.empty

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
⊢ w = Word.empty

Tactic:
ext

Result:
case toList.h.a
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
i✝ : ℕ
a✝ : (i : ι) × G i
⊢ a✝ ∈ w.toList[i✝]? ↔ a✝ ∈ Word.empty.toList[i✝]?