ι : Type ?u.24511
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
h : concat l₁ a = concat l₂ a
⊢ l₁ = l₂
ι : Type ?u.24511
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
⊢ concat l₁ a = concat l₂ a → l₁ = l₂
intro h
ι : Type ?u.24511
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [a]
⊢ l₁ = l₂
ι : Type ?u.24511
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
h : concat l₁ a = concat l₂ a
⊢ l₁ = l₂
rw [concat_eq_append, concat_eq_append] at h
no goals
ι : Type ?u.24511
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [a]
⊢ l₁ = l₂
exact append_right_cancel h