Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
have hcs' : μ s ≠ 0 :=
  (μ.toOuterMeasure.pos_of_subset_ne_zero (Set.inter_subset_left _ _) hci).ne'
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
⊢ MeasurableSet u → ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
ext u
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
a✝ : MeasurableSet u
⊢ ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
⊢ MeasurableSet u → ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
intro
no goals
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
a✝ : MeasurableSet u
⊢ ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
simp [*, hms.inter hmt, cond_apply, ← mul_assoc, ← Set.inter_assoc, ENNReal.mul_inv, mul_comm, ←
  mul_assoc, ENNReal.mul_inv_cancel]