-- Mathlib/GroupTheory/PushoutI.lean
theorem ext {w₁ w₂ : NormalWord d} (hhead : w₁.head = w₂.head)
    (hlist : w₁.toList = w₂.toList) : w₁ = w₂

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
w₁ w₂ : NormalWord d
hhead : w₁.head = w₂.head
hlist : w₁.toList = w₂.toList
⊢ w₁ = w₂

Tactic:
rcases w₁ with ⟨⟨_, _, _⟩, _, _⟩

Result:
case mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
w₂ : NormalWord d
head✝ : H
toList✝ : List ((i : ι) × G i)
ne_one✝ : ∀ l ∈ toList✝, l.snd ≠ 1
chain_ne✝ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝
normalized✝ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList → g ∈ d.set i
hhead :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.head =
    w₂.head
hlist :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.toList =
    w₂.toList
⊢ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ } = w₂

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
head✝¹ : H
toList✝¹ : List ((i : ι) × G i)
ne_one✝¹ : ∀ l ∈ toList✝¹, l.snd ≠ 1
chain_ne✝¹ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝¹
normalized✝¹ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹ }.toList → g ∈ d.set i
head✝ : H
toList✝ : List ((i : ι) × G i)
ne_one✝ : ∀ l ∈ toList✝, l.snd ≠ 1
chain_ne✝ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝
normalized✝ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList → g ∈ d.set i
hhead :
  { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹, normalized := normalized✝¹ }.head =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.head
hlist :
  { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹,
        normalized := normalized✝¹ }.toList =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.toList
⊢ { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹, normalized := normalized✝¹ } =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
w₂ : NormalWord d
head✝ : H
toList✝ : List ((i : ι) × G i)
ne_one✝ : ∀ l ∈ toList✝, l.snd ≠ 1
chain_ne✝ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝
normalized✝ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList → g ∈ d.set i
hhead :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.head =
    w₂.head
hlist :
  { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.toList =
    w₂.toList
⊢ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ } = w₂

Tactic:
rcases w₂ with ⟨⟨_, _, _⟩, _, _⟩

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
head✝¹ : H
toList✝¹ : List ((i : ι) × G i)
ne_one✝¹ : ∀ l ∈ toList✝¹, l.snd ≠ 1
chain_ne✝¹ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝¹
normalized✝¹ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹ }.toList → g ∈ d.set i
head✝ : H
toList✝ : List ((i : ι) × G i)
ne_one✝ : ∀ l ∈ toList✝, l.snd ≠ 1
chain_ne✝ : Chain' (fun l l' => l.fst ≠ l'.fst) toList✝
normalized✝ :
  ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList → g ∈ d.set i
hhead :
  { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹, normalized := normalized✝¹ }.head =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.head
hlist :
  { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹,
        normalized := normalized✝¹ }.toList =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }.toList
⊢ { toList := toList✝¹, ne_one := ne_one✝¹, chain_ne := chain_ne✝¹, head := head✝¹, normalized := normalized✝¹ } =
    { toList := toList✝, ne_one := ne_one✝, chain_ne := chain_ne✝, head := head✝, normalized := normalized✝ }