α : Type ?u.156969
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0
α : Type ?u.156969
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (fun t => m (t ∩ s)) ∅ = 0
simp
no goals
α : Type ?u.156969
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0
simp [m_empty]
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(LinearMap.comp (map Subtype.val) (comap Subtype.val)) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(restrict s) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
rw [restrict]
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(map Subtype.val) (↑(comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(LinearMap.comp (map Subtype.val) (comap Subtype.val)) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
simp only [LinearMap.comp_apply]
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(map Subtype.val)
      (OuterMeasure.ofFunction (fun s_1 => m (Subtype.val '' s_1)) (_ : (fun s_1 => m (Subtype.val '' s_1)) ∅ = 0)) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(map Subtype.val) (↑(comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
rw [comap_ofFunction _ (Or.inl hm)]
no goals
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ ↑(map Subtype.val)
      (OuterMeasure.ofFunction (fun s_1 => m (Subtype.val '' s_1)) (_ : (fun s_1 => m (Subtype.val '' s_1)) ∅ = 0)) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) (_ : (fun t => m (t ∩ s)) ∅ = 0)
simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]