awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.ZeroOne
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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
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
h₁ h₂ :
  ∀ (a : α) (ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)),
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Premises used: ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ
      ht_tail

Premises used: ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup, MeasureTheory.ae_dirac_eq, Filter.eventually_pure
-- Module: Mathlib.Probability.Independence.ZeroOne
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
⊢ ∀ᵐ (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_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ ht_tail)
-- Module: Mathlib.Probability.Independence.ZeroOne
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∞)
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := limsup_le_iSup.trans (iSup_le h_le) t ht_tail
-- Module: Mathlib.Probability.Independence.ZeroOne
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₁ :
  ∀ (ω : Ω)
    (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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    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ω

Premises used: ProbabilityTheory.condExpKernel_ae_eq_condExp
-- Module: Mathlib.Probability.Independence.ZeroOne
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
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
h₄ h₅ h₆ 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:
rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.measureReal_eq_zero_iff, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Independence.ZeroOne
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
⊢ ∀ (i : ι), BddAbove (ns i)

Tactic:
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
-- Module: Mathlib.Probability.Independence.ZeroOne
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) κ μα

Tactic:
indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_

Premises used: ProbabilityTheory.Kernel.indep_limsup_self
-- Module: Mathlib.Probability.Independence.ZeroOne
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
refine_3 : ∀ (n : ι), ∃ (a : ι), n ∈ ns a
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα

Tactic:
refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_

Premises used: ProbabilityTheory.Kernel.indep_limsup_self
-- Module: Mathlib.Probability.Independence.ZeroOne
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 ι),
    (∃ (x : ι), Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x} x) → ∃ (a : ι), ∀ b ≥ a, b ∉ t
⊢ ∀ (t : Set ι), BddAbove t → Membership.mem (γ := Filter ι) atTop tᶜ

Tactic:
simp only [mem_atTop_sets, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]

Premises used: Filter.mem_atTop_sets, upperBounds, BddAbove, Set.Nonempty, Set.mem_compl_iff
-- Module: Mathlib.Probability.Independence.ZeroOne
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 : ι), a < b

Tactic:
exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Probability.Independence.ZeroOne
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
refine_1 : ∀ (b : ι) (hb : a < b), ∃ (a : ι), ∀ b ≥ a, b ∉ t
⊢ ∃ (a : ι), ∀ b ≥ a, b ∉ t

Tactic:
obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Probability.Independence.ZeroOne
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

Tactic:
⟨b, fun c hc hct => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Probability.Independence.ZeroOne
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
refine_1 : ∀ (c : ι) (hc : c ≥ b) (hct : c ∈ t), False
⊢ ∃ (a : ι), ∀ b ≥ a, b ∉ t

Tactic:
refine ⟨b, fun c hc hct => ?_⟩
-- Module: Mathlib.Probability.Independence.ZeroOne
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
refine_1 : ∀ i ∈ t, i < c
⊢ False

Tactic:
suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)
-- Module: Mathlib.Probability.Independence.ZeroOne
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
⊢ ∀ i ∈ t, i < c

Tactic:
fun i hi => (ha hi).trans_lt (hb.trans_le hc)

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
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
⊢ ∀ i ∈ t, i < c

Tactic:
exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
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)
⊢ Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns

Tactic:
Monotone.directed_le fun i j hij k hki => le_trans hki hij

Premises used: Monotone.directed_le, le_trans
-- Module: Mathlib.Probability.Independence.ZeroOne
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)
⊢ Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns

Tactic:
exact Monotone.directed_le fun i j hij k hki => le_trans hki hij
-- Module: Mathlib.Probability.Independence.ZeroOne
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)
⊢ ∀ (n : ι), ∃ (a : ι), n ∈ ns a

Tactic:
fun n => ⟨n, le_rfl⟩

Premises used: le_rfl, Exists.intro
-- Module: Mathlib.Probability.Independence.ZeroOne
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)
⊢ ∀ (n : ι), ∃ (a : ι), n ∈ ns a

Tactic:
exact fun n => ⟨n, le_rfl⟩
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
⊢ Indep (limsup s atTop) (limsup s atTop) μ

Tactic:
Kernel.indep_limsup_atTop_self h_le h_indep

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_limsup_atTop_self
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
inst_3 : StandardBorelSpace Ω
hm : m ≤ m0
inst_4 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
⊢ CondIndep m (limsup s atTop) (limsup s atTop) hm μ

Tactic:
Kernel.indep_limsup_atTop_self h_le h_indep

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_limsup_atTop_self
-- Module: Mathlib.Probability.Independence.ZeroOne
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
apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (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:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)

Premises used: ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self', ProbabilityTheory.Kernel.indep_limsup_atTop_self, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- Module: Mathlib.Probability.Independence.ZeroOne
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 : α
ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Independence.ZeroOne
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
h₁ h₂ :
  ∀ (a : α) (ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)),
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Premises used: ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop h_le h_indep ht_tail

Premises used: ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop, MeasureTheory.ae_dirac_eq, Filter.eventually_pure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeSup ι
inst_1 : NoMaxOrder ι
inst_2 : Nonempty ι
inst_3 : StandardBorelSpace Ω
hm : m ≤ m0
inst_4 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1

Tactic:
condExp_eq_zero_or_one_of_condIndepSet_self hm (limsup_le_iSup.trans (iSup_le h_le) t ht_tail)
    ((condIndep_limsup_atTop_self hm h_le h_indep).condIndepSet_of_measurableSet ht_tail ht_tail)

Premises used: ProbabilityTheory.condIndep_limsup_atTop_self, ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet, Filter.limsup_le_iSup, iSup_le, LE.le.trans, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self
-- Module: Mathlib.Probability.Independence.ZeroOne
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
⊢ ∀ (i : ι), BddBelow (ns i)

Tactic:
have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
-- Module: Mathlib.Probability.Independence.ZeroOne
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) κ μα

Tactic:
indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_

Premises used: ProbabilityTheory.Kernel.indep_limsup_self
-- Module: Mathlib.Probability.Independence.ZeroOne
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
refine_3 : ∀ (n : ι), ∃ (a : ι), n ∈ ns a
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα

Tactic:
refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_

Premises used: ProbabilityTheory.Kernel.indep_limsup_self