-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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)
⊢ 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
have 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)) sorry :
        (a : G) → (↑(↑(toSubgroup A B (-u)) : Set G) : Type u_1) × (↑(d.set (-u)) : Type u_1))
      w.head).1
  1
Tactic: have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1