Fix one warning

Author: grunweg

Carleson/TwoSidedCarleson/RestrictedWeakType.lean

@@ -100,10 +100,7 @@ lemma interpolation_param_interpolation {t₀ t₁ t : ℝ} (h : t₀ ≠ t₁)
     t = (1 - interpolation_param t₀ t₁ t) * t₀ + interpolation_param t₀ t₁ t * t₁ := by
   have : t₁ - t₀ ≠ 0 := sub_ne_zero_of_ne (id (Ne.symm h))
   unfold interpolation_param
-  rw [← div_self this, div_sub_div_same]
-  symm
-  rw [div_mul_eq_mul_div, div_mul_eq_mul_div, div_add_div_same, div_eq_iff this]
-  ring
+  field_simp; ring
 
 --TODO: move
 lemma interpolation_param_mem_Ioo {t₀ t₁ t : ℝ} (h : t ∈ Ioo t₀ t₁) :