-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_smul {v : VectorMeasure α M} {i : Set α} (c : R) :
    (c • v).restrict i = c • v.restrict i

Proof state:
case neg.h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
a✝ : MeasurableSet j
⊢ ↑0 j = ↑(c • 0) j

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = c • 0

Tactic:
ext j

Result:
case neg.h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
a✝ : MeasurableSet j
⊢ ↑0 j = ↑(c • 0) j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
⊢ (c • v).restrict i = c • v.restrict 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
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i

Tactic:
ext j hj

Result:
case pos.h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((c • v).restrict i) j = ↑(c • v.restrict i) j

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i

Tactic:
simp only [restrict_not_measurable _ hi]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = c • 0

Proof state:
case pos.h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((c • v).restrict i) j = ↑(c • v.restrict i) j

Tactic:
simp [restrict_apply _ hi hj]

Result:
no goals