-- Mathlib/Data/List/Basic.lean
theorem monotone_filter_right (l : List α) ⦃p q : α → Bool⦄
    (h : ∀ a, p a → q a) : l.filter p <+ l.filter q

Proof state:
case nil
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p l <+ filter q l

Tactic:
induction' l with hd tl IH

Result:
case nil
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []

case cons
α : Type u
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)

Proof state:
case neg
α : Type u
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)

Tactic:
by_cases hq : q hd

Result:
case pos
α : Type u
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
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)

Proof state:
case pos
α : Type u
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

Tactic:
exact sublist_cons_of_sublist hd IH

Result:
no goals

Proof state:
case pos
α : Type u
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)

Tactic:
rw [filter_cons_of_pos hp, filter_cons_of_pos (h _ hp)]

Result:
case pos
α : Type u
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

Proof state:
case pos
α : Type u
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

Tactic:
exact IH.cons_cons hd

Result:
no goals

Proof state:
case neg
α : Type u
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

Tactic:
exact IH

Result:
no goals

Proof state:
case neg
α : Type u
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)

Tactic:
rw [filter_cons_of_neg hp]

Result:
case neg
α : Type u
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)

Proof state:
case pos
α : Type u
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)

Tactic:
rw [filter_cons_of_pos hq]

Result:
case pos
α : Type u
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

Proof state:
case neg
α : Type u
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)

Tactic:
rw [filter_cons_of_neg hq]

Result:
case neg
α : Type u
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

Proof state:
case cons
α : Type u
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)

Tactic:
by_cases hp : p hd

Result:
case pos
α : Type u
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
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)