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
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
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)
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⟩
-- 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
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)
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)
⊢ ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂'.toReducedWord
have rw : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂'.toReducedWord
Tactic: rw [hw₁'1, hw₂'1, hprod]
-- 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
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)
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)
rw : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂'.toReducedWord
rw₁ : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
⊢ ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂'.toReducedWord
have rw₂ : ReducedWord.prod φ w₂ = ReducedWord.prod φ w₂
Tactic: rw [hw₁'1, hw₂'1, hprod]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
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)
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)
have this : w₁' = w₂'
Tactic: have : w₁' = w₂' :=
    NormalWord.prod_injective φ d (by dsimp only; rw [hw₁'1, hw₂'1, hprod])
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
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)
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)
this : w₁' = 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 hw₂'1₁ : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
Tactic: subst this
Cleared hypotheses: w₂', hw₂'1, hw₂'2, hw₂'3, this
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
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)
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)
this : w₁' = w₂'
hw₂'1₁ : 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 hw₂'2₁ : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
Tactic: subst this
Cleared hypotheses: w₂', hw₂'1, hw₂'2, hw₂'3, this
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
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)
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)
this : w₁' = w₂'
hw₂'1₁ : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2₁ : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
⊢ 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 hw₂'3₁ : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
Tactic: subst this
Cleared hypotheses: w₂', hw₂'1, hw₂'2, hw₂'3, this
-- 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
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)
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)
rw : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
⊢ List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList
have rw₁ : List.map Prod.fst w₂.toList = List.map Prod.fst w₂.toList
Tactic: rw [← hw₁'2, hw₂'2]
-- 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
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)
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)
have refine : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
Tactic: refine ⟨by rw [← hw₁'2, hw₂'2], ?_⟩
-- 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
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)
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)
⊢ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
have simp : ∀
  (hw₁'3 :
    ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
      w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G))
  (hw₂'3 :
    ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
      w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)),
  ∀ u ∈ Option.map Prod.fst w₁.toList.head?,
    w₁.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
Tactic: simp only [← leftCoset_eq_iff] at *
Cleared hypotheses: hw₁'3, 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
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
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₂'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 • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ w₁.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
have rw : u ∈ Option.map Prod.fst w₂.toList.head?
Tactic: rw [← hw₁'3 _ hu, ← 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
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
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₂'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 • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?
have rwa : u ∈ (List.map Prod.fst w₂.toList).head?
Tactic: rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]
-- 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
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₂'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 • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
rwa : u ∈ (List.map Prod.fst w₂.toList).head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?
have rwa₁ : u ∈ (List.map Prod.fst w₁'.toList).head?
Tactic: rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]
-- 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
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₂'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 • (↑(toSubgroup A B (-u)) : Set G) = w₁.head • (↑(toSubgroup A B (-u)) : Set G)
hw₂'3 :
  ∀ u ∈ Option.map Prod.fst w₂.toList.head?,
    w₁'.head • (↑(toSubgroup A B (-u)) : Set G) = w₂.head • (↑(toSubgroup A B (-u)) : Set G)
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
rwa : u ∈ (List.map Prod.fst w₂.toList).head?
rwa₁ : u ∈ (List.map Prod.fst w₁'.toList).head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?
have rwa₂ : u ∈ (List.map Prod.fst w₁.toList).head?
Tactic: rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
hw : Membership.mem (γ := Subgroup (HNNExtension G A B φ)) (MonoidHom.range of) (ReducedWord.prod φ w)
⊢ w.toList = []
have rcases : ∀ (g : G) (hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w), w.toList = []
Tactic: rcases hw with ⟨g, hg⟩
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : (of : (a : G) → HNNExtension G A B φ) g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ w.toList = []
have this : ReducedWord.prod φ w = ReducedWord.prod φ w'
Tactic: have : w.prod φ = w'.prod φ := by simp [w', ReducedWord.prod, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
⊢ ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
have simp : ∀ (x y : G'),
  x⁻¹ * y ∈ comap f H ↔ HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G) ∈ H
Tactic: simp only [QuotientGroup.leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x y : G'
⊢ (f : (a : G') → G) (x⁻¹ * y) = HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
have rw : HMul.hMul (α := G) (β := G) ((f : (a : G') → G) x⁻¹ : G) ((f : (a : G') → G) y : G) =
  HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
Tactic: rw [f.map_mul, f.map_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x y : G'
rw :
  HMul.hMul (α := G) (β := G) ((f : (a : G') → G) x⁻¹ : G) ((f : (a : G') → G) y : G) =
    HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
⊢ (f : (a : G') → G) (x⁻¹ * y) = HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
have rw₁ : HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G) =
  HMul.hMul (α := G) (β := G) (((f : (a : G') → G) x)⁻¹ : G) ((f : (a : G') → G) y : G)
Tactic: rw [f.map_mul, f.map_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
⊢ (comap f H).index = H.index
have key : ∀ (x y : G'),
  (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
    (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
Tactic: have key : ∀ x y : G',
      QuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) := by
    simp only [QuotientGroup.leftRel_apply]
    exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ (comap f H).index = H.index
have refine_1 : Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) sorry)
Tactic: refine Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
refine_1 : Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
⊢ (comap f H).index = H.index
have refine_2 : Surjective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) sorry)
Tactic: refine Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
have key₁ : ∀ (x y : G'),
  Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
    Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
      (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
      (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
Tactic: simp_rw [← Quotient.eq''] at key
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
⊢ Injective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
have refine_1 : ∀ (x : G') ⦃a₂ : G' ⧸ comap f H⦄,
  Eq.{u_1 + 1} (α := G ⧸ H)
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) sorry (Quotient.mk'' x))
      (Quotient.map' (⇑f : (a : G') → G) sorry a₂) →
    Quotient.mk'' x = a₂
Tactic: refine Quotient.ind' fun x => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key_1 :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
key :
  ∀ (x y : G'),
    Eq (α := Quotient (QuotientGroup.leftRel (comap f H))) (Quotient.mk'' x) (Quotient.mk'' y) ↔
      Eq.{u_1 + 1} (α := Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) x) : Quotient (QuotientGroup.leftRel H))
        (Quotient.mk'' ((f : (a : G') → G) y) : Quotient (QuotientGroup.leftRel H))
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Eq.{u_1 + 1} (α := G ⧸ H)
        (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) ⋯ (Quotient.mk'' x))
        (Quotient.map' (⇑f : (a : G') → G) ⋯ a₂) →
      Quotient.mk'' x = a₂
have refine_1 : ∀ (y : G'),
  Eq.{u_1 + 1} (α := G ⧸ H)
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) sorry (Quotient.mk'' x))
      (Quotient.map' (s₁ := QuotientGroup.leftRel (comap f H)) (⇑f : (a : G') → G) sorry (Quotient.mk'' y)) →
    Eq (α := G' ⧸ comap f H) (Quotient.mk'' x) (Quotient.mk'' y)
Tactic: refine Quotient.ind' fun y => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective.{u_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := G' ⧸ comap f H) (β := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯)
have refine_2 : ∀ (x : G), ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) sorry a) (Quotient.mk'' x)
Tactic: refine Quotient.ind' fun x => ?_