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
g : HNNExtension G A B φ
w : NormalWord d
of :
  ∀ (g : G) (w : NormalWord d),
    ReducedWord.prod φ
        (HSMul.hSMul (α := HNNExtension G A B φ)
            ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ) w).toReducedWord =
      HMul.hMul (α := HNNExtension G A B φ)
        ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (ReducedWord.prod φ w.toReducedWord)
t :
  ∀ (w : NormalWord d),
    ReducedWord.prod φ (HSMul.hSMul (α := HNNExtension G A B φ) HNNExtension.t w).toReducedWord =
      HNNExtension.t * ReducedWord.prod φ w.toReducedWord
mul :
  ∀ (x y : HNNExtension G A B φ),
    (∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord) →
      (∀ (w : NormalWord d), ReducedWord.prod φ (y • w).toReducedWord = y * ReducedWord.prod φ w.toReducedWord) →
        ∀ (w : NormalWord d),
          ReducedWord.prod φ ((x * y) • w).toReducedWord = x * y * ReducedWord.prod φ w.toReducedWord
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord
have inv : ∀ (x : HNNExtension G A B φ)
  (ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord)
  (w : NormalWord d), ReducedWord.prod φ (x⁻¹ • w).toReducedWord = x⁻¹ * ReducedWord.prod φ w.toReducedWord
Tactic: induction g using induction_on generalizing w with
  | of => simp [of_smul_eq_smul]
  | t => simp [t_smul_eq_unitsSMul, prod_unitsSMul]
  | mul => simp_all [mul_smul, mul_assoc]
  | inv x ih =>
    rw [← mul_right_inj x, ← ih]
    simp
Cleared hypotheses: g, 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 : 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (cons g u w h1 h2).toReducedWord) empty = cons g u w h1 h2
have cons : HSMul.hSMul (β := NormalWord d) g
    (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 u w h1 h2
Tactic: rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]
-- 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 : 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
⊢ HSMul.hSMul (β := NormalWord d) g
      (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 u w h1 h2
have cons : HSMul.hSMul (β := NormalWord d) g
    (let g' := unitsSMulGroup φ d u w.head;
    cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry) =
  cons g u w h1 h2
Tactic: rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
-- 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 : 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
⊢ HSMul.hSMul (β := NormalWord d) g
      (let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2
have cons : cons
    (g *
      (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 sorry)) :
        G))
    u w sorry sorry =
  cons g u w h1 h2
Tactic: simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, 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 : 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
⊢ cons
      (g *
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
          G))
      u w ⋯ ⋯ =
    cons g u w h1 h2
have cons : (cons
      (g *
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 sorry)) :
          G))
      u w sorry sorry).head =
  (cons g u w h1 h2).head
Tactic: ext
-- 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 : 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
cons :
  (NormalWord.cons
        (g *
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
            G))
        u w ⋯ ⋯).head =
    (NormalWord.cons g u w h1 h2).head
⊢ NormalWord.cons
      (g *
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
          G))
      u w ⋯ ⋯ =
    NormalWord.cons g u w h1 h2
have cons₁ : ∀ (i : ℕ) (a : ℤˣ × G),
  getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length)
        (NormalWord.cons
            (g *
              (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                    (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 sorry)) :
                G))
            u w sorry sorry).toList
        i =
      some a ↔
    getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length) (NormalWord.cons g u w h1 h2).toList i = some a
Tactic: ext
-- 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
w : NormalWord d
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
have ofGroup : ∀ (g : G), HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))) empty = ofGroup g
Tactic: induction w using consRecOn with
  | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
  | cons g u w h1 h2 ih =>
    rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]
    rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
    -- Before https://github.com/leanprover/lean4/pull/2644, this was just
    -- simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
    --   -SetLike.coe_sort_coe]
    -- ext <;> simp [-SetLike.coe_sort_coe]
    simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]
    ext <;> simp
Cleared hypotheses: 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
w : NormalWord d
ofGroup :
  ∀ (g : G),
    HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (toReducedWord (d := d) (NormalWord.ofGroup g))) empty =
      NormalWord.ofGroup g
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
have cons : ∀ (g : 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')
  (ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w),
  HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (cons g u w h1 h2).toReducedWord) empty = cons g u w h1 h2
