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 α
inst_5 : TopologicalSpace δ
inst_6 : OpensMeasurableSpace δ
f : δ → α
hf : UpperSemicontinuous f
⊢ Measurable f

Tactic:
measurable_of_Iio fun y => (hf.isOpen_preimage y).measurableSet

Premises used: measurable_of_Iio, IsOpen.measurableSet, UpperSemicontinuous.isOpen_preimage
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ Measurable f

Tactic:
measurable_generateFrom (α := δ) _

Premises used: measurable_generateFrom
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
h : mα = MeasurableSpace.generateFrom (range Ioi)
convert_2 : Set (Set α)
convert_4 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Ioi) t → MeasurableSet (f ⁻¹' t)
⊢ Measurable f

Tactic:
convert! measurable_generateFrom (α := δ) _

Premises used: measurable_generateFrom
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ mα = MeasurableSpace.generateFrom (range Ioi)

Tactic:
BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ioi _)

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Ioi, Eq.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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ mα = MeasurableSpace.generateFrom (range Ioi)

Tactic:
exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ioi _)

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Ioi, Eq.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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Tactic:
hf x
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Tactic:
exact hf x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
⊢ Measurable.{u_4, u_2} (α := δ) (β := β) (⨆ (i : ι), f i)

Tactic:
measurable_of_Ioi fun c ↦ ?_

Premises used: measurable_of_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
refine : ∀ (c : β), MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
⊢ Measurable.{u_4, u_2} (α := δ) (β := β) (⨆ (i : ι), f i)

Tactic:
refine measurable_of_Ioi fun c ↦ ?_

Premises used: measurable_of_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
obtain : ∀ (J : Set ι) (cJ : J.Countable) (dJ : Dense J), MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
⊢ MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)

Tactic:
obtain ⟨J, cJ, dJ⟩ := TopologicalSpace.exists_countable_dense ι

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
rw : MeasurableSet.{u_4} (α := δ) (⋃ j ∈ J, {x : δ | c < f j x})
⊢ MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
j : ι
h : j ∈ J
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | c < f j x}

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
⊢ MeasurableSet.{u_4} (α := δ) (⋃ j ∈ J, {x : δ | c < f j x})

Tactic:
exact .biUnion cJ fun j _ ↦ by measurability
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
suffices : Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
⊢ MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)

Tactic:
suffices (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]
    exact .biUnion cJ fun j _ ↦ by measurability
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
h :
  ∀ (x : δ),
    Membership.mem (γ := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) x ↔
      Membership.mem (γ := Set δ) (⋃ j ∈ J, {x : δ | c < f j x}) x
⊢ Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : c < (⨆ (i : ι), f i) x ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
⊢ Membership.mem (γ := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) x ↔
    Membership.mem (γ := Set δ) (⋃ j ∈ J, {x : δ | c < f j x}) x

Tactic:
push _ ∈ _
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : (∃ (i : ι), c < f i x) ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
⊢ c < (⨆ (i : ι), f i) x ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x

Tactic:
simp_rw [iSup_apply, lt_iSup_iff]

Premises used: iSup_apply, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
⊢ (∃ (i : ι) (_ : i ∈ J), c < f i x) → ∃ (i : ι), c < f i x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : (∃ (i : ι), c < f i x) → ∀ (i : ι) (hi : c < f i x), ∃ (i : ι) (_ : i ∈ J), c < f i x
⊢ (∃ (i : ι), c < f i x) ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x

