no goals
α : Type u_1
as bs cs : List α
h : as ++ bs = cs ++ bs
⊢ as = cs
match as, cs with
| [], []       => rfl
| [], c::cs    => have aux := congrArg length h; simp_arith at aux
| a::as, []    => have aux := congrArg length h; simp_arith at aux
| a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
no goals
α : Type u_1
as bs cs : List α
h : [] ++ bs = [] ++ bs
⊢ [] = []
rfl
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
aux : length ([] ++ bs) = length (c :: cs ++ bs)
⊢ [] = c :: cs
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
⊢ [] = c :: cs
have aux := congrArg length h
no goals
α : Type u_1
as bs cs✝ : List α
c : α
cs : List α
h : [] ++ bs = c :: cs ++ bs
aux : length ([] ++ bs) = length (c :: cs ++ bs)
⊢ [] = c :: cs
simp_arith at aux
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
aux : length (a :: as ++ bs) = length ([] ++ bs)
⊢ a :: as = []
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
⊢ a :: as = []
have aux := congrArg length h
no goals
α : Type u_1
as✝ bs cs : List α
a : α
as : List α
h : a :: as ++ bs = [] ++ bs
aux : length (a :: as ++ bs) = length ([] ++ bs)
⊢ a :: as = []
simp_arith at aux
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h₁ : a = c
h₂ : List.append as bs = List.append cs bs
⊢ a :: as = c :: cs
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h : a :: as ++ bs = c :: cs ++ bs
⊢ a :: as = c :: cs
injection h with h₁ h₂
α : Type u_1
as✝ bs cs✝ : List α
a : α
as cs : List α
h₂ : List.append as bs = List.append cs bs
⊢ a :: as = a :: cs
α : Type u_1
as✝ bs cs✝ : List α
a : α
as : List α
c : α
cs : List α
h₁ : a = c
h₂ : List.append as bs = List.append cs bs
⊢ a :: as = c :: cs
subst h₁
no goals
α : Type u_1
as✝ bs cs✝ : List α
a : α
as cs : List α
h₂ : List.append as bs = List.append cs bs
⊢ a :: as = a :: cs
rw [append_cancel_right h₂]