case h
α : Type u_1
β : Type ?u.317389
γ : Type ?u.317392
δ : Type ?u.317395
ι : Type ?u.317398
R : Type ?u.317401
R' : Type ?u.317404
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : Set.Nonempty m
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict (sInf m) t) s = ↑↑(sInf ((fun μ => restrict μ t) '' m)) s
α : Type u_1
β : Type ?u.317389
γ : Type ?u.317392
δ : Type ?u.317395
ι : Type ?u.317398
R : Type ?u.317401
R' : Type ?u.317404
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : Set.Nonempty m
ht : MeasurableSet t
⊢ restrict (sInf m) t = sInf ((fun μ => restrict μ t) '' m)
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.317389
γ : Type ?u.317392
δ : Type ?u.317395
ι : Type ?u.317398
R : Type ?u.317401
R' : Type ?u.317404
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : Set.Nonempty m
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict (sInf m) t) s = ↑↑(sInf ((fun μ => restrict μ t) '' m)) s
simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
  Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
  Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
  OuterMeasure.restrict_apply]