-- 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 : ℤˣ
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_1 :
  ¬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 : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ cons
      (↑((toSubgroupEquiv φ (-u) : (a : ↥(toSubgroup A B (-u))) → ↥(toSubgroup A B (- -u)))
            ((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
                  (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                        (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                    G) *
                  w.head)).1) :
        G)
      (-u)
      (((↑((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
                    (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                  ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                          (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                      G) *
                    w.head)).2 :
            G) *
          (w.head⁻¹ *
            (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                    (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                G)⁻¹)) •
        HSMul.hSMul (α := G)
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
            G)
          w)
      ⋯ ⋯ =
    cons g u' w h1 h2
have neg : ∀ (h1 : w.head ∈ d.set { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ })
  (h2 :
    ∀ u' ∈ Option.map Prod.fst w.toList.head?,
      w.head ∈ toSubgroup A B { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } →
        { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } = u')
  (hcan :
    ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
        (if h :
            Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2) then
          unitsSMulWithCancel φ u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry } w h1 h2)
            h
        else
          let g' :=
            unitsSMulGroup φ d u
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2).head;
          cons (↑g'.1 : G) u
            (((↑g'.2 : G) *
                (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2).head⁻¹) •
              cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)
            sorry sorry))
  (hcan2 : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2))
  (hcan_2 :
    ¬Cancels (-u)
        (unitsSMulWithCancel φ u
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2) hcan2)),
  cons
      (↑((toSubgroupEquiv φ (-u) : (a : ↥(toSubgroup A B (-u))) → ↥(toSubgroup A B (- -u)))
            ((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) sorry :
                  (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                        (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g sorry)) :
                    G) *
                  w.head)).1) :
        G)
      (-u)
      (((↑((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) sorry :
                    (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                  ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                          (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g sorry)) :
                      G) *
                    w.head)).2 :
            G) *
          (w.head⁻¹ *
            (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                    (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g sorry)) :
                G)⁻¹)) •
        HSMul.hSMul (α := G)
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g sorry)) :
            G)
          w)
      sorry sorry =
    cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry } w h1 h2
Tactic: cases hcan2.2
Cleared hypotheses: u', h1, h2, hcan_1, hcan2, hcan