-- 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 : ¬Cancels u w
neg :
  ∀ (hcan : ¬Cancels 1 w),
    (of : (a : G) → HNNExtension G A B φ)
          (↑((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1)))
                ((IsComplement.equiv (S := (↑(toSubgroup A B 1) : Set G)) (T := d.set 1) ⋯ :
                      (a : G) → ↥(toSubgroup A B 1) × (↑(d.set 1) : Type u_1))
                    w.head).1) :
            G) *
        (HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
          (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
              ((of : (a : G) → HNNExtension G A B φ)
                  (↑((IsComplement.equiv (S := (↑(toSubgroup A B 1) : Set G)) (T := d.set 1) ⋯ :
                            (a : G) → ↥(toSubgroup A B 1) × (↑(d.set 1) : Type u_1))
                          w.head).2 :
                    G) :
                HNNExtension G A B φ)
              (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ) *
            ReducedWord.prod φ w.toReducedWord)) =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) * ReducedWord.prod φ w.toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              ((⋯.equiv (S := (↑(toSubgroup A B u) : Set G)) (T := d.set u) :
                    (a : G) → ↥(toSubgroup A B u) × (↑(d.set u) : Type u_1))
                  w.head).1) :
          G) *
      (HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
            ((of : (a : G) → HNNExtension G A B φ)
                (↑((⋯.equiv (S := (↑(toSubgroup A B u) : Set G)) (T := d.set u) :
                          (a : G) → ↥(toSubgroup A B u) × (↑(d.set u) : Type u_1))
                        w.head).2 :
                  G) :
              HNNExtension G A B φ)
            (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ) *
          ReducedWord.prod φ w.toReducedWord)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
have neg₁ : ∀ (hcan : ¬Cancels (-1) w),
  (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
              ((IsComplement.equiv (S := (↑(toSubgroup A B (-1)) : Set G)) (T := d.set (-1)) sorry :
                    (a : G) → ↥(toSubgroup A B (-1)) × (↑(d.set (-1)) : Type u_1))
                  w.head).1) :
          G) *
      (HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
        (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
            ((of : (a : G) → HNNExtension G A B φ)
                (↑((IsComplement.equiv (S := (↑(toSubgroup A B (-1)) : Set G)) (T := d.set (-1)) sorry :
                          (a : G) → ↥(toSubgroup A B (-1)) × (↑(d.set (-1)) : Type u_1))
                        w.head).2 :
                  G) :
              HNNExtension G A B φ)
            (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ) *
          ReducedWord.prod φ w.toReducedWord)) =
    HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) * ReducedWord.prod φ w.toReducedWord
Tactic: rcases Int.units_eq_one_or u with (rfl | rfl)
Cleared hypotheses: u, hcan