case refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ s' ∈ {s | MeasurableSet s}

case refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet s t
refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
case refine_1.refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), t ∈ {s} → (fun u => MeasurableSet u) t

case refine_1.refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ (fun u => MeasurableSet u) ∅

case refine_1.refine_3
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), (fun u => MeasurableSet u) t → (fun u => MeasurableSet u) (tᶜ)

case refine_1.refine_4
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (f : ℕ → Set Ω), (∀ (n : ℕ), (fun u => MeasurableSet u) (f n)) → (fun u => MeasurableSet u) (⋃ (i : ℕ), f i)
case refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ s' ∈ {s | MeasurableSet s}
refine @generateFrom_induction _ (fun u => MeasurableSet[m₁] u) {s} ?_ ?_ ?_ ?_ _ hs'
no goals
case refine_1.refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), t ∈ {s} → (fun u => MeasurableSet u) t
simp only [Set.mem_singleton_iff, forall_eq, hs]
no goals
case refine_1.refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ (fun u => MeasurableSet u) ∅
exact @MeasurableSet.empty _ m₁
no goals
case refine_1.refine_3
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), (fun u => MeasurableSet u) t → (fun u => MeasurableSet u) (tᶜ)
exact fun u hu => hu.compl
no goals
case refine_1.refine_4
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (f : ℕ → Set Ω), (∀ (n : ℕ), (fun u => MeasurableSet u) (f n)) → (fun u => MeasurableSet u) (⋃ (i : ℕ), f i)
exact fun f hf => MeasurableSet.iUnion hf
case refine_2.refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t_1 : Set Ω), t_1 ∈ {t} → (fun u => MeasurableSet u) t_1

case refine_2.refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ (fun u => MeasurableSet u) ∅

case refine_2.refine_3
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), (fun u => MeasurableSet u) t → (fun u => MeasurableSet u) (tᶜ)

case refine_2.refine_4
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (f : ℕ → Set Ω), (∀ (n : ℕ), (fun u => MeasurableSet u) (f n)) → (fun u => MeasurableSet u) (⋃ (i : ℕ), f i)
case refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}
refine @generateFrom_induction _ (fun u => MeasurableSet[m₂] u) {t} ?_ ?_ ?_ ?_ _ ht'
no goals
case refine_2.refine_1
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t_1 : Set Ω), t_1 ∈ {t} → (fun u => MeasurableSet u) t_1
simp only [Set.mem_singleton_iff, forall_eq, ht]
no goals
case refine_2.refine_2
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ (fun u => MeasurableSet u) ∅
exact @MeasurableSet.empty _ m₂
no goals
case refine_2.refine_3
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (t : Set Ω), (fun u => MeasurableSet u) t → (fun u => MeasurableSet u) (tᶜ)
exact fun u hu => hu.compl
no goals
case refine_2.refine_4
Ω : Type u_1
ι : Type ?u.2871903
s✝ t✝ : Set Ω
S T : Set (Set Ω)
m₁ m₂ m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : Indep m₁ m₂
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∀ (f : ℕ → Set Ω), (∀ (n : ℕ), (fun u => MeasurableSet u) (f n)) → (fun u => MeasurableSet u) (⋃ (i : ℕ), f i)
exact fun f hf => MeasurableSet.iUnion hf