case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs ↔ bs = cs
α : Type u_1
as bs cs : List α
⊢ (as ++ bs = as ++ cs) = (bs = cs)
apply propext
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs
case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs ↔ bs = cs
apply Iff.intro
case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs
next => apply append_cancel_left
no goals
case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs
next => intro h; simp [h]
no goals
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs
apply append_cancel_left
α : Type u_1
as bs cs : List α
h : bs = cs
⊢ as ++ bs = as ++ cs
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs
intro h
no goals
α : Type u_1
as bs cs : List α
h : bs = cs
⊢ as ++ bs = as ++ cs
simp [h]