awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (h_top : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h_top : κ a t = ∞
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (h_top : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (h_top : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h_top : κ a t = ∞
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h_top : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have ha₁ : Eq (α := ℝ≥0∞) (1 : ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← one_mul (κ a (t ∩ t)), Set.inter_self, ENNReal.mul_left_inj h0 h_top] at ha
Cleared hypotheses: ha, h0, h_top
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)
have h₁ : ∀ (a : α)
  (h_0_1_top :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h' : IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: filter_upwards [measure_eq_zero_or_one_or_top_of_indepSet_self h_indep, h] with a h_0_1_top h'
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
Tactic: have (a : _) : IsFiniteMeasure (condExpKernel μ m a) := inferInstance
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have h : ∀ᵐ (x : Ω) ∂μ,
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
Tactic: have h := ae_of_ae_trim hm (Kernel.measure_eq_zero_or_one_of_indepSet_self h_indep)
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have h₁ : ∀ (ω : Ω)
  (hω_eq :
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω)
  (hω :
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)),
  Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
Tactic: filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
ω : Ω
hω_eq : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω
hω :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have h₁ : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 0 ∨
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
Tactic: rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
ω : Ω
hω_eq : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω
hω :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
h₁ :
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 0 ∨
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
⊢ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have h₂ : Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
Tactic: rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
ω : Ω
hω_eq : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω
hω :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
h₁ :
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 0 ∨
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
h₂ :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
⊢ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have h₃ : Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) = 1
Tactic: rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) κ μα
have refine : limsup s f ≤ ⨆ n ∈ tᶜ, s n
Tactic: refine indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ limsup s f ≤ ⨆ n ∈ tᶜ, s n
have refine : ∀ᶠ (n : MeasurableSpace Ω) in Filter.map s f, n ≤ ⨆ n ∈ tᶜ, s n
Tactic: refine limsSup_le_of_le (by isBoundedDefault) ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (n : MeasurableSpace Ω) in Filter.map s f, n ≤ ⨆ n ∈ tᶜ, s n
have simp : ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι), ⨆ (_ : n ∉ t), s n
Tactic: simp only [Set.mem_compl_iff, eventually_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
have inl : ∀ (h_indep : iIndep s κ 0), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ 0
Tactic: rcases eq_or_ne μα 0 with rfl | hμ
Cleared hypotheses: μα, h_indep
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
inl : ∀ (h_indep : iIndep s κ 0), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ 0
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
have inr : ∀ (hμ : μα ≠ 0), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
Tactic: rcases eq_or_ne μα 0 with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
have inr : ∀ (η : Kernel α Ω)
  (η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
Tactic: obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μα] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
have h_indep₁ : iIndep s η μα
Tactic: replace h_indep := h_indep.congr η_eq
Cleared hypotheses: h_indep
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
have inr : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
Tactic: apply Indep.congr (Filter.EventuallyEq.symm η_eq)
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
have inr : ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα
Tactic: apply indep_iSup_of_directed_le
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
inr : ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
have inr₁ : ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0
Tactic: apply indep_iSup_of_directed_le
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
inr : ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα
inr₁ : ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
have inr₂ : limsup s f ≤ m0
Tactic: apply indep_iSup_of_directed_le
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
inr : ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα
inr₁ : ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0
inr₂ : limsup s f ≤ m0
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
have inr₃ : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) fun (i : β) ↦ ⨆ n ∈ ns i, s n
Tactic: apply indep_iSup_of_directed_le