Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ Function.Injective i

pp: case hfi
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ Function.Injective i

pp: case hf
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s ∩ t)

pp: case hfi
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ Function.Injective i

pp: case hf
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)

pp: case hms
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet s

pp: case hfi
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ Function.Injective i

pp: case hf
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet t

pp: case hms
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
all_goals first
  | exact hi.injective
  | exact hi.measurableSet_image'
  | exact hs
  | exact ht
  | exact hi.measurable hs
  | exact (hi.measurable hs).inter ht

Goal state after: