awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : ι → MeasurableSpace Ω
s : ι → Set (Set Ω)
hms : ∀ (n : ι), m n = generateFrom (s n)
h_indep : iCondIndep m' hm' m μ
⊢ ProbabilityTheory.iCondIndepSets m' hm' s μ

Tactic:
Kernel.iIndep.iIndepSets hms h_indep

Premises used: ProbabilityTheory.iCondIndepSets, ProbabilityTheory.Kernel.iIndep.iIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s1 s2 : Set (Set Ω)
h_indep : CondIndep m' (generateFrom s1) (generateFrom s2) hm' μ
⊢ CondIndepSets m' hm' s1 s2 μ

Tactic:
Kernel.Indep.indepSets h_indep

Premises used: ProbabilityTheory.Kernel.Indep.indepSets, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
p1 p2 : Set (Set Ω)
h1 : m₁ ≤ mΩ
h2 : m₂ ≤ mΩ
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m₁ = generateFrom p1
hpm2 : m₂ = generateFrom p2
hyp : CondIndepSets m' hm' p1 p2 μ
⊢ CondIndep m' m₁ m₂ hm' μ

Tactic:
Kernel.IndepSets.indep h1 h2 hp1 hp2 hpm1 hpm2 hyp

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.IndepSets.indep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
p1 p2 : Set (Set Ω)
hp1m : ∀ s ∈ p1, MeasurableSet s
hp2m : ∀ s ∈ p2, MeasurableSet s
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hyp : CondIndepSets m' hm' p1 p2 μ
⊢ CondIndep m' (generateFrom p1) (generateFrom p2) hm' μ

Tactic:
Kernel.IndepSets.indep' hp1m hp2m hp1 hp2 hyp

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.IndepSets.indep'
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iCondIndepSets m' hm' s μ
hST : Disjoint S T
⊢ CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T) μ

Tactic:
Kernel.indepSets_piiUnionInter_of_disjoint h_indep hST

Premises used: ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iCondIndepSet m' hm' s μ
S T : Set ι
hST : Disjoint S T
⊢ CondIndep m' (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) hm' μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_of_disjoint hsm hs S T hST

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ mΩ
h_indep : iCondIndep m' hm' m μ
S T : Set ι
hST : Disjoint S T
⊢ CondIndep m' (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) hm' μ

Tactic:
Kernel.indep_iSup_of_disjoint h_le h_indep hST

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_iSup_of_disjoint
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' m₁ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : ι → MeasurableSpace Ω
h_indep : ∀ (i : ι), CondIndep m' (m i) m₁ hm' μ
h_le : ∀ (i : ι), m i ≤ mΩ
h_le' : m₁ ≤ mΩ
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
⊢ CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ

Tactic:
Kernel.indep_iSup_of_directed_le h_indep h_le h_le' hm

Premises used: ProbabilityTheory.Kernel.indep_iSup_of_directed_le, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iCondIndepSet m' hm' s μ
i : ι
⊢ CondIndep m' (generateFrom {s i}) (generateFrom {t : Set Ω | ∃ j < i, s j = t}) hm' μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_lt hsm hs i

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iCondIndepSet m' hm' s μ
i k : ι
hk : i < k
⊢ CondIndep m' (generateFrom {s k}) (generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) hm' μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_le hsm hs i hk

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iCondIndepSet m' hm' s μ
n : ℕ
⊢ CondIndep m' (generateFrom {s (n + 1)}) (generateFrom {t : Set Ω | ∃ k ≤ n, s k = t}) hm' μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_le_nat hsm hs n

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' m₁ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : SemilatticeSup ι
m : ι → MeasurableSpace Ω
h_indep : ∀ (i : ι), CondIndep m' (m i) m₁ hm' μ
h_le : ∀ (i : ι), m i ≤ mΩ
h_le' : m₁ ≤ mΩ
hm : Monotone m
⊢ CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ

