awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst : StandardBorelSpace Ω
hm : m ≤ m0
inst_1 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
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∞)
ht : MeasurableSet t
ω : Ω
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 (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα
have hnsp : ∀ (i : ι), BddAbove (ns i)
Tactic: have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα
have refine_1 : ∀ (t : Set ι), BddAbove t → Membership.mem (γ := Filter ι) atTop tᶜ
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
refine_1 : ∀ (t : Set ι), BddAbove t → Membership.mem (γ := Filter ι) atTop tᶜ
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα
have refine_2 : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
refine_1 : ∀ (t : Set ι), BddAbove t → Membership.mem (γ := Filter ι) atTop tᶜ
refine_2 : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα
have refine_3 : ∀ (n : ι), ∃ (a : ι), n ∈ ns a
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → Membership.mem (γ := Filter ι) atTop tᶜ
have refine_1 : ∀ (t : Set ι), (∃ (x : ι), Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x} x) → ∃ (a : ι), ∀ b ≥ a, b ∉ t
Tactic: simp only [mem_atTop_sets, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x} a
⊢ ∃ (a : ι), ∀ b ≥ a, b ∉ t
have refine_1 : ∀ (b : ι) (hb : a < b), ∃ (a : ι), ∀ b ≥ a, b ∉ t
Tactic: obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x} a
b : ι
hb : a < b
⊢ ∃ (a : ι), ∀ b ≥ a, b ∉ t
have refine_1 : ∀ (c : ι) (hc : c ≥ b) (hct : c ∈ t), False
Tactic: refine ⟨b, fun c hc hct => ?_⟩
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x} a
b : ι
hb : a < b
c : ι
hc : c ≥ b
hct : c ∈ t
⊢ False
have refine_1 : ∀ i ∈ t, i < c
Tactic: suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet 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 apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
Tactic: apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
    a
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- 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 α
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h₁ : ∀ (a : α),
  IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a) →
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα
have hnsp : ∀ (i : ι), BddBelow (ns i)
Tactic: have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα
have refine_1 : ∀ (t : Set ι), BddBelow t → Membership.mem (γ := Filter ι) atBot tᶜ
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
refine_1 : ∀ (t : Set ι), BddBelow t → Membership.mem (γ := Filter ι) atBot tᶜ
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα
have refine_2 : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
refine_1 : ∀ (t : Set ι), BddBelow t → Membership.mem (γ := Filter ι) atBot tᶜ
refine_2 : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα
have refine_3 : ∀ (n : ι), ∃ (a : ι), n ∈ ns a
Tactic: refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → Membership.mem (γ := Filter ι) atBot tᶜ
have refine_1 : ∀ (t : Set ι), (∃ (x : ι), Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} x) → ∃ (a : ι), ∀ b ≤ a, b ∉ t
Tactic: simp only [mem_atBot_sets, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
⊢ ∃ (a : ι), ∀ b ≤ a, b ∉ t
have refine_1 : ∀ (b : ι) (hb : b < a), ∃ (a : ι), ∀ b ≤ a, b ∉ t
Tactic: obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
⊢ ∃ (a : ι), ∀ b ≤ a, b ∉ t
have refine_1 : ∀ (c : ι) (hc : c ≤ b) (hct : c ∈ t), False
Tactic: refine ⟨b, fun c hc hct => ?_⟩
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False
have refine_1 : ∀ i ∈ t, c < i
Tactic: suffices ∀ i ∈ t, c < i from lt_irrefl c (this c hct)
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet 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 apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
Tactic: apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atBot_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
    a
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- 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 α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h₁ : ∀ (a : α),
  IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a) →
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.dirac (f a)
have refine : ∀ (s : Set β) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((Measure.dirac (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((Measure.dirac (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 (f b)
Tactic: simp_rw [Measure.dirac_apply' _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)
have rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
Tactic: rw [deterministic_apply, lintegral_dirac' _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)
have rw₁ : f (g a) = f (g a)
Tactic: rw [deterministic_apply, lintegral_dirac' _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)
have rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
Tactic: rw [deterministic_apply, lintegral_dirac (g a) f]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)
have rw₁ : f (g a) = f (g a)
Tactic: rw [deterministic_apply, lintegral_dirac (g a) f]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0
have rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setLIntegral_dirac' hf hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst : Decidable (g a ∈ s)
rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0
have rw₁ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setLIntegral_dirac' hf hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
s : Set β
inst_1 : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0
have rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setLIntegral_dirac f s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
s : Set β
inst_1 : Decidable (g a ∈ s)
rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0
have rw₁ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setLIntegral_dirac f s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Eq (α := Measure α) ((Kernel.id : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
have rw : Eq (α := Measure α) ((deterministic id sorry : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
Tactic: rw [Kernel.id, deterministic_apply, id_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
rw : Eq (α := Measure α) ((deterministic id ⋯ : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
⊢ Eq (α := Measure α) ((Kernel.id : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
have rw₁ : Eq (α := Measure α) (Measure.dirac (id a)) (Measure.dirac a)
Tactic: rw [Kernel.id, deterministic_apply, id_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
rw : Eq (α := Measure α) ((deterministic id ⋯ : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
rw₁ : Eq (α := Measure α) (Measure.dirac (id a)) (Measure.dirac a)
⊢ Eq (α := Measure α) ((Kernel.id : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
have rw₂ : Eq (α := Measure α) (Measure.dirac a) (Measure.dirac a)
Tactic: rw [Kernel.id, deterministic_apply, id_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a
have rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
Tactic: rw [id_apply, lintegral_dirac' _ hf]