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
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ (g : G) → Cancels (A := A) (B := B) (d := d) u (ofGroup g) → NormalWord d
have simp : (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d
Tactic: simp [Cancels, ofGroup]
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
⊢ ∀ u' ∈ Option.map Prod.fst (((↑g'.2 : G) * w.head⁻¹) • w).toList.head?,
    (((↑g'.2 : G) * w.head⁻¹) • w).head ∈ toSubgroup A B u → u = u'
have simp : ∀ (u' : ℤˣ) (x : G) (h : w.toList.head? = some (u', x)),
  (↑((sorry.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).2 :
        G) ∈
      toSubgroup A B u →
    u = u'
Tactic: simp only [g', group_smul_toList, Option.mem_def, Option.map_eq_some_iff, Prod.exists,
          exists_and_right, exists_eq_right, group_smul_head, inv_mul_cancel_right,
          forall_exists_index, unitsSMulGroup]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
⊢ ∀ (u' : ℤˣ) (x : G) (h : w.toList.head? = some (u', x)),
    (↑((⋯.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).2 :
          G) ∈
        toSubgroup A B u →
      u = u'
have h₁ : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
Tactic: simp only [Cancels, Option.map_eq_some_iff, Prod.exists, exists_and_right, exists_eq_right,
          not_and, not_exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u
have this₁ : RightCosetEquivalence (↑(toSubgroup A B u) : Set G) w.head
  (↑((sorry.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).2 :
    G)
Tactic: have := (d.compl u).rightCosetEquivalence_equiv_snd w.head
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this :
  RightCosetEquivalence (↑(toSubgroup A B u) : Set G) w.head
    (↑((⋯.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).2 :
      G)
⊢ w.head ∈ toSubgroup A B u
have this₁ : w.head⁻¹ ∈ toSubgroup A B u
Tactic: rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
⊢ u = u'
have this₁ : w.head ∈ toSubgroup A B u
Tactic: have : w.head ∈ toSubgroup A B u := by
          have := (d.compl u).rightCosetEquivalence_equiv_snd w.head
          rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this
          simp_all
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this : w.head ∈ toSubgroup A B u
⊢ u = u'
have this₁ : ¬w.toList.head? = some (-u, x)
Tactic: have := h this x
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ¬Cancels u w
have simp : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
Tactic: simp only [Cancels, Option.map_eq_some_iff, Prod.exists,
    exists_and_right, exists_eq_right, not_and, not_exists]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
⊢ False
have h2₁ : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
Tactic: rw [hx] at h2
Cleared hypotheses: h2, hx
-- 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
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
have pos : ∀ (h : Cancels u w), Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
Tactic: by_cases h : Cancels u 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
u : ℤˣ
w : NormalWord d
pos : ∀ (h : Cancels u w), Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
have neg : ∀ (h : ¬Cancels u w), Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
Tactic: by_cases h : Cancels u 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
u : ℤˣ
w : NormalWord d
h : Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
have pos : ¬Cancels (-u) (unitsSMulWithCancel φ u w sorry)
Tactic: simp only [unitsSMul, h, dite_true, not_true_eq_false, iff_false]
-- 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 : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
h_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
⊢ False
have pos : Cancels u' w
Tactic: apply not_cancels_of_cons_hyp _ _ h2
-- 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
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
h_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
⊢ Cancels u' w
have h₁ : g ∈ toSubgroup A B u ∧ u' = -u
Tactic: simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h
-- 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 : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
h_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h_2 : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
h : g ∈ toSubgroup A B u ∧ u' = -u
⊢ Cancels u' w
have pos : ∀ (h1 : w.head ∈ d.set (-u)) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B (-u) → -u = u')
  (h : Cancels u (cons g (-u) w h1 h2)) (hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g (-u) w h1 h2) sorry))
  (h : g ∈ toSubgroup A B u ∧ -u = -u), Cancels (-u) w
Tactic: cases h.2
Cleared hypotheses: u', h1, h2, h_2, hc, h
-- 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
h : Cancels u w
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
have pos : ∀ (g : G) (h : Cancels (A := A) (B := B) (d := d) u (ofGroup g)), ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) sorry)
Tactic: induction w using consRecOn with
    | ofGroup => simp [Cancels, unitsSMulWithCancel]
    | cons g u' w h1 h2 _ =>
      intro hc
      apply not_cancels_of_cons_hyp _ _ h2
      simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h
      cases h.2
      simpa [Cancels, unitsSMulWithCancel,
        Subgroup.mul_mem_cancel_left] using hc
Cleared hypotheses: w, h
-- 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
h : Cancels u w
pos :
  ∀ (g : G) (h : Cancels (A := A) (B := B) (d := d) u (ofGroup g)),
    ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) ⋯)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
