-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.indep_aux {m₂ m : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)} (h2 : m₂ ≤ m)
    (hp2 : IsPiSystem p2) (hpm2 : m₂ = generateFrom p2) (hyp : IndepSets p1 p2 κ μ) {t1 t2 : Set Ω}
    (ht1 : t1 ∈ p1) (ht1m : MeasurableSet[m] t1) (ht2m : MeasurableSet[m₂] t2) :
    ∀ᵐ a ∂μ, κ a (t1 ∩ t2) = κ a t1 * κ a t2

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Tactic:
rw [inter_iUnion, measure_iUnion, measure_iUnion hfd fun i ↦ h2 _ (hfm i)]

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∑' (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * ∑' (i : ℕ), (κ a) (f i)

case h.hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ Pairwise (Function.onFun Disjoint fun i => t1 ∩ f i)

case h.h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ (i : ℕ), MeasurableSet (t1 ∩ f i)

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ 0 < (κ a) u → (κ a) u < 1 → (κ a) t1 ≠ ⊤

Tactic:
exact fun _ _ ↦ measure_ne_top _ _

Result:
no goals

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ (κ a) (t1 ∩ uᶜ) = (κ a) t1 * (κ a) uᶜ

Tactic:
rw [← Set.diff_eq, ← Set.diff_self_inter,
  measure_diff inter_subset_left (ht1m.inter (h2 _ hu)).nullMeasurableSet (measure_ne_top _ _),
  ha, measure_compl (h2 _ hu) (measure_ne_top _ _), measure_univ, ENNReal.mul_sub, mul_one]

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ 0 < (κ a) u → (κ a) u < 1 → (κ a) t1 ≠ ⊤

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∑' (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * ∑' (i : ℕ), (κ a) (f i)

Tactic:
simp only [ENNReal.tsum_mul_left, ha]

Result:
no goals

Proof state:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
μ : Measure α
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
ht2m : MeasurableSet t2
inst✝ : IsZeroOrMarkovKernel 0
hyp : IndepSets p1 p2 0 μ
⊢ ∀ᵐ (a : α) ∂μ, (0 a) (t1 ∩ t2) = (0 a) t1 * (0 a) t2

Tactic:
simp

Result:
no goals

Proof state:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Tactic:
filter_upwards [ihf] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Proof state:
case h.h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ (i : ℕ), MeasurableSet (t1 ∩ f i)

Tactic:
exact fun i ↦ .inter ht1m (h2 _ <| hfm i)

Result:
no goals