awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
hyz : y ≠ z
hsz : sy ∈ cs
hzsz : z ∈ sy
⊢ r y z ∨ r z y

Tactic:
(hcs₀ hsy).right hysy hzsz hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
hyz : y ≠ z
hsz : sy ∈ cs
hzsz : z ∈ sy
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsy).right hysy hzsz hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
refine_1 : ∀ (h : sy ⊆ sz), r y z ∨ r z y
refine_1₁ : ∀ (h : sz ⊆ sy), r y z ∨ r z y
⊢ r y z ∨ r z y

Tactic:
rcases hcs₁ hsy hsz hsseq with h | h
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sy ⊆ sz
⊢ r y z ∨ r z y

Tactic:
(hcs₀ hsz).right (h hysy) hzsz hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sy ⊆ sz
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsz).right (h hysy) hzsz hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y

Tactic:
(hcs₀ hsy).right hysy (h hzsz) hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsy).right hysy (h hzsz) hyz

Premises used: And.right
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
c : Set α
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
⊢ ∃ (s : Flag α), c ⊆ (↑s : Set α)

Tactic:
let ⟨s, hs, hcs⟩ := hc.exists_maxChain; ⟨ofIsMaxChain s hs, hcs⟩

Premises used: Flag.ofIsMaxChain, _private.0.IsChain.exists_subset_flag.match_1, Exists, HasSubset.Subset, SetLike.coe, Exists.intro, IsChain.exists_maxChain
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ∃ (s : Flag α), a ∈ s

Tactic:
let ⟨s, hs⟩ := Set.subsingleton_singleton (a := a).isChain.exists_subset_flag
  ⟨s, hs rfl⟩

Premises used: IsChain.exists_subset_flag, Membership.mem, Exists, Set.Subsingleton.isChain, _private.0.Flag.exists_mem.match_1, Set.subsingleton_singleton, Exists.intro, rfl
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ (s : Flag α), a ∈ s ∧ b ∈ s

Tactic:
simpa [Set.insert_subset_iff] using (IsChain.pair hab).exists_subset_flag

Premises used: IsChain.pair, IsChain.exists_subset_flag, Set.insert_subset_iff
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
c_1 : Set α
inst : Preorder α
c : Set α
s : Flag α
a b : α
⊢ Nonempty.{u_1 + 1} (Flag α)

Tactic:
⟨.ofIsMaxChain _ maxChain_spec⟩

Premises used: maxChain_spec, Flag.ofIsMaxChain, Nonempty.intro
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α

Tactic:
⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩

Premises used: LE.le.eq_or_lt, IsCoatomic.mk, le_top, Or.imp_right
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
refine : ∀ (x : α) (hx : x < ⊤), ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ IsCoatomic α

Tactic:
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
refine_2 : ∀ (this : ∃ (m : α), x ≤ m ∧ Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) m), ∃ (a : α), IsCoatom a ∧ x ≤ a
refine_1 :
  ∀ (c : Set α) (hxc : c ⊆ Ico x ⊤) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c) (y : α) (hy : y ∈ c),
    ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ (m : α), x ≤ m ∧ Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) m
refine_2 : ∀ (y : α) (hxy : x ≤ y) (hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y), ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
obtain ⟨y, hxy, hmax⟩ := this
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩

Premises used: LE.le.eq_or_lt, Maximal.prop, And.right, le_top, And.intro, Exists.intro, Or.resolve_right, LT.lt.ne
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y
refine_2 : ∀ (z : α) (hyz : y < z) (hz : z < ⊤), False
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False

Tactic:
hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le

Premises used: LT.lt.le, Maximal.eq_of_le, And.intro, LE.le.trans, LT.lt.ne
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun (x_1 : α) ↦ x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False

Tactic:
exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le

Premises used: LT.lt.le, Maximal.eq_of_le, And.intro, LE.le.trans, LT.lt.ne
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
refine_1 : ∀ (z : α) (hz : z ≠ ⊤) (hcz : z ∈ upperBounds c), ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩

Premises used: And.right, Exists.intro, rfl, LT.lt.ne
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩

Premises used: And.left, Ne.lt_top, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : α), x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
-- Module: Mathlib.Order.ZornAtoms
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → ⊥ ∉ c → ∃ (x : α), x ≠ ⊥ ∧ x ∈ lowerBounds c
⊢ IsAtomic α

Tactic:
isCoatomic_dual_iff_isAtomic.mp <| IsCoatomic.of_isChain_bounded fun c hc => h c hc.symm

Premises used: IsChain.symm, isCoatomic_dual_iff_isAtomic, Iff.mp, IsCoatomic.of_isChain_bounded
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
this :
  Indep (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j} k), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Indep (MeasurableSpace.comap (f j) mβ)
        (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ),
    Indep (MeasurableSpace.comap (f j) mβ)
      ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i)
    μ

Tactic:
rwa [iSup_singleton] at this

Premises used: iSup_singleton
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
suffices :
  Indep (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j} k), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) ((↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i)
    μ

Tactic:
suffices Indep (⨆ k ∈ ({j} : Set ι), MeasurableSpace.comap (f k) mβ)
      (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ by rwa [iSup_singleton] at this
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
⊢ Disjoint (α := Set ι) {j} {k : ι | k ≤ i}

Tactic:
simpa
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
⊢ Indep (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j} k), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι), ⨆ (_ : Membership.mem (γ := Set ι) {k : ι | k ≤ i} k), MeasurableSpace.comap (f k) mβ) μ

Tactic:
exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)

