Theorem: PMF.map_not_bernoulli' (LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ map Not (bernoulli' p hp) = bernoulli' (1 - p) ⋯
Tactic:
have : ∀ p : Prop, (Finset.univ.filter fun q : Prop ↦ ¬ q ↔ p) = {¬ p} := by
  rintro p
  ext q
  by_cases p <;> by_cases q <;> simp [*]
State after:
α : 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) ⋯

State before:
α : 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) ⋯
Tactic:
refine' (map_ofFintype _ _ _).trans _
State after:
α : 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) ⋯

State before:
α : 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) ⋯
Tactic:
simp only [this, bernoulli', Finset.mem_filter, Finset.mem_univ, true_and_iff,
  Finset.mem_disjiUnion, tsub_le_self, eq_iff_iff, Finset.sum_singleton, WithTop.coe_sub,
  ENNReal.coe_one]
State after:
α : 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 => if ¬b then ↑p else 1 - ↑p) ⋯ = ofFintype (fun b => if b then ↑(1 - p) else 1 - ↑(1 - p)) ⋯

State before:
α : 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 => if ¬b then ↑p else 1 - ↑p) ⋯ = ofFintype (fun b => if b then ↑(1 - p) else 1 - ↑(1 - p)) ⋯
Tactic:
congr 1 with q
State after:
case e_f.h
α : 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}
q : Prop
⊢ (if ¬q then ↑p else 1 - ↑p) = if q then ↑(1 - p) else 1 - ↑(1 - p)

State before:
case e_f.h
α : 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}
q : Prop
⊢ (if ¬q then ↑p else 1 - ↑p) = if q then ↑(1 - p) else 1 - ↑(1 - p)
Tactic:
split_ifs <;> simp [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
Tactic:
rintro p
State after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p : Prop
⊢ Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p : Prop
⊢ Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
Tactic:
ext q
State after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p q : Prop
⊢ q ∈ Finset.filter (fun q => ¬q ↔ p) Finset.univ ↔ q ∈ {¬p}

State before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p q : Prop
⊢ q ∈ Finset.filter (fun q => ¬q ↔ p) Finset.univ ↔ q ∈ {¬p}
Tactic:
by_cases p <;> by_cases q <;> simp [*]
State after:
no goals