case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (b : β), f b) ≤ restrict w (⋃ (b : β), f b)
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
⊢ restrict v (⋃ (b : β), f b) ≤ restrict w (⋃ (b : β), f b)
cases nonempty_encodable β
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) ≤
    restrict w (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (b : β), f b) ≤ restrict w (⋃ (b : β), f b)
rw [← Encodable.iUnion_decode₂]
case intro.refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ), MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)

case intro.refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ),
    restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
      restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) ≤
    restrict w (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)
refine' restrict_le_restrict_iUnion v w _ _
case intro.refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
case intro.refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ), MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
intro n
no goals
case intro.refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
measurability
case intro.refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
    restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
case intro.refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ),
    restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
      restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
intro n
case intro.refine'_2.none
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ none), f b) ≤ restrict w (⋃ (b : β) (_ : b ∈ none), f b)

case intro.refine'_2.some
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
b : β
⊢ restrict v (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1) ≤ restrict w (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1)
case intro.refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
    restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
cases' Encodable.decode₂ β n with b
no goals
case intro.refine'_2.none
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ none), f b) ≤ restrict w (⋃ (b : β) (_ : b ∈ none), f b)
simp
no goals
case intro.refine'_2.some
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
b : β
⊢ restrict v (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1) ≤ restrict w (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1)
simp [hf₂ b]