have pos₁ : ∀ (g : G) (u' : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u')
  (h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1),
  (∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w sorry)) →
    ∀ (h : Cancels u (cons g u' w h1 h2)), ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) sorry)
Tactic: induction w using consRecOn with
    | ofGroup => simp [Cancels, unitsSMulWithCancel]
    | cons g u' w h1 h2 _ =>
      intro hc
      apply not_cancels_of_cons_hyp _ _ h2
      simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h
      cases h.2
      simpa [Cancels, unitsSMulWithCancel,
        Subgroup.mul_mem_cancel_left] using hc
Cleared hypotheses: w, h
-- 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
h : ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
have neg : Cancels (-u)
    (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) sorry sorry) ↔
  ¬Cancels u w
Tactic: simp only [unitsSMul, dif_neg h]
-- 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
⊢ (if h : Cancels (-u) (unitsSMul φ u w) then unitsSMulWithCancel φ (-u) (unitsSMul φ u w) h
    else
      let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
      cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
have pos : ∀ (hcan : Cancels (-u) (unitsSMul φ u w)), unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w
Tactic: split_ifs with 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
u : ℤˣ
w : NormalWord d
pos : ∀ (hcan : Cancels (-u) (unitsSMul φ u w)), unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w
⊢ (if h : Cancels (-u) (unitsSMul φ u w) then unitsSMulWithCancel φ (-u) (unitsSMul φ u w) h
    else
      let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
      cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
have neg : ∀ (hcan : ¬Cancels (-u) (unitsSMul φ u w)),
  (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) sorry sorry) =
    w
Tactic: split_ifs with hcan
-- 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 : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w
have hncan : ¬Cancels u w
Tactic: have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 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
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-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) ⋯ ⋯)
      hcan =
    w
have pos : unitsSMulWithCancel φ (-u)
    (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) sorry sorry) sorry =
  w
Tactic: simp only [dif_neg hncan]
-- 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 : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
have hcan2 : Cancels u w
Tactic: have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 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
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
hcan2 : Cancels u w
⊢ (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
have neg : (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) :=
    unitsSMulGroup φ d (-u)
      (ReducedWord.head (A := A) (B := B)
        (toReducedWord (d := d)
          (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) sorry sorry)));
  cons (↑g'.1 : G) (-u)
    (HSMul.hSMul (β := NormalWord d)
      ((↑g'.2 : G) *
        (ReducedWord.head (A := A) (B := B)
            (toReducedWord (d := d)
              (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) sorry sorry)))⁻¹)
      (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) sorry sorry))
    sorry sorry) =
  w
Tactic: unfold unitsSMul at 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
u : ℤˣ
w : NormalWord d
hcan :
  ¬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
⊢ (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) :=
      unitsSMulGroup φ d (-u)
        (ReducedWord.head (A := A) (B := B)
          (toReducedWord (d := d)
            (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) ⋯ ⋯)));
    cons (↑g'.1 : G) (-u)
      (HSMul.hSMul (β := NormalWord d)
        ((↑g'.2 : G) *
          (ReducedWord.head (A := A) (B := B)
              (toReducedWord (d := d)
                (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) ⋯ ⋯)))⁻¹)
        (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) ⋯ ⋯))
      ⋯ ⋯) =
    w
have neg : ∀ (hcan_1 : ¬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)
      sorry sorry =
    w
Tactic: simp only [dif_pos hcan2] at 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
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
      ⋯ ⋯ =
    cons g u' w h1 h2
have neg : 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)) sorry :
                (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 sorry)) :
                  G) *
                w.head)).1) :
      G)
    (-u)
    (((↑((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) sorry :
                  (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 sorry)) :
                    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 sorry)) :
              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 sorry)) :
          G)
        w)
    sorry sorry =
  cons g u' w h1 h2
Tactic: simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, id_eq, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]