-- 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
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } = u'
hcan : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
pos :
  ∀ (h1 : w.head ∈ d.set { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ })
    (h2 :
      ∀ u' ∈ Option.map Prod.fst w.toList.head?,
        w.head ∈ toSubgroup A B { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
          { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } = u')
    (hcan : Cancels 1 (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)),
    (∀ (h : cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
        ReducedWord.prod φ
            (unitsSMulWithCancel φ 1
                (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
                hcan).toReducedWord =
          HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
            ReducedWord.prod φ
              (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1
                  h2).toReducedWord) →
      (of : (a : G) → HNNExtension G A B φ)
            (↑((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1)))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B 1) g ⋯)) :
              G) *
          ReducedWord.prod φ w.toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
          HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
            ((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)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
          G) *
      ReducedWord.prod φ w.toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        ((HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)
have pos₁ : ∀ (h1 : w.head ∈ d.set { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ })
  (h2 :
    ∀ u' ∈ Option.map Prod.fst w.toList.head?,
      w.head ∈ toSubgroup A B { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } →
        { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry } = u')
  (hcan :
    Cancels (-1) (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)),
  (∀ (h : cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2 = w),
      ReducedWord.prod φ
          (unitsSMulWithCancel φ (-1)
              (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)
              hcan).toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
          ReducedWord.prod φ
            (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1
                h2).toReducedWord) →
    (of : (a : G) → HNNExtension G A B φ)
          (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B (-1)) g sorry)) :
            G) *
        ReducedWord.prod φ w.toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
        HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
          ((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, h1, h2, hcan, h