-- Mathlib/Probability/Independence/Kernel.lean
theorem Indep.indepSet_of_measurableSet {m₁ m₂ _ : MeasurableSpace Ω} {κ : Kernel α Ω}
    {μ : Measure α}
    (h_indep : Indep m₁ m₂ κ μ) {s t : Set Ω} (hs : MeasurableSet[m₁] s)
    (ht : MeasurableSet[m₂] t) :
    IndepSet s t κ μ

Proof state:
case refine_1.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), f n ∈ {s | MeasurableSet s}
⊢ ⋃ i, f i ∈ {s | MeasurableSet s}

Tactic:
exact .iUnion hf

Result:
no goals

Proof state:
case refine_1
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}

Tactic:
induction s', hs' using generateFrom_induction with
| hC t ht => exact ht ▸ hs
| empty => exact @MeasurableSet.empty _ m₁
| compl u _ hu => exact hu.compl
| iUnion f _ hf => exact .iUnion hf

Result:
no goals

Proof state:
case refine_2.compl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}
u : Set Ω
ht✝ : MeasurableSet u
hu : u ∈ {s | MeasurableSet s}
⊢ uᶜ ∈ {s | MeasurableSet s}

Tactic:
exact hu.compl

Result:
no goals

Proof state:
case refine_2.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}
f : ℕ → Set Ω
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), f n ∈ {s | MeasurableSet s}
⊢ ⋃ i, f i ∈ {s | MeasurableSet s}

Tactic:
exact .iUnion hf

Result:
no goals

Proof state:
case refine_1.empty
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
⊢ ∅ ∈ {s | MeasurableSet s}

Tactic:
exact @MeasurableSet.empty _ m₁

Result:
no goals

Proof state:
case refine_1.hC
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t✝ : Set Ω
hs : MeasurableSet s
ht✝¹ : MeasurableSet t✝
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
t : Set Ω
ht : t ∈ {s}
ht✝ : MeasurableSet t
⊢ t ∈ {s | MeasurableSet s}

Tactic:
exact ht ▸ hs

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet s t κ μ

Tactic:
refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_

Result:
case refine_1
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}

Proof state:
case refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}

Tactic:
induction t', ht' using generateFrom_induction with
| hC s hs => exact hs ▸ ht
| empty => exact @MeasurableSet.empty _ m₂
| compl u _ hu => exact hu.compl
| iUnion f _ hf => exact .iUnion hf

Result:
no goals

Proof state:
case refine_1.compl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
u : Set Ω
ht✝ : MeasurableSet u
hu : u ∈ {s | MeasurableSet s}
⊢ uᶜ ∈ {s | MeasurableSet s}

Tactic:
exact hu.compl

Result:
no goals

Proof state:
case refine_2.empty
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : 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}
⊢ ∅ ∈ {s | MeasurableSet s}

Tactic:
exact @MeasurableSet.empty _ m₂

Result:
no goals

Proof state:
case refine_2.hC
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s✝ t : Set Ω
hs✝ : MeasurableSet s✝
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s | MeasurableSet s}
s : Set Ω
hs : s ∈ {t}
ht✝ : MeasurableSet s
⊢ s ∈ {s | MeasurableSet s}

Tactic:
exact hs ▸ ht

Result:
no goals