α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
⊢ inducedOuterMeasure (fun s x => ↑m₁ s) (_ : MeasurableSet ∅) (_ : ↑m₁ ∅ = 0) =
    inducedOuterMeasure (fun s x => ↑m₂ s) (_ : MeasurableSet ∅) (_ : ↑m₂ ∅ = 0)
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
⊢ trim m₁ = trim m₂
unfold trim
case e_m
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
⊢ (fun s x => ↑m₁ s) = fun s x => ↑m₂ s
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
⊢ inducedOuterMeasure (fun s x => ↑m₁ s) (_ : MeasurableSet ∅) (_ : ↑m₁ ∅ = 0) =
    inducedOuterMeasure (fun s x => ↑m₂ s) (_ : MeasurableSet ∅) (_ : ↑m₂ ∅ = 0)
congr
case e_m.h.h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
s : Set α
hs : MeasurableSet s
⊢ ↑m₁ s = ↑m₂ s
case e_m
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
⊢ (fun s x => ↑m₁ s) = fun s x => ↑m₂ s
funext s hs
no goals
case e_m.h.h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s
s : Set α
hs : MeasurableSet s
⊢ ↑m₁ s = ↑m₂ s
exact H hs