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

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

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