-- 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
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : Cancels 1 w
pos :
  ∀ (g_1 : G)
    (this :
      Cancels 1 (HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1)) ↔
        Cancels (A := A) (B := B) (d := d) 1 (ofGroup g_1))
    (hcan : Cancels (A := A) (B := B) (d := d) 1 (ofGroup g_1)),
    consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d)
        (HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1))
        (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦
          HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1))
        (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) (ofGroup g_1)
            (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ ofGroup g_1)
            (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) • w)
      (fun (g_1 : G) (a : g_1 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • w)
      (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) w
          (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ w)
          (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₁ : ∀ (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 : 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 sorry)) : G) w)
          sorry =
        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 sorry)) : 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 sorry)) : G) w)
        sorry =
      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 sorry)) : G) w)
            hcan :
          NormalWord d)
Tactic: cases w using consRecOn
Cleared hypotheses: w, this, hcan