-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_trim (hle : m ≤ n) {i : Set α} (hi : MeasurableSet[m] i) :
    @VectorMeasure.restrict α m M _ _ (v.trim hle) i = (v.restrict i).trim hle

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ (v.trim hle).restrict i = (v.restrict i).trim hle

Tactic:
ext j hj

Result:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((v.trim hle).restrict i) j = ↑((v.restrict i).trim hle) j

Proof state:
case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)

case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

Tactic:
all_goals measurability

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((v.trim hle).restrict i) j = ↑((v.restrict i).trim hle) j

Tactic:
rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]

Result:
case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)

case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

case h.hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

Proof state:
case h.hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

Tactic:
measurability

Result:
no goals