case mp
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w → ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i

case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → v = w
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
constructor
case mp
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑v i✝ = ↑v i✝
case mp
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w → ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
rintro rfl _ _
no goals
case mp
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑v i✝ = ↑v i✝
rfl
case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → ∀ (i : Set α), ↑v i = ↑w i
case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → v = w
rw [ext_iff']
case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
⊢ ↑v i = ↑w i
case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → ∀ (i : Set α), ↑v i = ↑w i
intro h i
case pos
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : MeasurableSet i
⊢ ↑v i = ↑w i

case neg
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i = ↑w i
case mpr
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
⊢ ↑v i = ↑w i
by_cases hi : MeasurableSet i
no goals
case pos
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : MeasurableSet i
⊢ ↑v i = ↑w i
exact h i hi
no goals
case neg
α : Type u_1
β : Type ?u.8146
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i = ↑w i
simp_rw [not_measurable _ hi]