-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem le_restrict_univ_iff_le : v ≤[Set.univ] w ↔ v ≤ w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[univ] w ↔ v ≤ w

Tactic:
constructor

Result:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[univ] w → v ≤ w

case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w → v ≤[univ] w

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w → v ≤[univ] w

Tactic:
intro h s hs

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑(v.restrict univ) s ≤ ↑(w.restrict univ) s

Proof state:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[univ] w → v ≤ w

Tactic:
intro h s hs

Result:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤[univ] w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s

Proof state:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤[univ] w
s : Set α
hs : MeasurableSet s
this : ↑(v.restrict univ) s ≤ ↑(w.restrict univ) s
⊢ ↑v s ≤ ↑w s

Tactic:
rwa [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ,
  restrict_apply _ MeasurableSet.univ hs, Set.inter_univ] at this

Result:
no goals

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s

Tactic:
exact h s hs

Result:
no goals

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑(v.restrict univ) s ≤ ↑(w.restrict univ) s

Tactic:
rw [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ,
  restrict_apply _ MeasurableSet.univ hs, Set.inter_univ]

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s

Proof state:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤[univ] w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s

Tactic:
have := h s hs

Result:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤[univ] w
s : Set α
hs : MeasurableSet s
this : ↑(v.restrict univ) s ≤ ↑(w.restrict univ) s
⊢ ↑v s ≤ ↑w s