Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ meromorphicOrderAt ((fun x_1 ↦ g x_1 - g x) ^ r) x =
    ↑r * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt ((fun x_1 ↦ g x_1 - g x) ^ r) x

pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ AnalyticAt 𝕜 (F ∘ g) x

Tactic:
meromorphicOrderAt_zpow,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ ↑r * meromorphicOrderAt (fun x_1 ↦ g x_1 - g x) x = ↑r * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

case inr.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt (fun x_1 ↦ g x_1 - g x) x

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt ((fun x_1 ↦ g x_1 - g x) ^ r) x

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = ↑r
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ AnalyticAt 𝕜 (F ∘ g) x