ι : Type ?u.33399
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
a : α
⊢ getLast (replicate m a ++ [a]) (_ : replicate m a ++ [a] ≠ []) = a
ι : Type ?u.33399
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
a : α
⊢ getLast (replicate (m + 1) a) (_ : replicate (m + 1) a ≠ []) = a
simp only [replicate_succ']
no goals
ι : Type ?u.33399
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
a : α
⊢ getLast (replicate m a ++ [a]) (_ : replicate m a ++ [a] ≠ []) = a
exact getLast_append_singleton _