Theorem: ProbabilityTheory.IsBernoulliSeq.union (LeanCamCombi/BernoulliSeq.lean)

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IsBernoulliSeq (fun ω => X ω ∪ Y ω) (p + q - p * q) μ
Tactic:
convert (hX.compl.inter hY.compl _).compl using 1
State after:
case h.e'_4
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ (fun ω => X ω ∪ Y ω) = fun ω => ((X ω)ᶜ ∩ (Y ω)ᶜ)ᶜ

case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + q - p * q = 1 - (1 - p) * (1 - q)

α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IndepFun (fun ω => (X ω)ᶜ) (fun ω => (Y ω)ᶜ) μ

State before:
case h.e'_4
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ (fun ω => X ω ∪ Y ω) = fun ω => ((X ω)ᶜ ∩ (Y ω)ᶜ)ᶜ
Tactic:
simp [compl_inter]
State after:
no goals

State before:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + q - p * q = 1 - (1 - p) * (1 - q)
Tactic:
rw [mul_tsub, mul_one, tsub_tsub, tsub_tsub_cancel_of_le, tsub_mul, one_mul,
  add_tsub_assoc_of_le (mul_le_of_le_one_left' $ hX.le_one)]
State after:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + (1 - p) * q ≤ 1

State before:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + (1 - p) * q ≤ 1
Tactic:
exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq
  (add_tsub_cancel_of_le hX.le_one)
State after:
no goals

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IndepFun (fun ω => (X ω)ᶜ) (fun ω => (Y ω)ᶜ) μ
Tactic:
rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl,
  MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff]
State after:
no goals