Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∈ p1
h2 : n ∈ p2
⊢ (κ a) (f1 n ∩ f2 n) = (κ a) (f1 n) * (κ a) (f2 n)

pp: case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∈ p1
h2 : n ∉ p2
⊢ (κ a) (f1 n ∩ univ) = (κ a) (f1 n) * 1

pp: case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∉ p1
h✝ : n ∈ p2
⊢ (κ a) (univ ∩ f2 n) = 1 * (κ a) (f2 n)

pp: case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∉ p1
h✝ : n ∉ p2
⊢ (κ a) (univ ∩ univ) = 1 * 1

Tactic:
· exact absurd rfl (Set.disjoint_iff_forall_ne.mp hST (hp1 h1) (hp2 h2))

Goal state after:
case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∈ p1
h2 : n ∉ p2
⊢ (κ a) (f1 n ∩ univ) = (κ a) (f1 n) * 1

case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∉ p1
h✝ : n ∈ p2
⊢ (κ a) (univ ∩ f2 n) = 1 * (κ a) (f2 n)

case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
h1 : n ∉ p1
h✝ : n ∉ p2
⊢ (κ a) (univ ∩ univ) = 1 * 1