-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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
intro intro₁ intro₂ intro₃ :
  ∀ (t₁ t₂ : Set Ω) (ht₁ : t₁ ∈ s i) (ht₂ : t₂ ∈ s j),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t₁ ∩ t₂) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₁ : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₂ : ℝ≥0∞)
intro₄ :
  ∀ (t₁ t₂ : Set Ω) (ht₁ : t₁ ∈ s i) (ht₂ : t₂ ∈ s j)
    (hf_m : ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → (if x = i then t₁ else t₂) ∈ s x),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t₁ ∩ t₂) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₁ : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₂ : ℝ≥0∞)
intro₅ :
  ∀ (t₁ t₂ : Set Ω) (ht₁ : t₁ ∈ s i) (ht₂ : t₂ ∈ s j)
    (hf_m : ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → (if x = i then t₁ else t₂) ∈ s x)
    (h_inter :
      (⋂ (t : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i, j} t), if t = i then t₁ else t₂) =
        (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t₁ ∩ t₂) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₁ : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₂ : ℝ≥0∞)
h :
  ∀ (t₁ t₂ : Set Ω) (ht₁ : t₁ ∈ s i) (ht₂ : t₂ ∈ s j)
    (hf_m : ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → (if x = i then t₁ else t₂) ∈ s x)
    (h_inter :
      (⋂ (t : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i, j} t), if t = i then t₁ else t₂) =
        (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂)
    (a : α)
    (h_indep' :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i_1 : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i, j} i_1), if i_1 = i then t₁ else t₂) :
          ℝ≥0∞)
        (∏ i_1 ∈ {i, j}, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (if i_1 = i then t₁ else t₂) :
          ℝ≥0∞)),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t₁ ∩ t₂) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₁ : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t₂ : ℝ≥0∞)
⊢ IndepSets (s i) (s j) κ μ

Tactic:
classical
  intro t₁ t₂ ht₁ ht₂
  have hf_m : ∀ x : ι, x ∈ ({i, j} : Finset ι) → ite (x = i) t₁ t₂ ∈ s x := by
    intro x hx
    rcases Finset.mem_insert.mp hx with hx | hx
    · simp [hx, ht₁]
    · simp [Finset.mem_singleton.mp hx, hij.symm, ht₂]
  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]
  filter_upwards [h_indep {i, j} hf_m] with a h_indep'
  grind