α : Type u_1
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), get? (a :: l₁) n = get? (a' :: l₂) n
h0 : some a = some a'
⊢ a :: l₁ = a' :: l₂
α : Type u_1
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), get? (a :: l₁) n = get? (a' :: l₂) n
⊢ a :: l₁ = a' :: l₂
have h0 : some a = some a' := h 0
α : Type u_1
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), get? (a :: l₁) n = get? (a' :: l₂) n
aa : a = a'
⊢ a :: l₁ = a' :: l₂
α : Type u_1
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), get? (a :: l₁) n = get? (a' :: l₂) n
h0 : some a = some a'
⊢ a :: l₁ = a' :: l₂
injection h0 with aa
no goals
α : Type u_1
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), get? (a :: l₁) n = get? (a' :: l₂) n
aa : a = a'
⊢ a :: l₁ = a' :: l₂
simp only [aa, ext fun n => h (n+1)]