Theorem: List.getLast?_some (One.lean)

State before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
⊢ l ≠ []
Tactic:
have h₂:= congr_arg Option.isSome h
State after:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ l ≠ []

State before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ l ≠ []
Tactic:
simp at h₂
State after:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ l ≠ []

State before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ l ≠ []
Tactic:
simp [h₂]
State after:
no goals

State before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
⊢ getLast l (_ : ¬l = []) = a
Tactic:
have h₂:= congr_arg Option.isSome h
State after:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ getLast l (_ : ¬l = []) = a

State before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ getLast l (_ : ¬l = []) = a
Tactic:
simp only [Option.isSome_some, getLast?_isSome, ne_eq] at h₂
State after:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ getLast l (_ : ¬l = []) = a

State before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ getLast l (_ : ¬l = []) = a
Tactic:
rw [ List.getLast?_eq_getLast l h₂] at h
State after:
α : Type u_1
l : List α
a : α
h✝ : getLast? l = some a
h₂ : ¬l = []
h : some (getLast l h₂) = some a
⊢ getLast l (_ : ¬l = []) = a

State before:
α : Type u_1
l : List α
a : α
h✝ : getLast? l = some a
h₂ : ¬l = []
h : some (getLast l h₂) = some a
⊢ getLast l (_ : ¬l = []) = a
Tactic:
simp_all only [Option.some.injEq]
State after:
no goals