-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ 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
have 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) sorry sorry))
  (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)
          sorry sorry =
        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)
      sorry sorry =
    cons g u' w h1 h2
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]
Cleared hypotheses: w, hcan_1, hcan2, hcan