-- Mathlib/GroupTheory/HNNExtension.lean
theorem ext {w w' : NormalWord d}
    (h1 : w.head = w'.head) (h2 : w.toList = w'.toList) : w = w'

Proof state:
case mk.mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
h1 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.head = w'.head
h2 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.toList = w'.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ } = w'

Tactic:
cases w'

Result:
case mk.mk.mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝¹ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
toReducedWord✝ : ReducedWord G A B
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord✝.toList → g ∈ d.set u
h1 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.head =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.head
h2 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.toList =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ } =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }

Proof state:
case mk.mk.mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝¹ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
toReducedWord✝ : ReducedWord G A B
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord✝.toList → g ∈ d.set u
h1 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.head =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.head
h2 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.toList =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ } =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }

Tactic:
simp_all

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w w' : NormalWord d
h1 : w.head = w'.head
h2 : w.toList = w'.toList
⊢ w = w'

Tactic:
rcases w with ⟨⟨⟩, _⟩

Result:
case mk.mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
h1 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.head = w'.head
h2 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.toList = w'.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ } = w'