Theorem: List.getLast_filter (LeanCamCombi/Mathlib/Data/List/Basic.lean)

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p ([a].getLast ⋯) = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯
Tactic:
rw [List.getLast_singleton'] at h'
State after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p a = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p a = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯
Tactic:
simp [List.filter_cons, h']
State after:
no goals

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((a :: b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (a :: b :: as).getLast ⋯
Tactic:
rw [List.getLast_cons_cons] at h' ⊢
State after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯
Tactic:
simp only [List.filter_cons (x := a)] at h ⊢
State after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
obtain ha | ha := Bool.eq_false_or_eq_true (p a)
State after:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = false
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

State before:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
simp only [ha, ite_true]
State after:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (a :: filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

State before:
case inl
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (a :: filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
rw [getLast_cons, getLast_filter (b :: as) _ h']
State after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ filter p (b :: as) ≠ []

State before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ filter p (b :: as) ≠ []
Tactic:
exact ne_nil_of_mem $ mem_filter.2 ⟨getLast_mem _, h'⟩
State after:
no goals

State before:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = false
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
simp only [ha, cond_false] at h ⊢
State after:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
ha : p a = false
h : (if False then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if False then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

State before:
case inr
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h✝ : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
ha : p a = false
h : (if False then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if False then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
Tactic:
exact getLast_filter (b :: as) h h'
State after:
no goals