case mk
α : Type u_1
β : Type ?u.23243
R : Type ?u.23246
R' : Type ?u.23249
ms : Set (OuterMeasure α)
m μ₂ : OuterMeasure α
measureOf✝ : Set α → ℝ≥0∞
empty✝ : measureOf✝ ∅ = 0
mono✝ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝ s₁ ≤ measureOf✝ s₂
iUnion_nat✝ : ∀ (s : ℕ → Set α), measureOf✝ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝ (s i)
h :
  (fun μ s => ↑μ s) { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ } =
    (fun μ s => ↑μ s) μ₂
⊢ { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ } = μ₂
α : Type u_1
β : Type ?u.23243
R : Type ?u.23246
R' : Type ?u.23249
ms : Set (OuterMeasure α)
m μ₁ μ₂ : OuterMeasure α
h : (fun μ s => ↑μ s) μ₁ = (fun μ s => ↑μ s) μ₂
⊢ μ₁ = μ₂
cases μ₁
case mk.mk
α : Type u_1
β : Type ?u.23243
R : Type ?u.23246
R' : Type ?u.23249
ms : Set (OuterMeasure α)
m : OuterMeasure α
measureOf✝¹ : Set α → ℝ≥0∞
empty✝¹ : measureOf✝¹ ∅ = 0
mono✝¹ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝¹ s₁ ≤ measureOf✝¹ s₂
iUnion_nat✝¹ : ∀ (s : ℕ → Set α), measureOf✝¹ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝¹ (s i)
measureOf✝ : Set α → ℝ≥0∞
empty✝ : measureOf✝ ∅ = 0
mono✝ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝ s₁ ≤ measureOf✝ s₂
iUnion_nat✝ : ∀ (s : ℕ → Set α), measureOf✝ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝ (s i)
h :
  (fun μ s => ↑μ s) { measureOf := measureOf✝¹, empty := empty✝¹, mono := mono✝¹, iUnion_nat := iUnion_nat✝¹ } =
    (fun μ s => ↑μ s) { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ }
⊢ { measureOf := measureOf✝¹, empty := empty✝¹, mono := mono✝¹, iUnion_nat := iUnion_nat✝¹ } =
    { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ }
case mk
α : Type u_1
β : Type ?u.23243
R : Type ?u.23246
R' : Type ?u.23249
ms : Set (OuterMeasure α)
m μ₂ : OuterMeasure α
measureOf✝ : Set α → ℝ≥0∞
empty✝ : measureOf✝ ∅ = 0
mono✝ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝ s₁ ≤ measureOf✝ s₂
iUnion_nat✝ : ∀ (s : ℕ → Set α), measureOf✝ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝ (s i)
h :
  (fun μ s => ↑μ s) { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ } =
    (fun μ s => ↑μ s) μ₂
⊢ { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ } = μ₂
cases μ₂
no goals
case mk.mk
α : Type u_1
β : Type ?u.23243
R : Type ?u.23246
R' : Type ?u.23249
ms : Set (OuterMeasure α)
m : OuterMeasure α
measureOf✝¹ : Set α → ℝ≥0∞
empty✝¹ : measureOf✝¹ ∅ = 0
mono✝¹ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝¹ s₁ ≤ measureOf✝¹ s₂
iUnion_nat✝¹ : ∀ (s : ℕ → Set α), measureOf✝¹ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝¹ (s i)
measureOf✝ : Set α → ℝ≥0∞
empty✝ : measureOf✝ ∅ = 0
mono✝ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝ s₁ ≤ measureOf✝ s₂
iUnion_nat✝ : ∀ (s : ℕ → Set α), measureOf✝ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measureOf✝ (s i)
h :
  (fun μ s => ↑μ s) { measureOf := measureOf✝¹, empty := empty✝¹, mono := mono✝¹, iUnion_nat := iUnion_nat✝¹ } =
    (fun μ s => ↑μ s) { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ }
⊢ { measureOf := measureOf✝¹, empty := empty✝¹, mono := mono✝¹, iUnion_nat := iUnion_nat✝¹ } =
    { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ }
congr