-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Count.lean
theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
s✝ : l₁ <+ l₂
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
⊢ countP p (a :: l₂✝) - ((a :: l₂✝).length - (a :: l₁✝).length) ≤ countP p (a :: l₁✝)

Tactic:
rename_i l₁ l₂

Result:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
⊢ countP p (a :: l₂) - ((a :: l₂).length - (a :: l₁).length) ≤ countP p (a :: l₁)

Proof state:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
this : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Tactic:
have := s.length_le

Result:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
this✝ : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁
this : l₁.length ≤ l₂.length
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Proof state:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
⊢ countP p (a :: l₂) - ((a :: l₂).length - (a :: l₁).length) ≤ countP p (a :: l₁)

Tactic:
simp only [countP_cons, length_cons]

Result:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
this : countP p l - (l.length - l₁.length) ≤ countP p l₁
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Tactic:
have := s.length_le

Result:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
this✝ : countP p l - (l.length - l₁.length) ≤ countP p l₁
this : l₁.length ≤ l.length
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
⊢ countP p (a :: l₂✝) - ((a :: l₂✝).length - l₁.length) ≤ countP p l₁

Tactic:
rename_i l

Result:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
⊢ countP p (a :: l) - ((a :: l).length - l₁.length) ≤ countP p l₁

Proof state:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Tactic:
have := s.le_countP p

Result:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
this : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
⊢ countP p (a :: l) - ((a :: l).length - l₁.length) ≤ countP p l₁

Tactic:
simp only [countP_cons, length_cons]

Result:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
this✝ : countP p l - (l.length - l₁.length) ≤ countP p l₁
this : l₁.length ≤ l.length
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Tactic:
split <;> omega

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
s : l₁ <+ l₂
p : α✝ → Bool
⊢ countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

Tactic:
match s with
| .slnil => simp
| .cons a s =>
  rename_i l
  simp only [countP_cons, length_cons]
  have := s.le_countP p
  have := s.length_le
  split <;> omega
| .cons₂ a s =>
  rename_i l₁ l₂
  simp only [countP_cons, length_cons]
  have := s.le_countP p
  have := s.length_le
  split <;> omega

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
s : l₁ <+ l₂
p : α✝ → Bool
⊢ countP p [] - ([].length - [].length) ≤ countP p []

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Tactic:
have := s.le_countP p

Result:
α✝ : Type u_1
l₁✝ l₂ : List α✝
s✝ : l₁✝ <+ l₂
p : α✝ → Bool
l₁ l : List α✝
a : α✝
s : l₁ <+ l
this : countP p l - (l.length - l₁.length) ≤ countP p l₁
⊢ (countP p l + if p a = true then 1 else 0) - (l.length + 1 - l₁.length) ≤ countP p l₁

Proof state:
α✝ : Type u_1
l₁✝ l₂✝ : List α✝
s✝ : l₁✝ <+ l₂✝
p : α✝ → Bool
l₁ l₂ : List α✝
a : α✝
s : l₁ <+ l₂
this✝ : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁
this : l₁.length ≤ l₂.length
⊢ (countP p l₂ + if p a = true then 1 else 0) - (l₂.length + 1 - (l₁.length + 1)) ≤
    countP p l₁ + if p a = true then 1 else 0

Tactic:
split <;> omega

Result:
no goals