refine' (map_ofFintype _ _ _).trans _
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ map Not (bernoulli' p hp) = bernoulli' (1 - p) ⋯
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => (¬a) = b) Finset.univ, if a then ↑p else 1 - ↑p) ⋯ =
    bernoulli' (1 - p) ⋯