-- Mathlib/GroupTheory/HNNExtension.lean
theorem exists_normalWord_prod_eq
    (d : TransversalPair G A B) (w : ReducedWord G A B) :
    ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧
      w'.toList.map Prod.fst = w.toList.map Prod.fst ∧
      ∀ u ∈ w.toList.head?.map Prod.fst,
      w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

Proof state:
case mk.cons.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)

Tactic:
refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩

Result:
case mk.cons.intro.intro.intro.refine_1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ ((t ^ ↑a.1 * of a.2) • w').toReducedWord =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }

case mk.cons.intro.intro.intro.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w✝ w : ReducedWord G A B
hw1 : w.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)

Tactic:
rcases w with ⟨g, l, chain⟩

Result:
case mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : { head := g, toList := l, chain := chain }.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := g, toList := l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain }.toList.head?, w'.head ∈ toSubgroup A B (-u)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ a.2 * w'.head ∈ toSubgroup A B a.1 → ∀ (x : G), ¬w'.toList.head? = some (-a.1, x)

Tactic:
intro hS x hx

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
⊢ False

Proof state:
case mk.cons.intro.intro.intro.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
this : ¬Cancels a.1 (a.2 • w')
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)

Tactic:
erw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def,
  t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]

Result:
case mk.cons.intro.intro.intro.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
this : ¬Cancels a.1 (a.2 • w')
⊢ List.map Prod.fst
        (let g' := unitsSMulGroup φ d a.1 { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ }.head;
          cons (↑g'.1) a.1
            ((↑g'.2 * { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ }.head⁻¹) •
              { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ })
            ⋯ ⋯).toList =
      a.1 :: List.map Prod.fst w'.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      (let g' := unitsSMulGroup φ d a.1 { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ }.head;
          cons (↑g'.1) a.1
            ((↑g'.2 * { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ }.head⁻¹) •
              { head := a.2 * w'.head, toList := w'.toList, chain := ⋯, mem_set := ⋯ })
            ⋯ ⋯).head ∈
        toSubgroup A B (-u)