awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : ∃ (i : ι), t1 ∈ s i
ht2 : t2 ∈ s'
obtain :
  ∀ (n : ι) (ht1 : t1 ∈ s n),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
obtain ⟨n, ht1⟩ := ht1
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
hyp n t1 t2 ht1 ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact hyp n t1 t2 ht1 ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋃ n ∈ u, s n) t1
ht2 : t2 ∈ s'
⊢ ∃ (i : ι) (_ : i ∈ u), t1 ∈ s i

Tactic:
simp_rw [Set.mem_iUnion] at ht1

Premises used: Set.mem_iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ (i : ι) (_ : i ∈ u), t1 ∈ s i
rcases :
  ∀ (n : ι) (hpn : n ∈ u) (ht1 : t1 ∈ s n),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rcases ht1 with ⟨n, hpn, ht1⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
hyp n hpn t1 t2 ht1 ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact hyp n hpn t1 t2 ht1 ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s' s₂ : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
⊢ IndepSets (s₁ ∩ s₂) s' κ μ

Tactic:
fun t1 t2 ht1 ht2 => h₁ t1 t2 ((Set.mem_inter_iff _ _ _).mp ht1).left ht2

Premises used: Set.mem_inter_iff, ProbabilityTheory.Kernel.IndepSets, And.left, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ (n : ι), s n) t1
ht2 : t2 ∈ s'
obtain :
  ∀ (n : ι) (h : IndepSets (s n) s' κ μ),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ (n : ι), s n) t1
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
h t1 t2 (Set.mem_iInter.mp ht1 n) ht2

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ (n : ι), s n) t1
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact h t1 t2 (Set.mem_iInter.mp ht1 n) ht2

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ n ∈ u, s n) t1
ht2 : t2 ∈ s'
rcases :
  ∀ (n : ι) (hn : n ∈ u) (h : IndepSets (s n) s' κ μ),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rcases h with ⟨n, hn, h⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ n ∈ u, s n) t1
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋂ n ∈ u, s n) t1
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
f : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
simp_rw : iIndep (fun (i : ι) ↦ generateFrom {f i}) κ μ ↔ iIndepSet f κ μ
⊢ iIndep (fun (i : ι) ↦ MeasurableSpace.comap (β := Prop) (fun (x : Ω) ↦ x ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ

Tactic:
simp_rw [← generateFrom_singleton, iIndepSet]

Premises used: ProbabilityTheory.Kernel.iIndepSet, MeasurableSpace.generateFrom_singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ iIndepSets (fun (i : ι) ↦ {s i}) κ μ ↔
    ∀ (S : Finset ι),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
          (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩

Premises used: Iff.intro, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
refine :
  ∀
    (h :
      ∀ (S : Finset ι),
        ∀ᵐ (a : α) ∂μ,
          Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
            (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
    (S : Finset ι) (f : ι → Set Ω)
    (hf : ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (i : ι) ↦ ({s i} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ iIndepSets (fun (i : ι) ↦ {s i}) κ μ ↔
    ∀ (S : Finset ι),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
          (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine ⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h :
  ∀ (S : Finset ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (i : ι) ↦ ({s i} : Set (Set Ω))) i) (f i)
h₁ :
  ∀ (a : α)
    (ha :
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
filter_upwards [h S] with a ha
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h :
  ∀ (S : Finset ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (i : ι) ↦ ({s i} : Set (Set Ω))) i) (f i)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi : i ∈ S
rw rw₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [hf i hi]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h :
  ∀ (S : Finset ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (i : ι) ↦ ({s i} : Set (Set Ω))) i) (f i)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ ∀ i ∈ S,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
have : ∀ i ∈ S, κ a (f i) = κ a (s i) := fun i hi ↦ by rw [hf i hi]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h :
  ∀ (S : Finset ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (i : ι) ↦ ({s i} : Set (Set Ω))) i) (f i)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
this :
  ∀ i ∈ S,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
    (∏ x ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s x) : ℝ≥0∞)
h₂ h₃ h₄ h₅ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
    (∏ x ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rwa [Finset.prod_congr rfl this, Set.iInter₂_congr hf]

Premises used: Finset.prod_congr, Set.iInter₂_congr, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
s1 t1 : Set Ω
hs1 : Membership.mem (γ := Set (Set Ω)) {s} s1
ht1 : Membership.mem (γ := Set (Set Ω)) {t} t1
rwa :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s1 ∩ t1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)

Tactic:
rwa [Set.mem_singleton_iff.mp hs1, Set.mem_singleton_iff.mp ht1]

Premises used: Set.mem_singleton_iff, Iff.mp
-- 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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx : Membership.mem (γ := Finset ι) {i, j} x
inl : ∀ (hx : x = i), (if x = i then t₁ else t₂) ∈ s x
inr : ∀ (hx : Membership.mem (γ := Finset ι) {j} x), (if x = i then t₁ else t₂) ∈ s x
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
rcases Finset.mem_insert.mp hx with hx | hx

Premises used: Finset.mem_insert, Iff.mp
-- 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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx_1 : Membership.mem (γ := Finset ι) {i, j} x
hx : x = i
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
simp [hx, ht₁]
-- 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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx_1 : Membership.mem (γ := Finset ι) {i, j} x
hx : Membership.mem (γ := Finset ι) {j} x
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
simp [Finset.mem_singleton.mp hx, hij.symm, ht₂]

Premises used: Finset.mem_singleton, Ne.symm, Iff.mp
-- 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
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → (if x = i then t₁ else t₂) ∈ s x

Tactic:
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₂]
-- 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
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
⊢ (⋂ (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₂

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

Premises used: Finset.set_biInter_insert, Finset.set_biInter_singleton
-- 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
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
⊢ (⋂ (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₂

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]