Premises used: MeasureTheory.StronglyMeasurable.measurable, Measurable.comap_le, ProbabilityTheory.indep_iSup_of_disjoint
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
inst_3 : SecondCountableTopology β
inst_4 : CompleteSpace β
inst_5 : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := hfi.isProbabilityMeasure
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
inst_3 : SecondCountableTopology β
inst_4 : CompleteSpace β
inst_5 : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
this : IsProbabilityMeasure μ
⊢ μ[f j | (↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] fun (x : Ω) ↦
    ∫ (x : Ω), f j x ∂μ

Tactic:
condExp_indep_eq (hf j).measurable.comap_le (Filtration.le _ _)
    (comap_measurable <| f j).stronglyMeasurable (hfi.indep_comap_natural_of_lt hf hij)

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, Measurable.comap_le, ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt, comap_measurable, MeasureTheory.Filtration.le, MeasureTheory.condExp_indep_eq
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst : LinearOrder ι
mβ : MeasurableSpace β
inst_1 : NormedAddCommGroup β
inst_2 : BorelSpace β
f : ι → Ω → β
i j : ι
inst_3 : SecondCountableTopology β
inst_4 : CompleteSpace β
inst_5 : NormedSpace ℝ β
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (β := fun (x : ι) ↦ β) f μ
hij : i < j
this : IsProbabilityMeasure μ
⊢ μ[f j | (↑(Filtration.natural (β := fun (i : ι) ↦ β) f hf) : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] fun (x : Ω) ↦
    ∫ (x : Ω), f j x ∂μ

Tactic:
exact condExp_indep_eq (hf j).measurable.comap_le (Filtration.le _ _)
    (comap_measurable <| f j).stronglyMeasurable (hfi.indep_comap_natural_of_lt hf hij)

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, Measurable.comap_le, ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt, comap_measurable, MeasureTheory.Filtration.le, MeasureTheory.condExp_indep_eq
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
rw :
  (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 |
      (↑(Filtration.natural (β := fun (x : ι) ↦ ℝ) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯) :
          ι → MeasurableSpace Ω)
        i]
    fun (x : Ω) ↦ μ.real (s j)
⊢ (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 | (↑(filtrationOfSet (s := s) hsm) : ι → MeasurableSpace Ω) i] fun (x : Ω) ↦
    μ.real (s j)

Tactic:
rw [Filtration.filtrationOfSet_eq_natural (β := fun _ ↦ ℝ) hsm]

Premises used: MeasureTheory.Filtration.filtrationOfSet_eq_natural
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 |
      (↑(Filtration.natural (β := fun (x : ι) ↦ ℝ) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯) :
          ι → MeasurableSpace Ω)
        i]
    fun (x : Ω) ↦ μ.real (s j)

Tactic:
(iIndepFun.condExp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans ?_

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, ProbabilityTheory.iIndepSet.iIndepFun_indicator
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
refine :
  (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), (s j).indicator (fun (_ω : Ω) ↦ 1) x ∂μ) fun (x : Ω) ↦
    μ.real (s j)
⊢ (ae μ).EventuallyEq (β := ℝ)
    μ[(s j).indicator fun (x : Ω) ↦ 1 |
      (↑(Filtration.natural (β := fun (x : ι) ↦ ℝ) (fun (i : ι) ↦ (s i).indicator fun (x : Ω) ↦ 1) ⋯) :
          ι → MeasurableSpace Ω)
        i]
    fun (x : Ω) ↦ μ.real (s j)

Tactic:
refine (iIndepFun.condExp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans ?_

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, ProbabilityTheory.iIndepSet.iIndepFun_indicator
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
simp : (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ μ.real (s j)) fun (x : Ω) ↦ μ.real (s j)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), (s j).indicator (fun (_ω : Ω) ↦ 1) x ∂μ) fun (x : Ω) ↦
    μ.real (s j)

Tactic:
simp only [integral_indicator_const _ (hsm _), smul_eq_mul, mul_one]

Premises used: MeasureTheory.integral_indicator_const, smul_eq_mul, mul_one
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : Ω) ↦ μ.real (s j)) fun (x : Ω) ↦ μ.real (s j)

Tactic:
rfl
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := hs.isProbabilityMeasure
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this : IsProbabilityMeasure μ
rw :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [measure_congr (eventuallyEq_set.2 (ae_mem_limsup_atTop_iff μ <|
    measurableSet_filtrationOfSet' hsm) : (limsup s atTop : Set Ω) =ᵐ[μ]
      {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
        (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop})]

Premises used: Iff.mpr, MeasureTheory.measure_congr, Filter.eventuallyEq_set, MeasureTheory.ae_mem_limsup_atTop_iff, MeasureTheory.measurableSet_filtrationOfSet'
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rw [measure_congr this, measure_univ]

Premises used: MeasureTheory.measure_congr, MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this : IsProbabilityMeasure μ
suffices :
  {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop} :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
suffices {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
      (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop} =ᵐ[μ] Set.univ by
    rw [measure_congr this, measure_univ]
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this : IsProbabilityMeasure μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)

Tactic:
have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ) | filtrationOfSet hsm n]) ω = _ :=
    ae_all_iff.2 fun n => hs.condExp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
h :
  ∀ (ω : Ω)
    (hω :
      ∀ (n : ℕ),
        μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω =
          μ.real (s (n + 1))),
    {ω : Ω |
          Tendsto (β := ℝ)
            (fun (n : ℕ) ↦
              ∑ k ∈ Finset.range n,
                μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
            atTop atTop}
        ω =
      Set.univ ω
⊢ {ω : Ω |
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦
          ∑ k ∈ Finset.range n,
            μ[(s (k + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) k] ω)
        atTop atTop} =ᶠ[ae μ]
    Set.univ

Tactic:
filter_upwards [this] with ω hω