-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
hcan2 : Cancels u w
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u w hcan2)
neg :
  ∀ (g : G)
    (hcan :
      ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
          (if h : Cancels (A := A) (B := B) (d := d) u (ofGroup g) then unitsSMulWithCancel φ u (ofGroup g) h
          else
            let g' := unitsSMulGroup φ d u (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)));
            cons (↑g'.1 : G) u
              (HSMul.hSMul (β := NormalWord d)
                ((↑g'.2 : G) * (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)))⁻¹) (ofGroup g))
              ⋯ ⋯))
    (hcan2 : Cancels (A := A) (B := B) (d := d) u (ofGroup g))
    (hcan_2 : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2)),
    cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).1 : G) (-u)
        (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).2 : G) *
            (unitsSMulWithCancel φ u (ofGroup g) hcan2).head⁻¹) •
          unitsSMulWithCancel φ u (ofGroup g) hcan2)
        ⋯ ⋯ =
      ofGroup g
neg₁ :
  ∀ (g : G) (u' : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u')
    (h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1)
    (hcan :
      ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
          (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
          else
            let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
            cons (↑g'.1 : G) u (((↑g'.2 : G) * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯))
    (hcan2 : Cancels u (cons g u' w h1 h2)) (hcan_2 : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2))
    (ih :
      ∀ (h : cons g u' w h1 h2 = w),
        cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).1 : G) (-u)
            (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).2 : G) *
                (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head⁻¹) •
              unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
            ⋯ ⋯ =
          cons g u' w h1 h2),
    cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).1 : G) (-u)
        (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).2 : G) *
            (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head⁻¹) •
          unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
        ⋯ ⋯ =
      cons g u' w h1 h2
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u w hcan2).head⁻¹) •
        unitsSMulWithCancel φ u w hcan2)
      ⋯ ⋯ =
    w

Tactic:
cases w using consRecOn with
    | ofGroup => simp [Cancels] at hcan2
    | cons g u' w h1 h2 ih =>
      clear ih
      simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, id_eq, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]
      cases hcan2.2
      have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1
      simpa [NormalWord.ext_iff, (d.compl (-u)).equiv_mul_left, Units.ext_iff,
        (d.compl (-u)).equiv_snd_eq_inv_mul]

Premises used: HNNExtension.NormalWord.ofGroup, HNNExtension.NormalWord.Cancels, Units.ext_iff, SetLike.coe_sort_coe, HNNExtension.NormalWord.ext_iff, HNNExtension.NormalWord.consRecOn_cons, HNNExtension.NormalWord.group_smul_head, And.right, HNNExtension.NormalWord.cons, mul_inv_rev, HNNExtension.NormalWord.TransversalPair.compl, HNNExtension.NormalWord.unitsSMulGroup, HNNExtension.NormalWord.unitsSMulWithCancel, Subgroup.IsComplement.equiv_mul_left, Subgroup.IsComplement.equiv_snd_eq_inv_mul, Neg.neg, id_eq