-- 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
g : ↥A
g_1 : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
this : Cancels 1 ((↑g : G) • cons g_1 u w h1 h2) ↔ Cancels 1 (cons g_1 u w h1 h2)
hcan : Cancels 1 (cons g_1 u w h1 h2)
h :
  ∀ (h : cons g_1 u w h1 h2 = w),
    consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) ((↑g : G) • cons g_1 u w h1 h2)
        (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • cons g_1 u w h1 h2)
        (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
            (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
            (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
          HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
        ⋯ =
      HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) (cons g_1 u w h1 h2)
            (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ cons g_1 u w h1 h2)
            (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
                (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
                (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
              HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
            hcan :
          NormalWord d)
⊢ consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) ((↑g : G) • cons g_1 u w h1 h2)
      (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • cons g_1 u w h1 h2)
      (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
          (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
          (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
        HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
      ⋯ =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) (cons g_1 u w h1 h2)
          (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ cons g_1 u w h1 h2)
          (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
              (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
              (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
            HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
          hcan :
        NormalWord d)
have pos : HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) ((↑g : G) * g_1) sorry)) : G) w =
  HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
    (HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g_1 sorry)) : G) w)
Tactic: simp only [smul_cons, consRecOn_cons]