-- Module: Mathlib.GroupTheory.HNNExtension
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)
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)

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl