-- 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
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)
neg :
  ∀ (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_1} (G := G) (A := A) (B := B) (d := d) (-u)
          (if h :
              Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2) then
            unitsSMulWithCancel φ u
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
          else
            let g' :=
              unitsSMulGroup φ d u
                (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).head;
            cons (↑g'.1 : G) u
              (((↑g'.2 : G) *
                  (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).head⁻¹) •
                cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
              ⋯ ⋯))
    (hcan2 : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2))
    (hcan_2 :
      ¬Cancels (-u)
          (unitsSMulWithCancel φ u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } 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 { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } w h1 h2
⊢ 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

Tactic:
cases hcan2.2

Premises used: And.right