Tactic:
Kernel.indep_iSup_of_monotone h_indep h_le h_le' hm

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_iSup_of_monotone
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' m₁ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : SemilatticeInf ι
m : ι → MeasurableSpace Ω
h_indep : ∀ (i : ι), CondIndep m' (m i) m₁ hm' μ
h_le : ∀ (i : ι), m i ≤ mΩ
h_le' : m₁ ≤ mΩ
hm : Antitone m
⊢ CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ

Tactic:
Kernel.indep_iSup_of_antitone h_indep h_le h_le' hm

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_iSup_of_antitone
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iCondIndepSets m' hm' π μ
haS : a ∉ S
⊢ CondIndepSets m' hm' (piiUnionInter π (↑S : Set ι)) (π a) μ

Tactic:
Kernel.iIndepSets.piiUnionInter_of_notMem hp_ind haS

Premises used: ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iCondIndepSets m' hm' π μ
⊢ ProbabilityTheory.iCondIndep m' hm' m μ

Tactic:
Kernel.iIndepSets.iIndep m h_le π h_pi h_generate h_ind

Premises used: ProbabilityTheory.Kernel.iIndepSets.iIndep, ProbabilityTheory.iCondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
S T : Set (Set Ω)
hs : s ∈ S
ht : t ∈ T
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_indep : CondIndepSets m' hm' S T μ
⊢ CondIndepSet m' hm' s t μ

Tactic:
Kernel.IndepSets.indepSet_of_mem _ _ hs ht hs_meas ht_meas _ _ h_indep

Premises used: ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem, ProbabilityTheory.CondIndepSet
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_indep : CondIndep m' m₁ m₂ hm' μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ CondIndepSet m' hm' s t μ

Tactic:
Kernel.Indep.indepSet_of_measurableSet h_indep hs ht

Premises used: ProbabilityTheory.CondIndepSet, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' s t μ

Tactic:
Kernel.indep_iff_forall_indepSet m₁ m₂ _ _

Premises used: ProbabilityTheory.Kernel.indep_iff_forall_indepSet, ProbabilityTheory.CondIndep, ProbabilityTheory.CondIndepSet
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
rw :
  (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)

Tactic:
rw [condIndepFun_iff _ _ _ _ hf hg]

Premises used: ProbabilityTheory.condIndepFun_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)

Tactic:
⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
refine_1 :
  ∀
    (h :
      ∀ (t1 t2 : Set Ω),
        MeasurableSet t1 →
          MeasurableSet t2 →
            μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
              HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m'])
    (s : Set β) (t : Set β') (hs : MeasurableSet s) (ht : MeasurableSet t),
    (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω) (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
refine_2 :
  ∀
    (h :
      ∀ (s : Set β) (t : Set β'),
        MeasurableSet s →
          MeasurableSet t →
            (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
                (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω))
    (s t : Set Ω),
    MeasurableSet s →
      MeasurableSet t →
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)

Tactic:
refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
    HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω) (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)

Tactic:
h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Premises used: Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
    HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω) (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)

Tactic:
exact h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Premises used: Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
            (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
h s t hs ht
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
            (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
exact h s t hs ht
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
rw :
  (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
hf₁ : ∀ (i : ι), Measurable (f i)
⊢ iCondIndepFun m' hm' (β := β) f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
rw [iCondIndepFun_iff]

Premises used: ProbabilityTheory.iCondIndepFun_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : ι), Measurable (f i)

Tactic:
hf
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : ι), Measurable (f i)

Tactic:
exact hf
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
        (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
          (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m']))
    (s : Finset ι) (sets : (i : ι) → Set (β i)) (h_sets : ∀ i ∈ s, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
refine_2 :
  ∀
    (h :
      ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
        (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
          (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m']))
    (s : Finset ι) (sets : ι → Set Ω) (h_sets : ∀ i ∈ s, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])
s : Finset ι
sets : (i : ι) → Set (β i)
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])
s : Finset ι
sets : (i : ι) → Set (β i)
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
refine_1 : ∀ (i : ι) (hi : i ∈ s), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ f i ⁻¹' sets i) i)
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
refine h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)