feat(Asymptotics/Theta): add 3 trivial lemmas (#8258)

Add `Filter.EventuallyEq.isTheta`,
`Asymptotics.IsTheta.isTheta_congr_left`,
and `Asymptotics.IsTheta.isTheta_congr_right`.

Mathlib/Analysis/Asymptotics/Theta.lean

@@ -147,6 +147,9 @@ theorem _root_.Filter.EventuallyEq.trans_isTheta {f₁ f₂ : α → E} {g : α
 instance : Trans (α := α → E) (β := α → E) (γ := α → F) (EventuallyEq l) (IsTheta l) (IsTheta l) :=
   ⟨EventuallyEq.trans_isTheta⟩
 
+lemma _root_.Filter.EventuallyEq.isTheta {f g : α → E} (h : f =ᶠ[l] g) : f =Θ[l] g :=
+  h.trans_isTheta isTheta_rfl
+
 @[simp]
 theorem isTheta_norm_left : (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g := by simp [IsTheta]
 #align asymptotics.is_Theta_norm_left Asymptotics.isTheta_norm_left
@@ -188,6 +191,12 @@ theorem IsTheta.isBigO_congr_right (h : g' =Θ[l] k') : f =O[l] g' ↔ f =O[l] k
   ⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩
 #align asymptotics.is_Theta.is_O_congr_right Asymptotics.IsTheta.isBigO_congr_right
 
+lemma IsTheta.isTheta_congr_left (h : f' =Θ[l] g') : f' =Θ[l] k ↔ g' =Θ[l] k :=
+  h.isBigO_congr_left.and h.isBigO_congr_right
+
+lemma IsTheta.isTheta_congr_right (h : f' =Θ[l] g') : k =Θ[l] f' ↔ k =Θ[l] g' :=
+  h.isBigO_congr_right.and h.isBigO_congr_left
+
 theorem IsTheta.mono (h : f =Θ[l] g) (hl : l' ≤ l) : f =Θ[l'] g :=
   ⟨h.1.mono hl, h.2.mono hl⟩
 #align asymptotics.is_Theta.mono Asymptotics.IsTheta.mono