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 α
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

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 α
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_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
⊢ 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 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 α
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 : α
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
⊢ ∃ (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⟩

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 α
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
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
⊢ ∃ (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⟩

Premises used: Dense.exists_gt
-- 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 α
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
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:
⟨_, ⟨l, hls, u, hus, hlx.trans_lt hxu, rfl⟩, hlx, hxu⟩

Premises used: And.intro, Exists.intro, LE.le.trans_lt, 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 α
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
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:
exact ⟨_, ⟨l, hls, u, hus, hlx.trans_lt 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 α
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}
l u : α
hlt : l < u
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico 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 α
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}
l u : α
hlt : l < u
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico 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 α
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}
l u : α
hlt : l < u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico l u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico 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 α
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}
l u : α
hlt : l < u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico l u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico 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 : 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∞)
⊢ μ = ν

Tactic:
@ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_

Premises used: MeasureTheory.Measure.ext_of_Ico', OrderDual
-- 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 α
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∞)
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' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_

Premises used: MeasureTheory.Measure.ext_of_Ico'
-- 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 α
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
refine_1 :
  Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
erw [Ico_toDual (α := α)]

Premises used: Set.Ico_toDual
-- 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 α
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
refine_2 :
  Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
    ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)

Tactic:
erw [Ico_toDual (α := α)]

Premises used: Set.Ico_toDual
-- 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 α
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∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hμ hab

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, OrderDual
-- 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 α
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∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)
    ((ν : (a : Set αᵒᵈ) → ℝ≥0∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞)

Tactic:
h hab

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, OrderDual
-- 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 α
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∞) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exacts [hμ hab, h hab]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
_m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
inst_5 : NoMaxOrder α
μ ν : Measure α
inst_6 : IsLocallyFiniteMeasure μ
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞)
⊢ μ = ν

Tactic:
μ.ext_of_Ico' ν (fun _ _ _ => measure_Ico_lt_top.ne) h

Premises used: measure_Ico_lt_top, MeasureTheory.Measure.ext_of_Ico', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
_m : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
inst_5 : NoMinOrder α
μ ν : Measure α
inst_6 : IsLocallyFiniteMeasure μ
h :
  ∀ ⦃a b : α⦄,
    a < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)
⊢ μ = ν

Tactic:
μ.ext_of_Ioc' ν (fun _ _ _ => measure_Ioc_lt_top.ne) h

Premises used: MeasureTheory.Measure.ext_of_Ioc', measure_Ioc_lt_top, LT.lt.ne
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext_of_Ioc_finite μ ν ?_ fun a b hlt => ?_

Premises used: MeasureTheory.Measure.ext_of_Ioc_finite
-- 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 α
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∞)
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 => ?_

Premises used: MeasureTheory.Measure.ext_of_Ioc_finite
-- 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 α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩

Premises used: exists_countable_dense_bot_top
-- 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 α
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
have : DirectedOn (· ≤ ·) s := directedOn_iff_directed.2 (Subtype.mono_coe _).directed_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 α
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
this : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp only [← biSup_measure_Iic hsc (hsd.exists_ge' hst) this, h]

Premises used: MeasureTheory.biSup_measure_Iic, 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 α
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∞)
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∞)

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]

Premises used: Iff.mpr, Set.Iic_subset_Iic, LT.lt.le, MeasureTheory.measure_diff, Set.Iic_diff_Iic, nullMeasurableSet_Iic
-- 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 α
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∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← h a]
-- 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 α
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∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
x : MeasurableSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : BorelSpace α
μ ν : Measure α
inst_5 : IsFiniteMeasure μ
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ici a) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ici a) : ℝ≥0∞)
⊢ μ = ν

Tactic:
@ext_of_Iic αᵒᵈ _ _ _ _ _ ‹_› _ _ _ h

Premises used: MeasureTheory.Measure.ext_of_Iic, OrderDual
-- 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∞)
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⟩

Premises used: exists_countable_dense_bot_top