α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b✝ b : Bool
⊢ b ∈ support (bernoulli p h) ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ support (bernoulli p h) = {b | bif b then p ≠ 0 else p ≠ 1}
refine' Set.ext fun b => _
case false
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ false ∈ support (bernoulli p h) ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

case true
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ true ∈ support (bernoulli p h) ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b✝ b : Bool
⊢ b ∈ support (bernoulli p h) ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}
induction b
case false
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
case false
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ false ∈ support (bernoulli p h) ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}
simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne.def, tsub_eq_zero_iff_le, not_le]
no goals
case false
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
exact ⟨ne_of_lt, lt_of_le_of_ne h⟩
no goals
case true
α : Type ?u.168514
β : Type ?u.168517
γ : Type ?u.168520
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ true ∈ support (bernoulli p h) ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq]