[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x = (true = true) then 1 else 0
[PROOFSTEP]
simp [countp, List.countp, List.countp.go]
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.single x 1 y
[PROOFSTEP]
simp [Pi.single, Function.update, count, countp, List.countp, List.countp.go, Bool.beq_eq_decide_eq]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0
[PROOFSTEP]
erw [FreeAddMonoid.countp_of]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if p x = (true = true) then 1 else 0) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0
[PROOFSTEP]
simp only [eq_iff_iff, iff_true, ofAdd_zero]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if p x then 1 else 0) = if p x then ↑Multiplicative.ofAdd 1 else 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x then ↑Multiplicative.ofAdd 1 else 1
[PROOFSTEP]
rw [countp_of', ofAdd_zero]
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.mulSingle x (↑Multiplicative.ofAdd 1) y
[PROOFSTEP]
simp [count, countp_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]
