-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.indep {m1 m2 m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    [IsZeroOrMarkovKernel κ] {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 κ μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : MeasurableSet t
iht : ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
a : α
ha : (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
⊢ tᶜ ∩ t2 = t2 \ (t ∩ t2)

Tactic:
rw [Set.inter_comm t, Set.diff_self_inter, Set.diff_eq_compl_inter]

Result:
no goals

Proof state:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Tactic:
rw [← ae_all_iff] at h

Result:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Tactic:
rw [Set.inter_comm, Set.inter_iUnion, measure_iUnion]

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∑' (i : ℕ), (κ a) (t2 ∩ f i) = (κ a) (⋃ i, f i) * (κ a) t2

case h.hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ Pairwise (Function.onFun Disjoint fun i => t2 ∩ f i)

case h.h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ (i : ℕ), MeasurableSet (t2 ∩ f i)

Proof state:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
μ : Measure α
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
inst✝ : IsZeroOrMarkovKernel 0
hyp : IndepSets p1 p2 0 μ
⊢ Indep m1 m2 0 μ

Tactic:
simp

Result:
no goals

Proof state:
case h.hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Function.onFun Disjoint (fun i => t2 ∩ f i) i j

Tactic:
rw [Function.onFun, Set.inter_comm t2, Set.inter_comm t2]

Result:
case h.hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
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 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Disjoint (f i ∩ t2) (f j ∩ t2)