awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
⊢ 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 _
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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})
⊢ 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

Premises used: Set.setOf_eq_eq_singleton, Set.setOf_exists
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
⊢ μ = ν

Tactic:
Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Icc, id, isPiSystem_Icc, MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
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
      ?_ ?_ ?_

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Icc, id, isPiSystem_Icc, MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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_1 :
  ∀ ⦃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}
l u : α
h : l ≤ u
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S} (Icc l u)

Tactic:
⟨l, u, h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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_1 :
  ∀ ⦃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}
l u : α
h : l ≤ u
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Icc l u = S} (Icc l u)

Tactic:
exact ⟨l, u, h, rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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

Tactic:
sUnion_eq_univ_iff.2 fun x => ?_

Premises used: Iff.mpr, Set.sUnion_eq_univ_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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_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
⊢ 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 sUnion_eq_univ_iff.2 fun x => ?_

Premises used: Iff.mpr, Set.sUnion_eq_univ_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : α
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
⊢ ∃ (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⟩

Premises used: Dense.exists_le'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ ∃ (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⟩

Premises used: Dense.exists_ge'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
⟨_, ⟨l, hls, u, hus, hlx.trans hxu, rfl⟩, hlx, hxu⟩

Premises used: And.intro, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
exact ⟨_, ⟨l, hls, u, hus, hlx.trans hxu, rfl⟩, hlx, hxu⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
l u : α
hlt : l ≤ u
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hμ hlt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
l u : α
hlt : l ≤ u
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hμ hlt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
l u : α
hlt : l ≤ u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞)

Tactic:
h hlt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
l u : α
hlt : l ≤ u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc l u) : ℝ≥0∞)

Tactic:
exact h hlt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
_m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : CompactIccSpace α
inst_5 : BorelSpace α
μ ν : Measure α
inst_6 : IsLocallyFiniteMeasure μ
h :
  ∀ ⦃a b : α⦄,
    a ≤ b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
⊢ μ = ν

Tactic:
μ.ext_of_Icc' ν (fun _ _ _ => measure_Icc_lt_top.ne) h

Premises used: measure_Icc_lt_top, MeasureTheory.Measure.ext_of_Icc', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
inst_3 : OrderClosedTopology α
⊢ MeasurableSet [[a, b]]

Tactic:
measurableSet_Icc

Premises used: measurableSet_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
inst_3 : ClosedIicTopology α
⊢ MeasurableSet (Ι a b)

Tactic:
measurableSet_Ioc

Premises used: Set.uIoc, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_4, u_1} (β := α) fun (a : δ) ↦ Max.max (f a) (g a)

Tactic:
simpa only [max_def'] using hf.piecewise (measurableSet_le hg hf) hg

Premises used: measurableSet_le, Measurable.piecewise, max_def'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
μ : Measure δ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (a : δ) ↦ Max.max (f a) (g a)) μ

Tactic:
⟨fun a => max (hf.mk f a) (hg.mk g a), hf.measurable_mk.max hg.measurable_mk,
    EventuallyEq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩

Premises used: Measurable.max, AEMeasurable, AEMeasurable.mk, Filter.EventuallyEq.comp₂, Max.max, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_4, u_1} (β := α) fun (a : δ) ↦ Min.min (f a) (g a)

Tactic:
simpa only [min_def] using hf.piecewise (measurableSet_le hf hg) hg

Premises used: measurableSet_le, Measurable.piecewise, min_def
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
μ : Measure δ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (a : δ) ↦ Min.min (f a) (g a)) μ

Tactic:
⟨fun a => min (hf.mk f a) (hg.mk g a), hf.measurable_mk.min hg.measurable_mk,
    EventuallyEq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩

Premises used: AEMeasurable, AEMeasurable.mk, Filter.EventuallyEq.comp₂, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, Measurable.min, Min.min, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : TopologicalSpace γ
mγ : MeasurableSpace γ
inst_3 : BorelSpace γ
inst_4 : SecondCountableTopology γ
inst_5 : Max γ
inst_6 : ContinuousSup γ
⊢ MeasurableSup₂ γ

Tactic:
⟨continuous_sup.measurable⟩

Premises used: ContinuousSup.continuous_sup, Continuous.measurable, MeasurableSup₂.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : TopologicalSpace γ
mγ : MeasurableSpace γ
inst_3 : BorelSpace γ
inst_4 : SecondCountableTopology γ
inst_5 : Min γ
inst_6 : ContinuousInf γ
⊢ MeasurableInf₂ γ

Tactic:
⟨continuous_inf.measurable⟩

Premises used: MeasurableInf₂.mk, Continuous.measurable, ContinuousInf.continuous_inf
-- 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 ⁻¹' Iio 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 ⁻¹' Iio x)
h : mα = MeasurableSpace.generateFrom (range Iio)
convert_2 : Set (Set α)
convert_4 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) 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 ⁻¹' Iio x)
⊢ mα = MeasurableSpace.generateFrom (range Iio)

Tactic:
BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Iio, 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 ⁻¹' Iio x)
⊢ mα = MeasurableSpace.generateFrom (range Iio)

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

Premises used: BorelSpace.measurable_eq, borel_eq_generateFrom_Iio, 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 ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio 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 ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)

Tactic:
exact hf x