case nil
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h✝ : l ≠ []
a✝ : α
h : [] ≠ []
a : α
⊢ drop (length []) [a] = [getLast [] h]

case cons
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
⊢ drop (length (y :: l)) (a :: y :: l) = [getLast (y :: l) h]
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : l ≠ []
a : α
⊢ drop (length l) (a :: l) = [getLast l h]
induction' l with y l ih generalizing a
no goals
case nil
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h✝ : l ≠ []
a✝ : α
h : [] ≠ []
a : α
⊢ drop (length []) [a] = [getLast [] h]
cases h rfl
case cons
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]
case cons
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
⊢ drop (length (y :: l)) (a :: y :: l) = [getLast (y :: l) h]
simp only [drop, length]
case pos
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]

case neg
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]
case cons
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]
by_cases h₁ : l = []
case neg
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast l h₁]
case neg
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]
rw [getLast_cons h₁]
no goals
case neg
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast l h₁]
exact ih h₁ y
no goals
case pos
ι : Type ?u.203942
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
h✝ : l✝ ≠ []
a✝ y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop (length l) (a :: l) = [getLast l h]
h : y :: l ≠ []
a : α
h₁ : l = []
⊢ drop (Nat.add (length l) 0) (y :: l) = [getLast (y :: l) h]
simp [h₁]