α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ countp (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) l = countp (fun x => x == a) l
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ count a (filter p l) = count a l
rw [count, countp_filter]
case e_p
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) = fun x => x == a
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ countp (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) l = countp (fun x => x == a) l
congr
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide ((b == a) = true ∧ p b = true) = (b == a)
case e_p
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) = fun x => x == a
funext b
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide ((b == a) = true ∧ p b = true) = (b == a)
rw [Bool.beq_eq_decide_eq]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)

case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : ¬b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
by_cases hb : b = a
no goals
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
simp [hb, h]
no goals
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : ¬b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
simp [hb]