awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
⊢ ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}

Tactic:
have A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c} := by
    intro i c
    exact measurableSet_le (hf i) measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
c : α
rw : MeasurableSet.{u_4} (α := δ) (⋂ (i : ι), {x : δ | f i x ≤ c})
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}

Tactic:
rw [setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
c : α
⊢ MeasurableSet.{u_4} (α := δ) (⋂ (i : ι), {x : δ | f i x ≤ c})

Tactic:
MeasurableSet.iInter (fun i ↦ A i c)

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
c : α
⊢ MeasurableSet.{u_4} (α := δ) (⋂ (i : ι), {x : δ | f i x ≤ c})

Tactic:
exact MeasurableSet.iInter (fun i ↦ A i c)

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
⊢ ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}

Tactic:
have B : ∀ (c : α), MeasurableSet {x | ∀ i, f i x ≤ c} := by
    intro c
    rw [setOf_forall]
    exact MeasurableSet.iInter (fun i ↦ A i c)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
⊢ ∃ (u : ℕ → α), Tendsto u atTop atTop

Tactic:
exists_seq_tendsto (atTop : Filter α)

Premises used: Filter.atTop, Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
inr :
  ∀ (u : ℕ → α) (hu : Tendsto u atTop atTop),
    MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
obtain ⟨u, hu⟩ : ∃ (u : ℕ → α), Tendsto u atTop atTop := exists_seq_tendsto (atTop : Filter α)

Premises used: Filter.atTop, Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
h₁ :
  Subset.{u_4} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
h₂ :
  Subset.{u_4} (α := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
    {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
c : α
hc : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) c
⊢ ∃ (n : ℕ), c ≤ u n

Tactic:
(tendsto_atTop.1 hu c).exists

Premises used: Filter.tendsto_atTop, Filter.Eventually.exists, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
c : α
hc : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) c
h₁ : ∀ (n : ℕ) (hn : c ≤ u n), Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x
⊢ Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x

Tactic:
obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists

Premises used: Filter.tendsto_atTop, Filter.Eventually.exists, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
c : α
hc : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) c
n : ℕ
hn : c ≤ u n
⊢ Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x

Tactic:
⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩

Premises used: Set.mem_range_self, Set.Mem, setOf, Exists.intro, LE.le.trans
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
c : α
hc : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) c
n : ℕ
hn : c ≤ u n
⊢ Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x

Tactic:
exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
⊢ Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} x

Tactic:
⟨u n, ?_⟩

Premises used: Set.Mem, setOf, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
h₂ : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) (u n)
⊢ Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} x

Tactic:
refine ⟨u n, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
i : ι
⊢ (fun (i : ι) ↦ f i x) i ≤ u n

Tactic:
hn i
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
i : ι
⊢ (fun (i : ι) ↦ f i x) i ≤ u n

Tactic:
exact hn i
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}

Tactic:
have : {b | BddAbove (range (fun i ↦ f i b))} = {x | ∃ n, ∀ i, f i x ≤ u n} := by
    apply Subset.antisymm
    · rintro x ⟨c, hc⟩
      obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
      exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
    · rintro x ⟨n, hn⟩
      refine ⟨u n, ?_⟩
      rintro - ⟨i, rfl⟩
      exact hn i
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
this :
  Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
inr : MeasurableSet.{u_4} (α := δ) (⋃ (i : ℕ), {x : δ | ∀ (i_1 : ι), f i_1 x ≤ u i})
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
rw [this, setOf_exists]

Premises used: Set.setOf_exists
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
this :
  Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
⊢ MeasurableSet.{u_4} (α := δ) (⋃ (i : ℕ), {x : δ | ∀ (i_1 : ι), f i_1 x ≤ u i})

Tactic:
MeasurableSet.iUnion (fun n ↦ B (u n))

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
this :
  Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
⊢ MeasurableSet.{u_4} (α := δ) (⋃ (i : ℕ), {x : δ | ∀ (i_1 : ι), f i_1 x ≤ u i})

Tactic:
exact MeasurableSet.iUnion (fun n ↦ B (u n))

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
measurableSet_bddAbove_range (α := αᵒᵈ) hf

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, OrderDual, measurableSet_bddAbove_range
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b

Tactic:
simp_rw [ciSup_eq_ite]

Premises used: ciSup_eq_ite
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b

Tactic:
exact hf
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅

Tactic:
measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
neg neg₁ : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b

Tactic:
classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

Premises used: ciSup_eq_ite, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b

Tactic:
simp_rw [ciInf_eq_ite]

Premises used: ciInf_eq_ite
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅

Tactic:
measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
neg neg₁ : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b

Tactic:
classical
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

Premises used: ciInf_eq_ite, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
inl : ∀ (hι : IsEmpty ι), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
inr : ∀ (hι : Nonempty ι), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : IsEmpty ι
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b

Tactic:
simp [iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
have A : MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} :=
    measurableSet_bddAbove_range hf
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅

Tactic:
have : Measurable (fun (_b : δ) ↦ sSup (∅ : Set α)) := measurable_const