Tactic:
refine ⟨fun ⟨i, hi⟩ ↦ ?_, by grind⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h_1 : ∃ (i : ι), c < f i x
i : ι
hi : c < f i x
h :
  ∀ (v : Set ι) (hv : v ∈ 𝓝 i) (hv' : ∀ y ∈ v, (fun (x1 : ι) (x2 : β) ↦ (fun (x_1 : ι) ↦ f x_1 x) x1 > x2) y c),
    ∃ (i : ι) (_ : i ∈ J), c < f i x
⊢ ∃ (i : ι) (_ : i ∈ J), c < f i x

Tactic:
obtain ⟨v, hv, hv'⟩ := eventually_iff_exists_mem.1 (cf x i c hi)

Premises used: Iff.mp, Filter.eventually_iff_exists_mem
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : ∃ (i : ι), c < f i x
i : ι
hi : c < f i x
v : Set ι
hv : v ∈ 𝓝 i
hv' : ∀ y ∈ v, (fun (x1 : ι) (x2 : β) ↦ (fun (x_1 : ι) ↦ f x_1 x) x1 > x2) y c
⊢ (J ∩ v).Nonempty

Tactic:
have hj := dJ.inter_nhds_nonempty hv
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : ∃ (i : ι), c < f i x
i : ι
hi : c < f i x
v : Set ι
hv : v ∈ 𝓝 i
hv' : ∀ y ∈ v, (fun (x1 : ι) (x2 : β) ↦ (fun (x_1 : ι) ↦ f x_1 x) x1 > x2) y c
hj : (J ∩ v).Nonempty
⊢ ∃ (i : ι) (_ : i ∈ J), c < f i x

Tactic:
⟨hj.some, mem_of_mem_inter_left hj.some_mem,
    hv' _ (mem_of_mem_inter_right hj.some_mem)⟩

Premises used: Set.mem_of_mem_inter_left, Set.Nonempty.some_mem, Exists.intro, Set.mem_of_mem_inter_right, Set.Nonempty.some
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
h : ∃ (i : ι), c < f i x
i : ι
hi : c < f i x
v : Set ι
hv : v ∈ 𝓝 i
hv' : ∀ y ∈ v, (fun (x1 : ι) (x2 : β) ↦ (fun (x_1 : ι) ↦ f x_1 x) x1 > x2) y c
hj : (J ∩ v).Nonempty
⊢ ∃ (i : ι) (_ : i ∈ J), c < f i x

Tactic:
exact ⟨hj.some, mem_of_mem_inter_left hj.some_mem,
    hv' _ (mem_of_mem_inter_right hj.some_mem)⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
β : Type u_2
δ : Type u_4
inst : TopologicalSpace β
mβ : MeasurableSpace β
inst_1 : BorelSpace β
mδ : MeasurableSpace δ
inst_2 : CompleteLinearOrder β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
ι : Type u_5
inst_5 : TopologicalSpace ι
inst_6 : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), UpperSemicontinuous.{u_5, u_2} (β := β) fun (x_1 : ι) ↦ f x_1 x
⊢ Measurable.{u_4, u_2} (α := δ) (β := β) (⨅ (i : ι), f i)

Tactic:
measurable_iSup_of_lowerSemicontinuous (β := βᵒᵈ) mf cf

Premises used: iInf, measurable_iSup_of_lowerSemicontinuous, OrderDual
-- 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 α
inst_5 : TopologicalSpace δ
inst_6 : OpensMeasurableSpace δ
f : δ → α
hf : LowerSemicontinuous f
⊢ Measurable f

Tactic:
measurable_of_Ioi fun y => (hf.isOpen_preimage y).measurableSet

Premises used: IsOpen.measurableSet, measurable_of_Ioi, LowerSemicontinuous.isOpen_preimage
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ Measurable f

Tactic:
apply measurable_of_Ioi

Premises used: measurable_of_Ioi
-- 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 α
f : δ → α
hf hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)

Tactic:
simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]

Premises used: MeasurableSet.compl_iff, Set.compl_Iic, Set.preimage_compl
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)

Tactic:
assumption
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ Measurable f

Tactic:
apply measurable_of_Iio

Premises used: measurable_of_Iio
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)

Tactic:
simp_rw [← compl_Ici, preimage_compl, MeasurableSet.compl_iff]

Premises used: MeasurableSet.compl_iff, Set.compl_Ici, Set.preimage_compl
-- 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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)

Tactic:
assumption
-- 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
⊢ ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)

Tactic:
change ∀ b, IsLUB (range fun i => f i b) (g b) at hg
-- 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
rw : Measurable g
⊢ Measurable g

Tactic:
rw [‹BorelSpace α›.measurable_eq, borel_eq_generateFrom_Ioi α]

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Ioi
-- 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Ioi) t → MeasurableSet (g ⁻¹' t)
⊢ Measurable g

Tactic:
apply measurable_generateFrom

Premises used: measurable_generateFrom
-- 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
a : α
h : MeasurableSet.{u_4} (α := δ) (⋃ (i : ι), {x : δ | a < f i x})
⊢ MeasurableSet (g ⁻¹' Ioi a)

Tactic:
simp_rw [Set.preimage, mem_Ioi, lt_isLUB_iff (hg _), exists_range_iff, setOf_exists]

Premises used: lt_isLUB_iff, Set.mem_Ioi, Set.setOf_exists, Set.preimage, Set.exists_range_iff
-- 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
a : α
⊢ MeasurableSet.{u_4} (α := δ) (⋃ (i : ι), {x : δ | a < f i x})

Tactic:
MeasurableSet.iUnion fun i => hf i (isOpen_lt' _).measurableSet

Premises used: IsOpen.measurableSet, isOpen_lt', 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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
a : α
⊢ MeasurableSet.{u_4} (α := δ) (⋃ (i : ι), {x : δ | a < f i x})

Tactic:
exact MeasurableSet.iUnion fun i => hf i (isOpen_lt' _).measurableSet

Premises used: IsOpen.measurableSet, isOpen_lt', 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
inl : ∀ (hι : IsEmpty ι), Measurable g
inr : ∀ (i : ι), Measurable g
⊢ Measurable g

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨i⟩⟩

Premises used: isEmpty_or_nonempty