Theorem: List.isInfix_countp_le (One.lean)

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
have ⟨s,t,heq⟩ := h
State after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ countp p l₁ ≤ countp p l₂

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
apply_fun countp p at heq
State after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p (s ++ l₁ ++ t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p (s ++ l₁ ++ t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
simp only [append_assoc, countp_append] at heq
State after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
rw [← heq]
State after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p s + (countp p l₁ + countp p t)

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p s + (countp p l₁ + countp p t)
Tactic:
linarith
State after:
no goals