Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
⊢ Indep m1 m2
intro t1 t2 ht1 ht2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
let μ_inter := μ.restrict t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
let ν := μ t2 • μ
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
have h_univ : μ_inter Set.univ = ν Set.univ := by
  rw [Measure.restrict_apply_univ, Measure.smul_apply, smul_eq_mul, measure_univ, mul_one]
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
haveI : IsFiniteMeasure μ_inter := @Restrict.isFiniteMeasure Ω _ t2 μ ⟨measure_lt_top μ t2⟩
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑(Measure.restrict μ t2) t1 = ↑↑μ t2 * ↑↑μ t1
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
rw [mul_comm, ← Measure.restrict_apply (h1 t1 ht1)]
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ ↑↑μ_inter t = ↑↑ν t
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑(Measure.restrict μ t2) t1 = ↑↑μ t2 * ↑↑μ t1
refine' ext_on_measurableSpace_of_generate_finite m p1 (fun t ht => _) h1 hpm1 hp1 h_univ ht1
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1✝ : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
ht1 : MeasurableSet t
⊢ ↑↑μ_inter t = ↑↑ν t
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ ↑↑μ_inter t = ↑↑ν t
have ht1 : MeasurableSet[m] t := by
  refine' h1 _ _
  rw [hpm1]
  exact measurableSet_generateFrom ht
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1✝ : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
ht1 : MeasurableSet t
⊢ ↑↑μ (t ∩ t2) = ↑↑μ t * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1✝ : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
ht1 : MeasurableSet t
⊢ ↑↑μ_inter t = ↑↑ν t
rw [Measure.restrict_apply ht1, Measure.smul_apply, smul_eq_mul, mul_comm]
no goals
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1✝ : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
ht1 : MeasurableSet t
⊢ ↑↑μ (t ∩ t2) = ↑↑μ t * ↑↑μ t2
exact IndepSets.indep_aux h2 hp2 hpm2 hyp ht ht2
no goals
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
⊢ ↑↑μ_inter Set.univ = ↑↑ν Set.univ
rw [Measure.restrict_apply_univ, Measure.smul_apply, smul_eq_mul, measure_univ, mul_one]
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t
refine' h1 _ _
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t
rw [hpm1]
no goals
Ω : Type u_1
ι : Type ?u.1736711
m1 m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t2
ν : MeasureTheory.Measure Ω := ↑↑μ t2 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t
exact measurableSet_generateFrom ht