-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem ext_iff (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, MeasurableSet i → v i = w i

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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

Tactic:
exact h i hi

Result:
no goals

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → v = w

Tactic:
rw [ext_iff']

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → ∀ (i : Set α), ↑v i = ↑w i

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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
m : MeasurableSpace α
M : Type u_3
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

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i

Tactic:
constructor

Result:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → v = w

Proof state:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w → ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i

Tactic:
rintro rfl _ _

Result:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑v i✝ = ↑v i✝

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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

Tactic:
simp_rw [not_measurable _ hi]

Result:
no goals

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → ∀ (i : Set α), ↑v i = ↑w i

Tactic:
intro h i

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
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

Proof state:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑v i✝ = ↑v i✝

Tactic:
rfl

Result:
no goals