-- Mathlib/GroupTheory/HNNExtension.lean
theorem map_fst_eq_and_of_prod_eq {w₁ w₂ : ReducedWord G A B}
    (hprod : w₁.prod φ = w₂.prod φ) :
    w₁.toList.map Prod.fst = w₂.toList.map Prod.fst ∧
     ∀ u ∈ w₁.toList.head?.map Prod.fst,
      w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
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)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?

Tactic:
rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
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)

Tactic:
subst this

Result:
case intro.intro.intro.intro.intro.intro.intro
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)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
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)

Tactic:
refine ⟨by rw [← hw₁'2, hw₂'2], ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
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)