Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} ⊆ {S | ∃ l u, l ≤ u ∧ Icc l u = S}

pp: case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} = univ

pp: case refine_3
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s

Tactic:
· rintro _ ⟨l, -, u, -, h, rfl⟩
    exact ⟨l, u, h, rfl⟩

Goal state after:
case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} = univ

case refine_3
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, μ s_1 ≠ ∞

case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s