awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s_1 : Set α
hd : Dense s_1
hbot : ∀ (x : α), IsTop x → x ∈ s_1
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s_1
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
s : Set α
h :
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s →
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s
h₁ :
  Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s →
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s ↔
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Membership.mem (γ := Set (Set α))
    {S : Set αᵒᵈ |
      ∃ (l : αᵒᵈ),
        Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
          ∃ (u : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
    (Ioc l u)

Tactic:
⟨u, hu, l, hl, hlt, Ico_toDual⟩

Premises used: Set.Mem, setOf, Set.Ico_toDual, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
l : αᵒᵈ
hl : Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l
u : αᵒᵈ
hu : Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u
hlt : l < u
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} (Ico l u)

Tactic:
⟨u, hu, l, hl, hlt, Ioc_toDual⟩

Premises used: Set.Mem, setOf, Set.Ioc_toDual, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Membership.mem (γ := Set (Set α))
    {S : Set αᵒᵈ |
      ∃ (l : αᵒᵈ),
        Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
          ∃ (u : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
    (Ioc l u)

Tactic:
exacts [⟨u, hu, l, hl, hlt, Ico_toDual⟩, ⟨u, hu, l, hl, hlt, Ioc_toDual⟩]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
erw : Eq (α := Set α) ((⇑OrderDual.ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ) ⁻¹' Ioo x y) ∅
⊢ Ioo y x = ∅

Tactic:
erw [Ioo_toDual]

Premises used: Set.Ioo_toDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Eq (α := Set α) ((⇑OrderDual.ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ) ⁻¹' Ioo x y) ∅

Tactic:
he

Premises used: Set.Mem, setOf, Set.preimage, OrderDual, Set.Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Eq (α := Set α) ((⇑OrderDual.ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ) ⁻¹' Ioo x y) ∅

Tactic:
exact he
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
inst_4 : DenselyOrdered α
inst_5 : NoMaxOrder α
s : Set α
hd : Dense s
⊢ ∀ (x : α), IsTop x → x ∈ s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ioc l u = S}

Tactic:
simpa only [exists_prop, mem_univ, true_and] using
    (@dense_univ α _).borel_eq_generateFrom_Ioc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _

Premises used: dense_univ, exists_prop, Dense.borel_eq_generateFrom_Ioc_mem_aux, Set.mem_univ, true_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : borel α ≤ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
a₁ : MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} ≤ borel α
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a :
  LE.le.{u_5} (α := MeasurableSpace α)
    (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ioc l u = S})
    (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S})
⊢ borel α ≤ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}

Tactic:
rw [borel_eq_generateFrom_Ioc]

Premises used: borel_eq_generateFrom_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ Subset.{u_5} (α := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ioc l u = S}
    {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ LE.le.{u_5} (α := MeasurableSpace α)
    (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ioc l u = S})
    (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S})

Tactic:
apply generateFrom_mono (by grind)

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a :
  ∀ (t : Set α),
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} t → MeasurableSet t
⊢ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} ≤ borel α

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u v : α
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u v : α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ MeasurableSet (Ioc u v)

Tactic:
measurableSet_Ioc

Premises used: measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u v : α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ MeasurableSet (Ioc u v)

Tactic:
exact measurableSet_Ioc

Premises used: measurableSet_Ioc
-- 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μν : 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∞)
⊢ μ = ν

Tactic:
ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
      (isPiSystem_Ico (id : α → α) id) ?_ hμν

Premises used: MeasureTheory.ext_of_generate_finite, BorelSpace.measurable_eq, id, isPiSystem_Ico, borel_eq_generateFrom_Ico, 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 α
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∞)
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μν

Premises used: MeasureTheory.ext_of_generate_finite, BorelSpace.measurable_eq, id, isPiSystem_Ico, borel_eq_generateFrom_Ico, 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 α
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∞)
a b : α
hlt : a < b
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥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 α
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∞)
a b : α
hlt : a < b
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥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 α
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∞)
⊢ μ = ν

Tactic:
@ext_of_Ico_finite αᵒᵈ _ _ _ _ _ ‹_› μ ν _ hμν fun a b hab => ?_

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

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

Tactic:
exact h hab
-- 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∞)
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, _⟩

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 α
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
⊢ 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 _
-- 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 α) (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l < u), {Ico l u})
⊢ 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

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 α
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}
⊢ μ = ν

Tactic:
Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico id id) ?_ this
      ?_ ?_ ?_

Premises used: BorelSpace.measurable_eq, id, isPiSystem_Ico, borel_eq_generateFrom_Ico, 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 α
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∞)
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
      ?_ ?_ ?_

Premises used: BorelSpace.measurable_eq, id, isPiSystem_Ico, borel_eq_generateFrom_Ico, 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_1 :
  ∀ ⦃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 : α
h : l < u
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S} (Ico 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 α
inst_5 : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_1 :
  ∀ ⦃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 : α
h : l < u
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S} (Ico l u)

Tactic:
exact ⟨l, u, h, rfl⟩