case nil
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
hl : [] ≠ []
⊢ getLast (map f []) (_ : ¬map f [] = []) = f (getLast [] hl)

case cons
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd : α
l_tl : List α
l_ih : ∀ (hl : l_tl ≠ []), getLast (map f l_tl) (_ : ¬map f l_tl = []) = f (getLast l_tl hl)
hl : l_hd :: l_tl ≠ []
⊢ getLast (map f (l_hd :: l_tl)) (_ : ¬map f (l_hd :: l_tl) = []) = f (getLast (l_hd :: l_tl) hl)
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl : l ≠ []
⊢ getLast (map f l) (_ : ¬map f l = []) = f (getLast l hl)
induction' l with l_hd l_tl l_ih
no goals
case nil
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
hl : [] ≠ []
⊢ getLast (map f []) (_ : ¬map f [] = []) = f (getLast [] hl)
apply (hl rfl).elim
case cons.nil
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd : α
l_ih : ∀ (hl : [] ≠ []), getLast (map f []) (_ : ¬map f [] = []) = f (getLast [] hl)
hl : [l_hd] ≠ []
⊢ getLast (map f [l_hd]) (_ : ¬map f [l_hd] = []) = f (getLast [l_hd] hl)

case cons.cons
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd head✝ : α
tail✝ : List α
l_ih :
  ∀ (hl : head✝ :: tail✝ ≠ []),
    getLast (map f (head✝ :: tail✝)) (_ : ¬map f (head✝ :: tail✝) = []) = f (getLast (head✝ :: tail✝) hl)
hl : l_hd :: head✝ :: tail✝ ≠ []
⊢ getLast (map f (l_hd :: head✝ :: tail✝)) (_ : ¬map f (l_hd :: head✝ :: tail✝) = []) =
    f (getLast (l_hd :: head✝ :: tail✝) hl)
case cons
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd : α
l_tl : List α
l_ih : ∀ (hl : l_tl ≠ []), getLast (map f l_tl) (_ : ¬map f l_tl = []) = f (getLast l_tl hl)
hl : l_hd :: l_tl ≠ []
⊢ getLast (map f (l_hd :: l_tl)) (_ : ¬map f (l_hd :: l_tl) = []) = f (getLast (l_hd :: l_tl) hl)
cases l_tl
no goals
case cons.nil
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd : α
l_ih : ∀ (hl : [] ≠ []), getLast (map f []) (_ : ¬map f [] = []) = f (getLast [] hl)
hl : [l_hd] ≠ []
⊢ getLast (map f [l_hd]) (_ : ¬map f [l_hd] = []) = f (getLast [l_hd] hl)
simp
no goals
case cons.cons
ι : Type ?u.138776
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
hl✝ : l ≠ []
l_hd head✝ : α
tail✝ : List α
l_ih :
  ∀ (hl : head✝ :: tail✝ ≠ []),
    getLast (map f (head✝ :: tail✝)) (_ : ¬map f (head✝ :: tail✝) = []) = f (getLast (head✝ :: tail✝) hl)
hl : l_hd :: head✝ :: tail✝ ≠ []
⊢ getLast (map f (l_hd :: head✝ :: tail✝)) (_ : ¬map f (l_hd :: head✝ :: tail✝) = []) =
    f (getLast (l_hd :: head✝ :: tail✝) hl)
simpa using l_ih _