diff --git a/BirkhoffErgodicThm/FilterPR.lean b/BirkhoffErgodicThm/FilterPR.lean
index 0b6170c..12fd4a0 100644
--- a/BirkhoffErgodicThm/FilterPR.lean
+++ b/BirkhoffErgodicThm/FilterPR.lean
@@ -1,13 +1,11 @@
 import Mathlib.Tactic
 
-/-- If two functions `f₁` and `f₂` are eventually equal with respect to a filter `f`,
-then adding to right the same function `f₃` to both `f₁` and `f₂` results in two functions that
-are also eventually equal with respect to the same filter `f`. -/
-lemma Filter.EventuallyEq.add_right {f : Filter α} {f₁ f₂ f₃ : α → ℝ} (h : f₁ =ᶠ[f] f₂) :
-    f₁ + f₃ =ᶠ[f] f₂ + f₃ := h.mono fun x hx ↦ by simp [hx]
-
-/-- If two functions `f₁` and `f₂` are eventually equal with respect to a filter `f`,
-then adding to left the same function `f₃` to both `f₁` and `f₂` results in two functions that
-are also eventually equal with respect to the same filter `f`. -/
-lemma Filter.EventuallyEq.add_left {f : Filter α} {f₁ f₂ f₃ : α → ℝ} (h : f₁ =ᶠ[f] f₂) :
-    f₃ + f₁ =ᶠ[f] f₃ + f₂ := h.mono fun x hx ↦ by simp [hx]
+namespace Filter.EventuallyEq
+
+variable {f : Filter α} {f₁ f₂ f₃ : α → β} [Mul β]
+
+@[to_additive]
+lemma mul_right (h : f₁ =ᶠ[f] f₂) : f₁ * f₃ =ᶠ[f] f₂ * f₃ := mul h (by rfl)
+
+@[to_additive]
+lemma mul_left (h : f₁ =ᶠ[f] f₂) : f₃ * f₁ =ᶠ[f] f₃ * f₂ := mul (by rfl) h