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
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)
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 }
⊢ ∃ (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₁ : List.map Prod.fst
      (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').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?,
    (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').head ∈
      toSubgroup A B (-u)
Tactic: refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • 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 : 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)
⊢ 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 }
have cons : 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 φ) *
    ReducedWord.prod φ { head := 1, toList := l, chain := sorry : ReducedWord G A B } =
  ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }
Tactic: rw [prod_smul, hw'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
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)
⊢ ¬Cancels a.1 (a.2 • w')
have simp : a.2 * w'.head ∈ toSubgroup A B a.1 → ∀ (x : G), ¬w'.toList.head? = some (-a.1, x)
Tactic: simp only [Cancels, group_smul_head, group_smul_toList, 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
φ : ↥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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
⊢ False
have hx' : Option.map Prod.fst w'.toList.head? = Option.map Prod.fst (some (-a.1, x))
Tactic: have hx' := congr_arg (Option.map Prod.fst) hx
-- 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
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst w'.toList.head? = Option.map Prod.fst (some (-a.1, x))
⊢ False
have hx'₁ : Option.map Prod.fst { head := 1, toList := l, chain := sorry : ReducedWord G A B }.toList.head? = some (-a.1, x).1
Tactic: rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
Cleared hypotheses: hx'
-- 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
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
⊢ False
have this : w'.head ∈ toSubgroup A B a.1
Tactic: have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ 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
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this : w'.head ∈ toSubgroup A B a.1
⊢ False
have rw : ∀ (hS : a.2 ∈ toSubgroup A B a.1) (x : G) (hx : w'.toList.head? = some (-a.1, x))
  (hx' : Option.map Prod.fst { head := 1, toList := l, chain := sorry : ReducedWord G A B }.toList.head? = some (-a.1, x).1)
  (this : w'.head ∈ toSubgroup A B a.1), False
Tactic: rw [mul_mem_cancel_right this] at hS
Cleared hypotheses: hS, x, hx, hx', this
-- 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
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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this : w'.head ∈ toSubgroup A B a.1
⊢ a.1 = -a.1
have hl : l ≠ []
Tactic: have hl : l ≠ [] := by rintro rfl; 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
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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
⊢ a.1 = -a.1
have this₁ : a.1 = (l.head hl).1
Tactic: have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
-- 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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this_1 : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
this : a.1 = (l.head hl).1
⊢ a.1 = -a.1
have rwa : ∀ (hx' : Option.map Prod.fst (some (l.head hl)) = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
Tactic: rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
Cleared hypotheses: hx', this
-- 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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this_1 : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
this : a.1 = (l.head hl).1
rwa : ∀ (hx' : Option.map Prod.fst (some (l.head hl)) = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
⊢ a.1 = -a.1
have rwa₁ : ∀ (hx' : some (l.head hl).1 = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
Tactic: rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
Cleared hypotheses: hx', this
-- 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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this_1 : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
this : a.1 = (l.head hl).1
rwa : ∀ (hx' : Option.map Prod.fst (some (l.head hl)) = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
rwa₁ : ∀ (hx' : some (l.head hl).1 = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
⊢ a.1 = -a.1
have rwa₂ : ∀ (hx' : some a.1 = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
Tactic: rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
Cleared hypotheses: hx', this
-- 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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this_1 : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
this : a.1 = (l.head hl).1
rwa : ∀ (hx' : Option.map Prod.fst (some (l.head hl)) = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
rwa₁ : ∀ (hx' : some (l.head hl).1 = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
rwa₂ : ∀ (hx' : some a.1 = some (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
⊢ a.1 = -a.1
have rwa₃ : ∀ (hx' : a.1 = (-a.1, x).1) (this : a.1 = (l.head hl).1), a.1 = -a.1
Tactic: rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
Cleared hypotheses: hx', this
-- 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
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)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ : ReducedWord G A B }.toList.head? = some (-a.1, x).1
this : w'.head ∈ toSubgroup A B a.1
⊢ False
have this₁ : a.1 = -a.1
Tactic: have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
-- 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
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)
⊢ List.map Prod.fst
        (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').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?,
      (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').head ∈
        toSubgroup A B (-u)
have this : ¬Cancels a.1 (a.2 • w')
Tactic: have : ¬ Cancels a.1 (a.2 • w') := by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff,
          Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
-- 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
l : List (ℤˣ × G)
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)
have nil : ∀ (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []),
  ∃ (w' : NormalWord d),
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := [], chain := chain } ∧
      List.map Prod.fst w'.toList =
          List.map Prod.fst { head := 1, toList := [], chain := chain : ReducedWord G A B }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := chain : ReducedWord G A B }.toList.head?,
          w'.head ∈ toSubgroup A B (-u)
Tactic: induction l with
  | nil =>
    exact
      ⟨{ head := 1
         toList := []
         mem_set := by simp
         chain := List.isChain_nil }, by simp⟩
  | cons a l ih =>
    rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
    clear ih
    refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
    · rw [prod_smul, hw'1]
      simp [ReducedWord.prod]
    · have : ¬ Cancels a.1 (a.2 • w') := by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff,
          Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
      simp [mul_smul, of_smul_eq_smul, t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]
Cleared hypotheses: l, chain
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = 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 rcases : ∀ (d : TransversalPair G A B),
  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 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
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
⊢ 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 rcases : ∀ (w₁' : NormalWord d) (hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁)
  (hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList)
  (hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)),
  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 exists_normalWord_prod_eq φ d w₁ with ⟨w₁', hw₁'1, hw₁'2, hw₁'3⟩