chore(Analysis/Meromorphic/Basic): use variable more (#31214)

Declare frequently used objects as `variable`, to avoid repetitive declarations.

Author: kebekus

Mathlib/Analysis/Meromorphic/Basic.lean

@@ -52,15 +52,19 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero {f : 𝕜 → E}
 
 namespace MeromorphicAt
 
+variable {ι : Type*} {s : Finset ι} {F : ι → 𝕜 → 𝕜} {G : ι → 𝕜 → E}
+
 @[fun_prop]
 lemma id (x : 𝕜) : MeromorphicAt id x := analyticAt_id.meromorphicAt
 
 @[fun_prop, simp]
 lemma const (e : E) (x : 𝕜) : MeromorphicAt (fun _ ↦ e) x :=
   analyticAt_const.meromorphicAt
 
+variable {x : 𝕜}
+
 @[fun_prop]
-lemma add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma add {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f + g) x := by
   rcases hf with ⟨m, hf⟩
   rcases hg with ⟨n, hg⟩
@@ -74,14 +78,14 @@ lemma add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : Meromorph
     (((analyticAt_id.sub analyticAt_const).pow _).smul hg)
 
 @[fun_prop]
-lemma fun_add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma fun_add {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (fun z ↦ f z + g z) x :=
   hf.add hg
 
 @[deprecated (since := "2025-05-09")] alias add' := fun_add
 
 @[fun_prop]
-lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f • g) x := by
   rcases hf with ⟨m, hf⟩
   rcases hg with ⟨n, hg⟩
@@ -91,29 +95,28 @@ lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f
   module
 
 @[fun_prop]
-lemma fun_smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma fun_smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (fun z ↦ f z • g z) x :=
   hf.smul hg
 
 @[deprecated (since := "2025-05-09")] alias smul' := fun_smul
 
 @[fun_prop]
-lemma mul {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma mul {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f * g) x :=
   hf.smul hg
 
 @[fun_prop]
-lemma fun_mul {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma fun_mul {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (fun z ↦ f z * g z) x :=
   hf.smul hg
 
 @[deprecated (since := "2025-05-09")] alias mul' := fun_mul
 
 /-- Finite products of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜}
-    (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (∏ n ∈ s, f n) x := by
+theorem prod (h : ∀ σ, MeromorphicAt (F σ) x) :
+    MeromorphicAt (∏ n ∈ s, F n) x := by
   classical
   induction s using Finset.induction with
   | empty =>
@@ -125,16 +128,15 @@ theorem prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜}
 
 /-- Finite products of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem fun_prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜}
-    (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (fun z ↦ ∏ n ∈ s, f n z) x := by
+theorem fun_prod (h : ∀ σ, MeromorphicAt (F σ) x) :
+    MeromorphicAt (fun z ↦ ∏ n ∈ s, F n z) x := by
   convert prod h (s := s)
   simp
 
 /-- Finite sums of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem sum {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → E} {x : 𝕜} (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (∑ n ∈ s, f n) x := by
+theorem sum (h : ∀ σ, MeromorphicAt (G σ) x) :
+    MeromorphicAt (∑ n ∈ s, G n) x := by
   classical
   induction s using Finset.induction with
   | empty =>
@@ -146,46 +148,45 @@ theorem sum {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → E} {x : 𝕜} (h :
 
 /-- Finite sums of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem fun_sum {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → E} {x : 𝕜}
-    (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (fun z ↦ ∑ n ∈ s, f n z) x := by
+theorem fun_sum (h : ∀ σ, MeromorphicAt (G σ) x) :
+    MeromorphicAt (fun z ↦ ∑ n ∈ s, G n z) x := by
   convert sum h (s := s)
   simp
 
 @[fun_prop]
-lemma neg {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (-f) x := by
+lemma neg {f : 𝕜 → E} (hf : MeromorphicAt f x) : MeromorphicAt (-f) x := by
   convert (MeromorphicAt.const (-1 : 𝕜) x).smul hf using 1
   ext1 z
   simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul]
 
 @[fun_prop]
-lemma fun_neg {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (fun z ↦ -f z) x :=
+lemma fun_neg {f : 𝕜 → E} (hf : MeromorphicAt f x) : MeromorphicAt (fun z ↦ -f z) x :=
   hf.neg
 
 @[deprecated (since := "2025-05-09")] alias neg' := fun_neg
 
 @[simp]
-lemma neg_iff {f : 𝕜 → E} {x : 𝕜} :
+lemma neg_iff {f : 𝕜 → E} :
     MeromorphicAt (-f) x ↔ MeromorphicAt f x :=
   ⟨fun h ↦ by simpa only [neg_neg] using h.neg, MeromorphicAt.neg⟩
 
 @[fun_prop]
-lemma sub {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma sub {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f - g) x := by
   convert hf.add hg.neg using 1
   ext1 z
   simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]
 
 @[fun_prop]
-lemma fun_sub {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma fun_sub {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (fun z ↦ f z - g z) x :=
   hf.sub hg
 
 @[deprecated (since := "2025-05-09")] alias sub' := fun_sub
 
 /-- With our definitions, `MeromorphicAt f x` depends only on the values of `f` on a punctured
 neighbourhood of `x` (not on `f x`) -/
-lemma congr {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hfg : f =ᶠ[𝓝[≠] x] g) :
+lemma congr {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hfg : f =ᶠ[𝓝[≠] x] g) :
     MeromorphicAt g x := by
   rcases hf with ⟨m, hf⟩
   refine ⟨m + 1, ?_⟩
@@ -200,7 +201,7 @@ lemma congr {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hfg : f =ᶠ
 /--
 If two functions agree on a punctured neighborhood, then one is meromorphic iff the other is so.
 -/
-lemma meromorphicAt_congr {f g : 𝕜 → E} {x : 𝕜} (h : f =ᶠ[𝓝[≠] x] g) :
+lemma meromorphicAt_congr {f g : 𝕜 → E} (h : f =ᶠ[𝓝[≠] x] g) :
     MeromorphicAt f x ↔ MeromorphicAt g x :=
   ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
 
@@ -215,7 +216,7 @@ lemma update [DecidableEq 𝕜] {f : 𝕜 → E} {z} (hf : MeromorphicAt f z) (w
   update_iff.mpr hf
 
 @[fun_prop]
-lemma inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x := by
+lemma inv {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x := by
   rcases hf with ⟨m, hf⟩
   by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
   · -- silly case: f locally 0 near x
@@ -241,56 +242,56 @@ lemma inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicA
       simp [field, pow_succ', mul_assoc, hfg]
 
 @[fun_prop]
-lemma fun_inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (fun z ↦ (f z)⁻¹) x :=
+lemma fun_inv {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (fun z ↦ (f z)⁻¹) x :=
   hf.inv
 
 @[deprecated (since := "2025-05-09")] alias inv' := fun_inv
 
 @[simp]
-lemma inv_iff {f : 𝕜 → 𝕜} {x : 𝕜} :
+lemma inv_iff {f : 𝕜 → 𝕜} :
     MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x :=
   ⟨fun h ↦ by simpa only [inv_inv] using h.inv, MeromorphicAt.inv⟩
 
 @[fun_prop]
-lemma div {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma div {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f / g) x :=
   (div_eq_mul_inv f g).symm ▸ (hf.mul hg.inv)
 
 @[fun_prop]
-lemma fun_div {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
+lemma fun_div {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (fun z ↦ f z / g z) x :=
   hf.div hg
 
 @[deprecated (since := "2025-05-09")] alias div' := fun_div
 
 @[fun_prop]
-lemma pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (f ^ n) x := by
+lemma pow {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (f ^ n) x := by
   induction n with
   | zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
   | succ m hm => simpa only [pow_succ] using hm.mul hf
 
 @[fun_prop]
-lemma fun_pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) :
+lemma fun_pow {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℕ) :
     MeromorphicAt (fun z ↦ (f z) ^ n) x :=
   hf.pow n
 
 @[deprecated (since := "2025-05-09")] alias pow' := fun_pow
 
 @[fun_prop]
-lemma zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (f ^ n) x := by
+lemma zpow {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (f ^ n) x := by
   cases n with
   | ofNat m => simpa only [Int.ofNat_eq_coe, zpow_natCast] using hf.pow m
   | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)
 
 @[fun_prop]
-lemma fun_zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) :
+lemma fun_zpow {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℤ) :
     MeromorphicAt (fun z ↦ (f z) ^ n) x :=
   hf.zpow n
 
 @[deprecated (since := "2025-05-09")] alias zpow' := fun_zpow
 
 /-- If a function is meromorphic at a point, then it is continuous at nearby points. -/
-theorem eventually_continuousAt {f : 𝕜 → E} {x : 𝕜}
+theorem eventually_continuousAt {f : 𝕜 → E}
     (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, ContinuousAt f y := by
   obtain ⟨n, h⟩ := h
   have : ∀ᶠ y in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y :=
@@ -306,7 +307,7 @@ theorem eventually_continuousAt {f : 𝕜 → E} {x : 𝕜}
 /-- In a complete space, a function which is meromorphic at a point is analytic at all nearby
 points. The completeness assumption can be dispensed with if one assumes that `f` is meromorphic
 on a set around `x`, see `MeromorphicOn.eventually_analyticAt`. -/
-theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
+theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E}
     (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y := by
   obtain ⟨n, h⟩ := h
   apply AnalyticAt.eventually_analyticAt at h
@@ -322,7 +323,7 @@ theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
     intro z hz
     simp [smul_smul, hz, sub_eq_zero]
 
-lemma iff_eventuallyEq_zpow_smul_analyticAt {f : 𝕜 → E} {x : 𝕜} : MeromorphicAt f x ↔
+lemma iff_eventuallyEq_zpow_smul_analyticAt {f : 𝕜 → E} : MeromorphicAt f x ↔
     ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by
   refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
   · filter_upwards with z hz