internlm/Lean-Github huggingface dataset:
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
Proof state after:
case cons.inl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
rewrite [hone, Nat.add_comm]
Proof state after:
case cons.inl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) + 1 ≤ 1
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) + 1 ≤ 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case cons.inl.a
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) ≤ 0
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inl.a
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
if hpa : p a = true then
  have : a = b := hp _ _ hpa hb.2
  cases this
  exact absurd hb.1 hl.head
else
  rewrite [if_neg hpa]; exact .refl
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
have : a = b := hp _ _ hpa hb.2
Proof state after:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
this : a = b
⊢ (if p a = true then 1 else 0) ≤ 0
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
this : a = b
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
cases this
Proof state after:
case refl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
hpa : p a = true
hb : a ∈ l ∧ p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case refl
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
hpa : p a = true
hb : a ∈ l ∧ p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
exact absurd hb.1 hl.head
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
rewrite [if_neg hpa]
Proof state after:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ 0 ≤ 0
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ 0 ≤ 0
Tactic:
exact .refl
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inr
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hlt : countP p l < 1
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
Proof state after:
case cons.inr
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hlt : countP p l < 1
this : countP p l = 0
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inr
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hlt : countP p l < 1
this : countP p l = 0
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
rewrite [this, Nat.zero_add]
Proof state after:
case cons.inr
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hlt : countP p l < 1
this : countP p l = 0
⊢ (if p a = true then 1 else 0) ≤ 1
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons.inr
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hlt : countP p l < 1
this : countP p l = 0
⊢ (if p a = true then 1 else 0) ≤ 1
Tactic:
cases p a <;> decide
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
α : Type u
β : Type v
p q : α → Bool
l : List α
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
Tactic:
induction l with
| nil => exact .refl
| cons a l IH =>
  simp only [countP_cons]
  cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
  . exact IH
  . exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case nil
α : Type u
β : Type v
p q : α → Bool
⊢ countP (fun a => p a || q a) [] ≤ countP p [] + countP q []
Tactic:
exact .refl
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) (a :: l) ≤ countP p (a :: l) + countP q (a :: l)
Tactic:
simp only [countP_cons]
Proof state after:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) ≤
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Theorem: List.countP_or_le_add
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) ≤
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Tactic:
cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
Proof state after:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l

case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Theorem: List.countP_or_le_add
Proof state before:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l

case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. exact IH
Proof state after:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Theorem: List.countP_or_le_add
Proof state before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. exact Nat.succ_le_succ IH
Proof state after:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. rewrite [Nat.succ_add]; exact Nat.succ_le_succ IH
Proof state after:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
Tactic:
exact IH
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)
Tactic:
exact Nat.succ_le_succ IH
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l
Tactic:
rewrite [Nat.succ_add]
Proof state after:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + countP q l)
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + countP q l)
Tactic:
exact Nat.succ_le_succ IH
Proof state after:
no goals
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
rewrite [Nat.succ_add]
Proof state after:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + (countP q l + 1))
Theorem: List.countP_or_le_add
Proof state before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + (countP q l + 1))
Tactic:
exact Nat.succ_le_succ <| .step IH
Proof state after:
no goals
Theorem: List.countP_disjoint
Proof state before:
α : Type u
β : Type v
p q : α → Bool
l : List α
h : ∀ (a : α), (p a && q a) = false
⊢ countP (fun a => p a || q a) l = countP p l + countP q l
Tactic:
induction l with
| nil => exact (Nat.zero_add 0).symm
| cons a l IH =>
  simp only [countP_cons]
  specialize h a; revert h
  cases p a <;> cases q a <;> simp [IH]
  . rw [Nat.add_assoc]
  . rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: List.countP_disjoint
Proof state before:
case nil
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
⊢ countP (fun a => p a || q a) [] = countP p [] + countP q []
Tactic:
exact (Nat.zero_add 0).symm
Proof state after:
no goals
Theorem: List.countP_disjoint
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP (fun a => p a || q a) (a :: l) = countP p (a :: l) + countP q (a :: l)
Tactic:
simp only [countP_cons]
Proof state after:
case cons
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Theorem: List.countP_disjoint
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Tactic:
specialize h a
Proof state after:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
h : (p a && q a) = false
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Theorem: List.countP_disjoint
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
h : (p a && q a) = false
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Tactic:
revert h
Proof state after:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ (p a && q a) = false →
    (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
      (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Theorem: List.countP_disjoint
Proof state before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ (p a && q a) = false →
    (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) =
      (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Tactic:
cases p a <;> cases q a <;> simp [IH]
Proof state after:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + 1 + countP q l
Theorem: List.countP_disjoint
Proof state before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
. rw [Nat.add_assoc]
Proof state after:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + 1 + countP q l
Theorem: List.countP_disjoint
Proof state before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
. rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: List.countP_disjoint
Proof state before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + (countP q l + 1)
Tactic:
rw [Nat.add_assoc]
Proof state after:
no goals
Theorem: List.countP_disjoint
Proof state before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l = countP p l + countP q l
⊢ countP p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: List.countP_image_le_length
Proof 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
Proof state after:
no goals
Theorem: List.countP_image_le_length
Proof 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
Proof state after:
no goals
Theorem: List.countP_image_le_length
Proof 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]
Proof 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)
Theorem: List.countP_image_le_length
Proof 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 ?_
Proof 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)
Theorem: List.countP_image_le_length
Proof 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]
Proof 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
Theorem: List.countP_image_le_length
Proof 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
Proof 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