awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u v : α
⊢ MeasurableSet (Ioc u v)
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- 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 α
inst_5 : IsFiniteMeasure μ
hμν : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
⊢ μ = ν
have ext_of_generate_finite : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S} s →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine
    ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
      (isPiSystem_Ico (id : α → α) id) ?_ hμν
-- 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 α
inst_5 : IsFiniteMeasure μ
hμν : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
⊢ μ = ν
have refine : ∀ (a b : αᵒᵈ) (hab : a < b),
  Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
Tactic: refine @ext_of_Ico_finite αᵒᵈ _ _ _ _ _ ‹_› μ ν _ hμν fun a b hab => ?_
-- 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 α
inst_5 : IsFiniteMeasure μ
hμν : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
a b : αᵒᵈ
hab : a < b
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
have erw : Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
  ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
Tactic: erw [Ico_toDual (α := α)]
-- 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
⊢ μ = ν
have rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s) (hsb : ∀ (x : α), IsBot x → x ∈ s),
  (∀ (x : α), IsTop x → x ∈ s) → μ = ν
Tactic: rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, _⟩
-- 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (x : α), IsTop x → x ∈ s
⊢ μ = ν
have this : Set.Countable.{u_5} (α := Set α) (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l < u), {Ico l u})
Tactic: have : (⋃ (l ∈ s) (u ∈ s) (_ : l < u), {Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (x : α), IsTop x → x ∈ s
this : Set.Countable.{u_5} (α := Set α) (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l < u), {Ico l u})
⊢ μ = ν
have this₁ : Set.Countable.{u_5} (α := Set α)
  {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico 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 = Ico i i_2}
  {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S}
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}
    {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico 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 = Ico i i_2})
  univ
Tactic: refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}
    {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S}
refine_2 :
  Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico 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 = Ico 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_Ico α)) (isPiSystem_Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico i i_2}
refine_1 :
  Subset.{u_5} (α := Set (Set α))
    {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}
    {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S}
refine_2 :
  Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico 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 = Ico 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 ∧ Ico 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_Ico α)) (isPiSystem_Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico i i_2}
⊢ Eq.{u_5 + 1} (α := Set α)
    (⋃₀ {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico 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 = Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico i i_2}
x : α
⊢ ∃ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ (i : α) (_ : i ∈ s) (i_2 : α) (_ : i_2 ∈ s) (_ : i < i_2), x = Ico 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 = Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right : ∀ (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 = Ico 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 = Ico 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 = Ico i i_2} b ∧
      x ∈ b
Tactic: rcases hsd.exists_gt x with ⟨u, hus, hxu⟩
-- 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 α
inst_5 : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
⊢ μ = ν
have refine_1 : ∀ ⦃a b : αᵒᵈ⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_
-- 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 α
inst_5 : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
refine_1 : ∀ ⦃a b : αᵒᵈ⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ = ν
have refine_2 : ∀ ⦃a b : αᵒᵈ⦄,
  a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
Tactic: refine @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_
-- 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 α
inst_5 : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
a b : αᵒᵈ
hab : a < b
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: erw [Ico_toDual (α := α)]
-- 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 α
inst_5 : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
a b : αᵒᵈ
hab : a < b
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
  ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
Tactic: erw [Ico_toDual (α := α)]
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
⊢ μ = ν
have refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: refine ext_of_Ioc_finite μ ν ?_ fun a b hlt => ?_
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ μ = ν
have refine_2 : ∀ (a b : α) (hlt : a < b),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
Tactic: refine ext_of_Ioc_finite μ ν ?_ fun a b hlt => ?_
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have refine_1 : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s) (hst : ∀ (x : α), IsTop x → x ∈ s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
s : Set α
hsc : s.Countable
hsd : Dense s
hst : ∀ (x : α), IsTop x → x ∈ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have this : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: have : DirectedOn (· ≤ ·) s := directedOn_iff_directed.2 (Subtype.mono_coe _).directed_le
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
a b : α
hlt : a < b
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
have refine_2 : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic,
    measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic, h a, h b]
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
a b : α
hlt : a < b
refine_2 : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
have refine_2₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic,
    measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic, h a, h b]
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
a b : α
hlt : a < b
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← h a]
-- 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∞)
⊢ μ = ν
have rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s) (hsb : ∀ (x : α), IsBot x → x ∈ s) (hst : ∀ (x : α), IsTop x → x ∈ s),
  μ = ν
Tactic: rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, hst⟩