awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
⊢ μ = ν
have this : Set.Countable.{u_5} (α := Set α) (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l ≤ u), {Icc l u})
Tactic: have : (⋃ (l ∈ s) (u ∈ s) (_ : l ≤ u), {Icc l u} : Set (Set α)).Countable :=
    hsc.biUnion fun l _ => hsc.biUnion fun u _ => countable_iUnion fun _ => countable_singleton _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : Set.Countable.{u_5} (α := Set α) (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l ≤ u), {Icc l u})
⊢ μ = ν
have this₁ : Set.Countable.{u_5} (α := Set α)
  {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
Tactic: simp only [← setOf_eq_eq_singleton, ← setOf_exists] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
⊢ μ = ν
have refine_1 : Subset.{u_5} (α := Set (Set α)) {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
  {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S}
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
    {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S}
⊢ μ = ν
have refine_2 : Eq.{u_5 + 1} (α := Set α) (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2})
  univ
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
    {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S}
refine_2 :
  Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}) univ
⊢ μ = ν
have refine_3 : ∀ (s_1 : Set α),
  Membership.mem (γ := Set (Set α))
      {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} s_1 →
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
    {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S}
refine_2 :
  Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}) univ
refine_3 :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} s_1 →
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ = ν
have refine_4 : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S} s →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
⊢ Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}) univ
have refine_2 : ∀ (x : α),
  ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} b ∧
      x ∈ b
Tactic: refine sUnion_eq_univ_iff.2 fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
x : α
⊢ ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} b ∧
      x ∈ b
have refine_2 : ∀ (l : α) (hls : l ∈ s) (hlx : l ≤ x),
  ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} b ∧
      x ∈ b
Tactic: rcases hsd.exists_le' hsb x with ⟨l, hls, hlx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this :
  Set.Countable.{u_5} (α := Set α)
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}
x l : α
hls : l ∈ s
hlx : l ≤ x
⊢ ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} b ∧
      x ∈ b
have refine_2 : ∀ (u : α) (hus : u ∈ s) (hxu : x ≤ u),
  ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} b ∧
      x ∈ b
Tactic: rcases hsd.exists_ge' hst x with ⟨u, hus, hxu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 ⁻¹' Iio x)
⊢ Measurable f
have h : mα = MeasurableSpace.generateFrom (range Iio)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 ⁻¹' Iio x)
h : mα = MeasurableSpace.generateFrom (range Iio)
⊢ Measurable f
have convert_2 : Set (Set α)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 ⁻¹' Iio x)
h : mα = MeasurableSpace.generateFrom (range Iio)
convert_2 : Set (Set α)
⊢ Measurable f
have convert_4 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) t → MeasurableSet (f ⁻¹' t)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
have h : mα = MeasurableSpace.generateFrom (range Ioi)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable f
have convert_2 : Set (Set α)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 α)
⊢ Measurable f
have convert_4 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Ioi) t → MeasurableSet (f ⁻¹' t)
Tactic: convert! measurable_generateFrom (α := δ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
have refine : ∀ (c : β), MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
Tactic: refine measurable_of_Ioi fun c ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : β
⊢ MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
have obtain : ∀ (J : Set ι) (cJ : J.Countable) (dJ : Dense J), MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
Tactic: obtain ⟨J, cJ, dJ⟩ := TopologicalSpace.exists_countable_dense ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
have rw : MeasurableSet.{u_4} (α := δ) (⋃ j ∈ J, {x : δ | c < f j x})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ MeasurableSet.{u_4} (α := δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c)
have suffices : Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
Tactic: suffices (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]
    exact .biUnion cJ fun j _ ↦ by measurability
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ Eq.{u_4 + 1} (α := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) (⋃ j ∈ J, {x : δ | c < f j x})
have h : ∀ (x : δ),
  Membership.mem (γ := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) x ↔
    Membership.mem (γ := Set δ) (⋃ j ∈ J, {x : δ | c < f j x}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : δ
⊢ Membership.mem (γ := Set δ) ((⨆ (i : ι), f i) ⁻¹' Ioi c) x ↔
    Membership.mem (γ := Set δ) (⋃ j ∈ J, {x : δ | c < f j x}) x
have h : c < (⨆ (i : ι), f i) x ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
Tactic: push _ ∈ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : δ
⊢ c < (⨆ (i : ι), f i) x ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
have h : (∃ (i : ι), c < f i x) ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
Tactic: simp_rw [iSup_apply, lt_iSup_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : ι), c < f i x) ↔ ∃ (i : ι) (_ : i ∈ J), c < f i x
have h : (∃ (i : ι), c < f i x) → ∀ (i : ι) (hi : c < f i x), ∃ (i : ι) (_ : i ∈ J), c < f i x
Tactic: refine ⟨fun ⟨i, hi⟩ ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
have 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
Tactic: obtain ⟨v, hv, hv'⟩ := eventually_iff_exists_mem.1 (cf x i c hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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
⊢ ∃ (i : ι) (_ : i ∈ J), c < f i x
have hj : (J ∩ v).Nonempty
Tactic: have hj := dJ.inter_nhds_nonempty hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable f
have hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
Tactic: apply measurable_of_Ioi
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable f
have hf₁ : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
Tactic: apply measurable_of_Iio
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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)
⊢ Measurable g
have hg₁ : ∀ (b : δ), IsLUB (range fun (i : ι) ↦ f i b) (g b)
Tactic: change ∀ b, IsLUB (range fun i => f i b) (g b) at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable g
have rw : Measurable g
Tactic: rw [‹BorelSpace α›.measurable_eq, borel_eq_generateFrom_Ioi α]