Tactic: induction w using consRecOn with
  | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
  | cons g u w h1 h2 ih =>
    rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]
    rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
    -- Before https://github.com/leanprover/lean4/pull/2644, this was just
    -- simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
    --   -SetLike.coe_sort_coe]
    -- ext <;> simp [-SetLike.coe_sort_coe]
    simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]
    ext <;> simp
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
⊢ Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)
have rcases : ∀ (d : TransversalPair G A B),
  Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)
Tactic: rcases TransversalPair.nonempty G A B with ⟨d⟩
-- 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
⊢ Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)
have refine : Injective.{u_1 + 1, u_1 + 1} (α := G) (β := NormalWord d → NormalWord d)
  ((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ))
Tactic: refine Function.Injective.of_comp
    (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_
-- 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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
have pos : ∀ (hw1 : w.head = 1),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
Tactic: by_cases hw1 : w.head = 1
-- 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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
pos :
  ∀ (hw1 : w.head = 1),
    ∃ (w' : NormalWord d),
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
        List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
          ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
have neg : ∀ (hw1 : ¬w.head = 1),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
Tactic: by_cases hw1 : w.head = 1
-- 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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : w.head = 1
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
have pos : ∃ (w' : NormalWord d),
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
    List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
      ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
Tactic: simp only [hw1, inv_mem_iff, mul_one]
-- 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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ (w' : NormalWord d),
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
have neg : ∀ (w' : NormalWord d)
  (hw' :
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := sorry } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := w.toList, chain := sorry : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := sorry : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
Tactic: rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩
-- 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
w : ReducedWord G A B
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
have suffices : ∀ (w : ReducedWord G A B),
  w.head = 1 →
    ∃ (w' : NormalWord d),
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
        List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
          ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
Tactic: suffices ∀ w : ReducedWord G A B,
      w.head = 1 → ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧
      w'.toList.map Prod.fst = w.toList.map Prod.fst ∧
      ∀ u ∈ w.toList.head?.map Prod.fst,
      w'.head ∈ toSubgroup A B (-u) by
    by_cases hw1 : w.head = 1
    · simp only [hw1, inv_mem_iff, mul_one]
      exact this w hw1
    · rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩
      exact ⟨w.head • w', by
        simpa [ReducedWord.prod, mul_assoc] using hw'⟩
-- 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
w_1 w : ReducedWord G A B
hw1 : w.head = 1
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
have rcases : ∀ (g : G) (l : List (ℤˣ × G)) (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l)
  (hw1 : { head := g, toList := l, chain := chain : ReducedWord G A B }.head = 1),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
Tactic: rcases w with ⟨g, l, chain⟩
Cleared hypotheses: w, hw1
-- 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
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : g = 1
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
have subst : ∃ (w' : NormalWord d),
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := chain } ∧
    List.map Prod.fst w'.toList =
        List.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
Tactic: subst hw1
Cleared hypotheses: g, hw1
-- 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
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
ih :
  ∀ (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l),
    ∃ (w' : NormalWord d),
      ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := chain } ∧
        List.map Prod.fst w'.toList =
            List.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList ∧
          ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := chain : ReducedWord G A B }.toList.head?,
            w'.head ∈ toSubgroup A B (-u)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
have cons : ∀ (w' : NormalWord d)
  (hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := sorry })
  (hw'2 :
    List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := sorry : ReducedWord G A B }.toList)
  (hw'3 :
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := sorry : ReducedWord G A B }.toList.head?,
      w'.head ∈ toSubgroup A B (-u)),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
Tactic: rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
-- 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
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList
hw'3 :
  ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head?,
    w'.head ∈ toSubgroup A B (-u)
⊢ ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
have cons : ReducedWord.prod φ
    (HMul.hMul (β := HNNExtension G A B φ) (HPow.hPow (α := HNNExtension G A B φ) t (↑a.1 : ℤ))
          ((of : (a : G) → HNNExtension G A B φ) a.2 : HNNExtension G A B φ) •
        w').toReducedWord =
  ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }
Tactic: refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