diff --git a/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean b/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean
index fe918492197a54..b5e56842f647f8 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean
@@ -367,7 +367,7 @@ theorem exists_upperSemicontinuous_le_lintegral_le (f : α → ℝ≥0) (int_f :
     ∃ fs : α →ₛ ℝ≥0, (∀ x, fs x ≤ f x) ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := by
     have := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
     conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
-    erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => by simp⟩]
+    rw [ENNReal.biSup_add'] at this <;> [skip; exact ⟨0, fun x => by simp⟩]
     simp only [lt_iSup_iff] at this
     rcases this with ⟨fs, fs_le_f, int_fs⟩
     refine ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, ?_⟩