-- 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_1 :
  ¬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 :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u
        (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2) hcan2)
this :
  Eq.{u_1 + 1} (α := (↑(↑(toSubgroup A B (-u)) : Set G) : Type u_1))
    ((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
          (a : G) → (↑(↑(toSubgroup A B (-u)) : Set G) : Type u_1) × (↑(d.set (-u)) : Type u_1))
        w.head).1
    1
⊢ 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

Tactic:
simpa [NormalWord.ext_iff, (d.compl (-u)).equiv_mul_left, Units.ext_iff,
        (d.compl (-u)).equiv_snd_eq_inv_mul]

Premises used: Units.ext_iff, HNNExtension.NormalWord.ext_iff, HNNExtension.NormalWord.TransversalPair.compl, Subgroup.IsComplement.equiv_mul_left, Subgroup.IsComplement.equiv_snd_eq_inv_mul, Neg.neg