α : Type u_1
β : Type ?u.10223
γ : Type ?u.10226
δ : Type ?u.10229
ι : Type ?u.10232
inst✝ : MeasurableSpace α
μ μ₁ : Measure α
s✝ s₁ s₂ t s : Set α
_hs : MeasurableSet s
⊢ ↑↑μ₁ s = ↑↑μ₁ s
α : Type u_1
β : Type ?u.10223
γ : Type ?u.10226
δ : Type ?u.10229
ι : Type ?u.10232
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ μ₁ = μ₂ → ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s
rintro rfl s _hs
no goals
α : Type u_1
β : Type ?u.10223
γ : Type ?u.10226
δ : Type ?u.10229
ι : Type ?u.10232
inst✝ : MeasurableSpace α
μ μ₁ : Measure α
s✝ s₁ s₂ t s : Set α
_hs : MeasurableSet s
⊢ ↑↑μ₁ s = ↑↑μ₁ s
rfl