Theorem: ProbabilityTheory.IsBernoulliSeq.meas_apply (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 μ
a : α
⊢ μ {ω | a ∈ X ω} = ↑p
Tactic:
rw [(_ : {ω | a ∈ X ω} = (fun ω ↦ a ∈ X ω) ⁻¹' {True}),
  ← Measure.map_apply_of_aemeasurable (hX.aemeasurable a) MeasurableSpace.measurableSet_top]
State after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ (Measure.map (fun ω => a ∈ X ω) μ) {True} = ↑p

α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ {ω | a ∈ X ω} = (fun ω => a ∈ X ω) ⁻¹' {True}

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 μ
a : α
⊢ (Measure.map (fun ω => a ∈ X ω) μ) {True} = ↑p
Tactic:
simp [hX.map]
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 μ
a : α
⊢ {ω | a ∈ X ω} = (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
ext ω
State after:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
ω : Ω
⊢ ω ∈ {ω | a ∈ X ω} ↔ ω ∈ (fun ω => a ∈ X ω) ⁻¹' {True}

State before:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
ω : Ω
⊢ ω ∈ {ω | a ∈ X ω} ↔ ω ∈ (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
simp
State after:
no goals