awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁ a₂ : G
h :
  Eq (α := NormalWord d → NormalWord d)
    (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₁)
    (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₂)
w : NormalWord d
⊢ a₁ • w = a₂ • w

Tactic:
simp_all [funext_iff, of_smul_eq_smul]

Premises used: funext_iff, HNNExtension.NormalWord.of_smul_eq_smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁ a₂ : G
h :
  Eq (α := NormalWord d → NormalWord d)
    (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₁)
    (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₂)
⊢ a₁ = a₂

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, of_smul_eq_smul])

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
pos :
  ∀ (hw1 : w.head = 1),
    ∃ (w' : NormalWord d),
      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⁻¹ * w.head ∈ toSubgroup A B (-u)
neg :
  ∀ (hw1 : ¬w.head = 1),
    ∃ (w' : NormalWord d),
      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⁻¹ * w.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
by_cases hw1 : w.head = 1

Premises used: HNNExtension.NormalWord.ReducedWord.head
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : w.head = 1
pos :
  ∃ (w' : NormalWord d),
    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)
⊢ ∃ (w' : NormalWord d),
    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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
simp only [hw1, inv_mem_iff, mul_one]

Premises used: inv_mem_iff, mul_one
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : w.head = 1
⊢ ∃ (w' : NormalWord d),
    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:
this w hw1
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : w.head = 1
⊢ ∃ (w' : NormalWord d),
    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:
exact this w hw1
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : ¬w.head = 1
neg :
  ∀ (w' : NormalWord d)
    (hw' :
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
        List.map Prod.fst w'.toList =
            List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)),
    ∃ (w' : NormalWord d),
      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⁻¹ * w.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩

Premises used: HNNExtension.NormalWord.ReducedWord.chain, HNNExtension.NormalWord.ReducedWord.toList, HNNExtension.NormalWord.ReducedWord.mk, OfNat.ofNat, rfl
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : ¬w.head = 1
w' : NormalWord d
hw' :
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
    List.map Prod.fst w'.toList =
        List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ (w.head • w').toReducedWord = ReducedWord.prod φ w ∧
    List.map Prod.fst (w.head • w').toList = List.map Prod.fst w.toList ∧
      ∀ u ∈ Option.map Prod.fst w.toList.head?, (w.head • w').head⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
simpa [ReducedWord.prod, mul_assoc] using hw'

Premises used: mul_assoc, HNNExtension.NormalWord.ReducedWord.prod
-- 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
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
hw1 : ¬w.head = 1
w' : NormalWord d
hw' :
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
    List.map Prod.fst w'.toList =
        List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ : ReducedWord G A B }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
exact ⟨w.head • w', by
        simpa [ReducedWord.prod, mul_assoc] using hw'⟩
-- 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
suffices :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        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)
⊢ ∃ (w' : NormalWord d),
    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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
suffices ∀ w : ReducedWord G A B,
      w.head = 1 → ∃ 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 ∈ toSubgroup A B (-u) by
    by_cases hw1 : w.head = 1
    · simp only [hw1, inv_mem_iff, mul_one]
      exact this w hw1
    · rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩
      exact ⟨w.head • w', by
        simpa [ReducedWord.prod, mul_assoc] using hw'⟩
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w_1 w : ReducedWord G A B
hw1 : w.head = 1
rcases :
  ∀ (g : G) (l : List (ℤˣ × G)) (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l)
    (hw1 : { head := g, toList := l, chain := chain : ReducedWord G A B }.head = 1),
    ∃ (w' : NormalWord d),
      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 : ReducedWord G A B }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    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⟩
-- 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
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : g = 1
subst :
  ∃ (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)
⊢ ∃ (w' : NormalWord d),
    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 : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)

Tactic:
subst hw1
-- 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
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []
⊢ ∀ (u : ℤˣ) (g : G), Membership.mem (γ := List (ℤˣ × G)) [] (u, g) → g ∈ d.set u

Tactic:
simp
-- 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
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []
⊢ ReducedWord.prod φ (toReducedWord (d := d) { head := 1, toList := [], chain := ⋯, mem_set := ⋯ : NormalWord d }) =
      ReducedWord.prod φ { head := 1, toList := [], chain := chain } ∧
    List.map.{u_1, 0} (α := ℤˣ × G) Prod.fst
          (ReducedWord.toList (A := A) (B := B)
            (toReducedWord (d := d) { head := 1, toList := [], chain := ⋯, mem_set := ⋯ : NormalWord d })) =
        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?,
        ReducedWord.head (A := A) (B := B)
            (toReducedWord (d := d) { head := 1, toList := [], chain := ⋯, mem_set := ⋯ }) ∈
          toSubgroup A B (-u)

Tactic:
simp
-- 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
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)

Tactic:
exact
      ⟨{ head := 1
         toList := []
         mem_set := by simp
         chain := List.isChain_nil }, by simp⟩
-- 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
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)
cons :
  ∀ (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 := ⋯ : ReducedWord G A B }.toList)
    (hw'3 :
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, 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 := 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 := 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)

Tactic:
rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩

Premises used: And.right, List.isChain_cons, Iff.mp
-- 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
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ 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 := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, 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 := 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)

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

Premises used: Units.val, HMul.hMul, HNNExtension.of, HNNExtension.t, Prod.fst, HPow.hPow, And.intro, Exists.intro, HSMul.hSMul, Prod.snd, DFunLike.coe
-- 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
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ 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 := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head?,
    w'.head ∈ toSubgroup A B (-u)
cons :
  ReducedWord.prod φ
      (HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
            ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) •
          w').toReducedWord =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }
cons₁ :
  List.map Prod.fst
        (HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
              ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) •
            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?,
      (HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
              ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) •
            w').head ∈
        toSubgroup A B (-u)
⊢ ∃ (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)

Tactic:
refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
-- 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
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ 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 := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head?,
    w'.head ∈ toSubgroup A B (-u)
cons :
  HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
        ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) *
      ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ : ReducedWord G A B } =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }
⊢ ReducedWord.prod φ
      (HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
            ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) •
          w').toReducedWord =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }

Tactic:
rw [prod_smul, hw'1]

Premises used: HNNExtension.NormalWord.prod_smul
-- 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
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ 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 := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head?,
    w'.head ∈ toSubgroup A B (-u)
⊢ HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
        ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) *
      ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ : ReducedWord G A B } =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }

Tactic:
simp [ReducedWord.prod]

Premises used: HNNExtension.NormalWord.ReducedWord.prod
-- 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
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ 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 := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head?,
    w'.head ∈ toSubgroup A B (-u)
simp : a.2 * w'.head ∈ toSubgroup A B a.1 → ∀ (x : G), ¬w'.toList.head? = some (-a.1, x)
⊢ ¬Cancels a.1 (a.2 • w')

Tactic:
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]

Premises used: HNNExtension.NormalWord.Cancels, HNNExtension.NormalWord.group_smul_toList, not_exists, exists_eq_right, exists_and_right, HNNExtension.NormalWord.group_smul_head, Prod.exists, not_and, Option.map_eq_some_iff