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Ω
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
h_ne_top :
  Ne (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Ne (α := ℝ≥0∞) (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) ∞
⊢ Eq (α := ℝ) (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (∏ i ∈ s, ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))

Tactic:
Finset.prod_congr rfl (fun i hi ↦ (h_eq i hi).symm)

Premises used: Finset.prod_congr, Eq.symm, rfl
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
h_ne_top :
  Ne (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Ne (α := ℝ≥0∞) (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) ∞
⊢ Eq (α := ℝ) (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (∏ i ∈ s, ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))

Tactic:
exact Finset.prod_congr rfl (fun i hi ↦ (h_eq i hi).symm)

Premises used: Finset.prod_congr, Eq.symm, rfl
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
have hs1_eq : ∀ s ∈ s1, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs1 s hs)
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
⊢ ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
have hs2_eq : ∀ s ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs2 s hs)
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
⊢ ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
have hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (s ∩ t)))
      =ᵐ[μ] μ⟦s ∩ t | m'⟧ :=
    fun s hs t ht ↦ condExpKernel_ae_eq_condExp hm' ((hs1 s hs).inter ((hs2 t ht)))
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']

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

Premises used: Iff.intro
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
refine_1 :
  ∀
    (h :
      ∀ (t1 t2 : Set Ω),
        t1 ∈ s1 →
          t2 ∈ s2 →
            ∀ᵐ (a : Ω) ∂μ.trim hm',
              (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
                HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                  ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                  ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞))
    (s t : Set Ω) (hs : s ∈ s1) (ht : t ∈ s2),
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
refine_2 :
  ∀
    (h :
      ∀ (t1 t2 : Set Ω),
        t1 ∈ s1 →
          t2 ∈ s2 →
            μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
              HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m'])
    (s t : Set Ω) (hs : s ∈ s1) (ht : t ∈ s2),
    ∀ᵐ (a : Ω) ∂μ.trim hm',
      (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
h :
  ∀ (t1 t2 : Set Ω),
    t1 ∈ s1 →
      t2 ∈ s2 →
        ∀ᵐ (a : Ω) ∂μ.trim hm',
          (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
              ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
              ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
⊢ ∀ᵐ (a : Ω) ∂μ.trim hm',
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
specialize h s t hs ht
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
h :
  ∀ (t1 t2 : Set Ω),
    t1 ∈ s1 →
      t2 ∈ s2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
⊢ μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
specialize h s t hs ht
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h :
  ∀ᵐ (a : Ω) ∂μ.trim hm',
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (x : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
    fun (x : Ω) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have h' := ae_eq_of_ae_eq_trim h
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h :
  ∀ᵐ (a : Ω) ∂μ.trim hm',
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
h' :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (x : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
    fun (x : Ω) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  ∀ (ω : Ω)
    (hs_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
        μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (ht_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
        μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (hst_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (h' :
      (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)),
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
⊢ μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h'] with ω hs_eq ht_eq hst_eq h'
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
⊢ ∀ᵐ (a : Ω) ∂μ.trim hm',
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
((stronglyMeasurable_condExpKernel ((hs1 s hs).inter (hs2 t ht))).ae_eq_trim_iff hm'
      ((measurable_condExpKernel (hs1 s hs)).mul
        (measurable_condExpKernel (hs2 t ht))).stronglyMeasurable).mpr ?_

Premises used: Iff.mpr, Measurable.mul, Measurable.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_condExpKernel, Filter.EventuallyEq, ProbabilityTheory.measurable_condExpKernel, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff, MeasurableSet.inter