awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
u : ℤˣ
w : NormalWord d
hcan_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
hcan2 : Cancels u w
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u w hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u w hcan2).head⁻¹) •
        unitsSMulWithCancel φ u w hcan2)
      ⋯ ⋯ =
    w
have neg : ∀ (g : G)
  (hcan :
    ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
        (if h : Cancels (A := A) (B := B) (d := d) u (ofGroup g) then unitsSMulWithCancel φ u (ofGroup g) h
        else
          let g' := unitsSMulGroup φ d u (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)));
          cons (↑g'.1 : G) u
            (HSMul.hSMul (β := NormalWord d)
              ((↑g'.2 : G) * (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)))⁻¹) (ofGroup g))
            sorry sorry))
  (hcan2 : Cancels (A := A) (B := B) (d := d) u (ofGroup g))
  (hcan_2 : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2)),
  cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u (ofGroup g) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (ofGroup g) hcan2)
      sorry sorry =
    ofGroup g
Tactic: cases w using consRecOn with
    | ofGroup => simp [Cancels] at hcan2
    | cons g u' w h1 h2 ih =>
      clear ih
      simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, id_eq, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]
      cases hcan2.2
      have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1
      simpa [NormalWord.ext_iff, (d.compl (-u)).equiv_mul_left, Units.ext_iff,
        (d.compl (-u)).equiv_snd_eq_inv_mul]
Cleared hypotheses: w, hcan_1, hcan2, hcan
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
x : NormalWord d
⊢ unitsSMul φ (-1) (unitsSMul φ 1 x) = x
have rw : x = x
Tactic: rw [unitsSMul_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
w : NormalWord d
⊢ unitsSMul φ 1 (unitsSMul φ (-1) w) = w
have h : Eq (α := ℤˣ) 1 (- -1)
Tactic: convert! unitsSMul_neg _ _ w
-- 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
⊢ unitsSMul φ 1 ((↑g : G) • w) = HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G) (unitsSMul φ 1 w)
have unfold : (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
  else
    let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
    cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) sorry sorry) =
  HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
    (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry)
Tactic: unfold unitsSMul
-- 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
g : ↥A
w : NormalWord d
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
Tactic: have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by
    simp [Cancels, Subgroup.mul_mem_cancel_left]
-- 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
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have pos : ∀ (hcan : Cancels 1 w),
  (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) sorry sorry) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry)
Tactic: by_cases hcan : Cancels 1 w
-- 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
pos :
  ∀ (hcan : Cancels 1 w),
    (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
      HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
        else
          let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
          cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have neg : ∀ (hcan : ¬Cancels 1 w),
  (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) sorry sorry) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry)
Tactic: by_cases hcan : Cancels 1 w
-- 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
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have pos : 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 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) 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 sorry)) : G) w)
        hcan :
      NormalWord d)
Tactic: simp only [unitsSMulWithCancel, toSubgroup_one, id_eq, toSubgroup_neg_one, toSubgroupEquiv_one,
      group_smul_head, mul_inv_rev, dif_pos (this.2 hcan), dif_pos hcan]
-- 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
⊢ 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)
  (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 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) (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 sorry)) : G) w)
          hcan :
        NormalWord d)
Tactic: cases w using consRecOn
Cleared hypotheses: w, this, hcan
-- 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)
⊢ HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) ((↑g : G) * g_1) ⋯)) : 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 ⋯)) : G) w)
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 * Subtype.mk (p := fun (x : G) ↦ x ∈ A) g_1 sorry)) : G) w
Tactic: rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ]
-- 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
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have neg : (let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
  cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) sorry sorry) =
  HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
    (let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
    cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry)
Tactic: rw [dif_neg (mt this.1 hcan), dif_neg hcan]
-- 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
⊢ (let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
    cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
have neg : cons
    (↑((φ : (a : ↥A) → ↥B)
          (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                  G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                (a : G) → ↥A × (↑(d.set 1) : Type u_1))
              ((↑g : G) * w.head)).1) :
      G)
    1
    (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).2 :
          G) *
        w.head⁻¹) •
      w)
    sorry sorry =
  cons
    (HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G))
    1
    (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).2 :
          G) *
        w.head⁻¹) •
      w)
    sorry sorry
Tactic: simp +instances only [toSubgroup_neg_one, unitsSMulGroup, toSubgroup_one, toSubgroupEquiv_one,
      SetLike.coe_sort_coe, group_smul_head, mul_inv_rev, ← mul_smul, mul_assoc, inv_mul_cancel,
      mul_one, smul_cons]
-- 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
⊢ cons
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).1) :
        G)
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  ((↑g : G) * w.head)).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯ =
    cons
      (HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (↑((φ : (a : ↥A) → ↥B)
              (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).1) :
          G))
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯
have neg : (↑((φ : (a : ↥A) → ↥B)
        (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
              (a : G) → ↥A × (↑(d.set 1) : Type u_1))
            ((↑g : G) * w.head)).1) :
    G) =
  HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
    (↑((φ : (a : ↥A) → ↥B)
          (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                  G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                (a : G) → ↥A × (↑(d.set 1) : Type u_1))
              w.head).1) :
      G)
Tactic: congr 1