Theorem: List.countP_image_le_length (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq β
la : List α
lb : List β
hnodup : Nodup lb
f : α → β
⊢ countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
Tactic:
induction la with
| nil => simp
| cons a la IH =>
  simp only [mem_cons, exists_eq_or_imp, decide_or]
  refine trans (s:=LE.le) countP_or_le_add ?_
  rewrite [length_cons, Nat.succ_eq_one_add]
  refine Nat.add_le_add ?_ IH
  refine countP_le_one_of_unique_nodup ?_ hnodup
  intro b₁ b₂ hb₁ hb₂
  cases of_decide_eq_true hb₁
  cases of_decide_eq_true hb₂
  rfl
State after:
no goals

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
⊢ countP (fun b => decide (∃ a, a ∈ [] ∧ f a = b)) lb ≤ length []
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (∃ a_1, a_1 ∈ a :: la ∧ f a_1 = b)) lb ≤ length (a :: la)
Tactic:
simp only [mem_cons, exists_eq_or_imp, decide_or]
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b) || decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length (a :: la)

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b) || decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length (a :: la)
Tactic:
refine trans (s:=LE.le) countP_or_le_add ?_
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb + countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length (a :: la)

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb + countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length (a :: la)
Tactic:
rewrite [length_cons, Nat.succ_eq_one_add]
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb + countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ 1 + length la

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb + countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ 1 + length la
Tactic:
refine Nat.add_le_add ?_ IH
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb ≤ 1

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb ≤ 1
Tactic:
refine countP_le_one_of_unique_nodup ?_ hnodup
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ ∀ (a_1 b : β), decide (f a = a_1) = true → decide (f a = b) = true → a_1 = b

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ ∀ (a_1 b : β), decide (f a = a_1) = true → decide (f a = b) = true → a_1 = b
Tactic:
intro b₁ b₂ hb₁ hb₂
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₁ b₂ : β
hb₁ : decide (f a = b₁) = true
hb₂ : decide (f a = b₂) = true
⊢ b₁ = b₂

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₁ b₂ : β
hb₁ : decide (f a = b₁) = true
hb₂ : decide (f a = b₂) = true
⊢ b₁ = b₂
Tactic:
cases of_decide_eq_true hb₁
State after:
case cons.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₂ : β
hb₂ : decide (f a = b₂) = true
hb₁ : decide (f a = f a) = true
⊢ f a = b₂

State before:
case cons.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₂ : β
hb₂ : decide (f a = b₂) = true
hb₁ : decide (f a = f a) = true
⊢ f a = b₂
Tactic:
cases of_decide_eq_true hb₂
State after:
case cons.refl.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
hb₁ hb₂ : decide (f a = f a) = true
⊢ f a = f a

State before:
case cons.refl.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
hb₁ hb₂ : decide (f a = f a) = true
⊢ f a = f a
Tactic:
rfl
State after:
no goals