no goals
α : Type u_1
β : Type ?u.9151
γ : Type ?u.9154
δ : Type ?u.9157
ι : Type ?u.9160
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
x✝¹ x✝ : Measure α
m₁ : OuterMeasure α
u₁ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑m₁ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑m₁ (f i)
h₁ : OuterMeasure.trim m₁ = m₁
m₂ : OuterMeasure α
_u₂ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑m₂ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑m₂ (f i)
_h₂ : OuterMeasure.trim m₂ = m₂
_h :
  ↑{ toOuterMeasure := m₁, m_iUnion := u₁, trimmed := h₁ } = ↑{ toOuterMeasure := m₂, m_iUnion := _u₂, trimmed := _h₂ }
⊢ { toOuterMeasure := m₁, m_iUnion := u₁, trimmed := h₁ } = { toOuterMeasure := m₂, m_iUnion := _u₂, trimmed := _h₂ }
congr