α : Type ?u.2411683
β : Type ?u.2411686
γ : Type ?u.2411689
γ₂ : Type ?u.2411692
δ : Type ?u.2411695
ι : Sort y
s t u : Set α
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
⊢ ∀ (s : Set ℝ), (∃ i i_1 h, s = Ioo ↑i ↑i_1) → ↑↑μ s = ↑↑ν s
α : Type ?u.2411683
β : Type ?u.2411686
γ : Type ?u.2411689
γ₂ : Type ?u.2411692
δ : Type ?u.2411695
ι : Sort y
s t u : Set α
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
⊢ ∀ (s : Set ℝ), (s ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → ↑↑μ s = ↑↑ν s
simp only [mem_iUnion, mem_singleton_iff]
case intro.intro.intro
α : Type ?u.2411683
β : Type ?u.2411686
γ : Type ?u.2411689
γ₂ : Type ?u.2411692
δ : Type ?u.2411695
ι : Sort y
s t u : Set α
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
a b : ℚ
⊢ ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
α : Type ?u.2411683
β : Type ?u.2411686
γ : Type ?u.2411689
γ₂ : Type ?u.2411692
δ : Type ?u.2411695
ι : Sort y
s t u : Set α
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
⊢ ∀ (s : Set ℝ), (∃ i i_1 h, s = Ioo ↑i ↑i_1) → ↑↑μ s = ↑↑ν s
rintro _ ⟨a, b, -, rfl⟩
no goals
case intro.intro.intro
α : Type ?u.2411683
β : Type ?u.2411686
γ : Type ?u.2411689
γ₂ : Type ?u.2411692
δ : Type ?u.2411695
ι : Sort y
s t u : Set α
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
a b : ℚ
⊢ ↑↑μ (Ioo ↑a ↑b) = ↑↑ν (Ioo ↑a ↑b)
apply h