-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
nil :
  ∀ (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []),
    ∃ (w' : NormalWord d),
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := [], chain := chain } ∧
        List.map Prod.fst w'.toList =
            List.map Prod.fst { head := 1, toList := [], chain := chain : ReducedWord G A B }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := chain : ReducedWord G A B }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)
cons :
  ∀ (a : ℤˣ × G) (l : List (ℤˣ × G))
    (ih :
      ∀ (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l),
        ∃ (w' : NormalWord d),
          ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := chain } ∧
            List.map Prod.fst w'.toList =
                List.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList ∧
              ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
                w'.head ∈ toSubgroup A B (-u))
    (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)),
    ∃ (w' : NormalWord d),
      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 : ReducedWord G A B }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)

Tactic:
induction l with
  | nil =>
    exact
      ⟨{ head := 1
         toList := []
         mem_set := by simp
         chain := List.isChain_nil }, by simp⟩
  | cons a l ih =>
    rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
    clear ih
    refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
    · rw [prod_smul, hw'1]
      simp [ReducedWord.prod]
    · have : ¬ Cancels a.1 (a.2 • w') := by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff,
          Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
      simp [mul_smul, of_smul_eq_smul, t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]

Premises used: HNNExtension.NormalWord.prod_smul, HNNExtension.NormalWord.unitsSMul, HNNExtension.NormalWord.ReducedWord.prod, HNNExtension.NormalWord.cons, HNNExtension.NormalWord.of_smul_eq_smul, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul, SemigroupAction.mul_smul