-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSets.indepSets {s : ι → Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} (h_indep : iIndepSets s κ μ) {i j : ι} (hij : i ≠ j) :
    IndepSets (s i) (s j) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Tactic:
have h1 : t₁ = ite (i = i) t₁ t₂ := by simp only [if_true, eq_self_iff_true]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
⊢ ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x

Tactic:
intro x hx

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx : x ∈ {i, j}
⊢ (if x = i then t₁ else t₂) ∈ s x

Proof state:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx✝ : x ∈ {i, j}
hx : x = i
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
simp [hx, ht₁]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Tactic:
filter_upwards [h_indep {i, j} hf_m] with a h_indep'

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
a : α
h_indep' : (κ a) (⋂ i_1 ∈ {i, j}, if i_1 = i then t₁ else t₂) = ∏ i_1 ∈ {i, j}, (κ a) (if i_1 = i then t₁ else t₂)
⊢ (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
⊢ (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂

Tactic:
simp only [Finset.set_biInter_singleton, Finset.set_biInter_insert]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Tactic:
have h_inter : ⋂ (t : ι) (_ : t ∈ ({i, j} : Finset ι)), ite (t = i) t₁ t₂ =
    ite (i = i) t₁ t₂ ∩ ite (j = i) t₁ t₂ := by
  simp only [Finset.set_biInter_singleton, Finset.set_biInter_insert]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
a : α
h_indep' : (κ a) (⋂ i_1 ∈ {i, j}, if i_1 = i then t₁ else t₂) = ∏ i_1 ∈ {i, j}, (κ a) (if i_1 = i then t₁ else t₂)
h_prod :
  ∏ t ∈ {i, j}, (κ a) (if t = i then t₁ else t₂) = (κ a) (if i = i then t₁ else t₂) * (κ a) (if j = i then t₁ else t₂)
⊢ (κ a) ((if i = i then t₁ else t₂) ∩ t₂) = (κ a) (if i = i then t₁ else t₂) * (κ a) t₂

Tactic:
nth_rw 2 [h2]

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
a : α
h_indep' : (κ a) (⋂ i_1 ∈ {i, j}, if i_1 = i then t₁ else t₂) = ∏ i_1 ∈ {i, j}, (κ a) (if i_1 = i then t₁ else t₂)
h_prod :
  ∏ t ∈ {i, j}, (κ a) (if t = i then t₁ else t₂) = (κ a) (if i = i then t₁ else t₂) * (κ a) (if j = i then t₁ else t₂)
⊢ (κ a) ((if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂) = (κ a) (if i = i then t₁ else t₂) * (κ a) t₂

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
⊢ t₂ = if j = i then t₁ else t₂

Tactic:
simp only [hij.symm, if_false]

Result:
no goals