awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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']
⊢ (∀ (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']
have 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∞)
Tactic: refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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
⊢ μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have 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∞)
Tactic: specialize h s t hs ht
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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
⊢ ∀ᵐ (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∞)
have h₁ : μ[(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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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∞)
⊢ μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have 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∞)
Tactic: have h' := ae_eq_of_ae_eq_trim h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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∞)
⊢ μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have 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'] ω
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'
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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'_1 :
  (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∞)
ω : Ω
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'] ω
have h₁ : ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
  HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
Tactic: rw [← hst_eq, Pi.mul_apply, ← hs_eq, ← ht_eq, h', ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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∞)
have refine_2 : (ae μ).EventuallyEq (β := ℝ≥0∞)
  (fun (ω : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
  fun (a : Ω) ↦
  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: refine ((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 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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']
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (ω : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
    fun (a : Ω) ↦
    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∞)
have 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 :
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω),
  (((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∞)
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
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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_1 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
ω : Ω
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 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
⊢ (((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∞)
have h_ne_top : Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: have h_ne_top : condExpKernel μ m' ω (s ∩ t) ≠ ∞ := measure_ne_top (condExpKernel μ m' ω) _