-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq_1 :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      (z - x) ^ m • g z
z : 𝕜
hg_eq :
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    (z - x) ^ m • g z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
h₁ :
  HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      f z =
    HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z
rwa : ℤ
h₂ :
  HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      f z =
    (HPow.hPow (β := ℤ) (z - x)
          (↑(Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
            ℤ) *
        (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ)) •
      g z
rwa₁ : ℤ
h₃ :
  HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      f z =
    (z - x) ^
        ((↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
                hf) :
            ℤ) +
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ)) •
      g z
h₄ : ℤ
h₅ :
  HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      f z =
    (z - x) ^
        (HAdd.hAdd (α := ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ)
            (↑m : ℤ) -
          (↑(Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
            ℤ)) •
      g z
h₆ : ℤ
h₇ :
  HPow.hPow (β := ℤ) (z - x)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf) :
          ℤ) •
      f z =
    HPow.hPow (β := ℤ) (z - x) (↑m : ℤ) • g z
h₈ :
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    HPow.hPow (β := ℤ) (z - x) (↑m : ℤ) • g z
h₉ h₁₀ h₁₁ h₁₂ :
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    (z - x) ^ m • g z
⊢ f z =
    (z - x) ^
        HSub.hSub (α := ℤ) (↑m : ℤ)
          (↑(Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
            ℤ) •
      g z

Tactic:
rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul,
        ← zpow_add₀ (sub_ne_zero.mpr hz), ← add_sub_assoc, add_sub_cancel_left, zpow_natCast,
        zpow_natCast]

Premises used: zpow_natCast, Iff.mpr, add_sub_assoc, add_sub_cancel_left, sub_ne_zero, zpow_add₀, zpow_ne_zero, SemigroupAction.mul_smul, smul_right_inj