α : 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
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ↑(countp p) (of x) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0
erw [FreeAddMonoid.countp_of]
α : 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
α : 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
simp only [eq_iff_iff, iff_true, ofAdd_zero]
no goals
α : 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
rfl