case nil
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []

case cons
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p l <+ filter q l
induction' l with hd tl IH
no goals
case nil
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []
rfl
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : p hd = true
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)

case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)
case cons
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)
by_cases hp : p hd
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : p hd = true
⊢ hd :: filter p tl <+ hd :: filter q tl
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : p hd = true
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)
rw [filter_cons_of_pos _ hp, filter_cons_of_pos _ (h _ hp)]
no goals
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : p hd = true
⊢ hd :: filter p tl <+ hd :: filter q tl
exact IH.cons_cons hd
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
⊢ filter p tl <+ filter q (hd :: tl)
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
⊢ filter p (hd :: tl) <+ filter q (hd :: tl)
rw [filter_cons_of_neg _ hp]
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : q hd = true
⊢ filter p tl <+ filter q (hd :: tl)

case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ filter p tl <+ filter q (hd :: tl)
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
⊢ filter p tl <+ filter q (hd :: tl)
by_cases hq : q hd
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : q hd = true
⊢ filter p tl <+ hd :: filter q tl
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : q hd = true
⊢ filter p tl <+ filter q (hd :: tl)
rw [filter_cons_of_pos _ hq]
no goals
case pos
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : q hd = true
⊢ filter p tl <+ hd :: filter q tl
exact sublist_cons_of_sublist hd IH
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ filter p tl <+ filter q tl
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ filter p tl <+ filter q (hd :: tl)
rw [filter_cons_of_neg _ hq]
no goals
case neg
ι : Type ?u.380416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
hd : α
tl : List α
IH : filter p tl <+ filter q tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ filter p tl <+ filter q tl
exact IH