α : Type u_1
a : α
s₁ : List α
b : α
s₂ t₁ t₂ : List α
hl : length (a :: s₁) = length (b :: s₂)
h : a = b
⊢ a = b
α : Type u_1
a : α
s₁ : List α
b : α
s₂ t₁ t₂ : List α
h : a :: s₁ ++ t₁ = b :: s₂ ++ t₂
hl : length (a :: s₁) = length (b :: s₂)
⊢ a :: s₁ = b :: s₂ ∧ t₁ = t₂
simp [append_inj (cons.inj h).2 (Nat.succ.inj hl)] at h ⊢
no goals
α : Type u_1
a : α
s₁ : List α
b : α
s₂ t₁ t₂ : List α
hl : length (a :: s₁) = length (b :: s₂)
h : a = b
⊢ a = b
exact h