awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0
have inl : ∀ᶠ (b : 𝕜) in map g (𝓝[≠] x), f b = 0
Tactic: rw [Function.comp_def, ← eventually_map (P := (f · = 0))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
Tactic: have hr := (WithTop.coe_untop₀_of_ne_top hf').symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have hf'₁ : ∃ (g_1 : 𝕜 → E),
  AnalyticAt 𝕜 g_1 (g x) ∧
    g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z
Tactic: rw [meromorphicOrderAt_ne_top_iff hf] at hf'
Cleared hypotheses: hf', hr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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₀
hf' : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inr : meromorphicOrderAt (f ∘ g) x =
  (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
Tactic: rw [hr]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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₀
hf' : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inr : ∀ (F : 𝕜 → E) (hFan : AnalyticAt 𝕜 F (g x)) (hFne : F (g x) ≠ 0)
  (hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z),
  meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
Tactic: obtain ⟨F, hFan, hFne, hFev⟩ := hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
Tactic: have aux1 : f ∘ g =ᶠ[𝓝[≠] x] (g · - g x) ^ r • (F ∘ g) := hFev.comp_tendsto (hg.map_nhdsNE hg_nc)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ meromorphicOrderAt (F ∘ g) x = 0
have rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
⊢ meromorphicOrderAt (F ∘ g) x = 0
have rw₁ : Eq (α := WithTop ℤ) (ENat.map Nat.cast 0) 0
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
rw₁ : Eq (α := WithTop ℤ) (ENat.map Nat.cast 0) 0
⊢ meromorphicOrderAt (F ∘ g) x = 0
have rw₂ : Eq (α := WithTop ℤ) (↑(↑0 : ℤ) : WithTop ℤ) 0
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
rw₁ : Eq (α := WithTop ℤ) (ENat.map Nat.cast 0) 0
rw₂ : Eq (α := WithTop ℤ) (↑(↑0 : ℤ) : WithTop ℤ) 0
⊢ meromorphicOrderAt (F ∘ g) x = 0
have rw₃ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
rw₁ : Eq (α := WithTop ℤ) (ENat.map Nat.cast 0) 0
rw₂ : Eq (α := WithTop ℤ) (↑(↑0 : ℤ) : WithTop ℤ) 0
rw₃ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
⊢ meromorphicOrderAt (F ∘ g) x = 0
have rw₄ : Eq (α := WithTop ℤ) 0 0
Tactic: rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have aux2 : meromorphicOrderAt (F ∘ g) x = 0
Tactic: have aux2 : meromorphicOrderAt (F ∘ g) x = 0 := by
    rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inr : AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
Tactic: rw [meromorphicOrderAt_congr aux1, meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),
    aux2, add_zero, meromorphicOrderAt_zpow, AnalyticAt.meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
inr : AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inr₁ : MeromorphicAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
Tactic: rw [meromorphicOrderAt_congr aux1, meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),
    aux2, add_zero, meromorphicOrderAt_zpow, AnalyticAt.meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
inr : AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
inr₁ : MeromorphicAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have rw : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r) x
Tactic: rw [meromorphicOrderAt_congr aux1, meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),
    aux2, add_zero, meromorphicOrderAt_zpow, AnalyticAt.meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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 : WithTop ℤ)
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
inr : AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
inr₁ : MeromorphicAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
rw : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r) x
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have rw₁ : AnalyticAt 𝕜 (F ∘ g) x
Tactic: rw [meromorphicOrderAt_congr aux1, meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),
    aux2, add_zero, meromorphicOrderAt_zpow, AnalyticAt.meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have pos : ∀ (hf : MeromorphicAt f (g x)), meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
Tactic: by_cases hf : MeromorphicAt f (g x)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
pos : ∀ (hf : MeromorphicAt f (g x)), meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have neg : ∀ (hf : ¬MeromorphicAt f (g x)), meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
Tactic: by_cases hf : MeromorphicAt f (g x)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
Tactic: have hgo : analyticOrderAt _ x = 1 := hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have pos : meromorphicOrderAt f (g x) * ENat.map Nat.cast 1 = meromorphicOrderAt f (g x)
Tactic: rw [hf.meromorphicOrderAt_comp hg, hgo]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
pos : meromorphicOrderAt f (g x) * ENat.map Nat.cast 1 = meromorphicOrderAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have pos₁ : ¬EventuallyConst g (𝓝 x)
Tactic: rw [hf.meromorphicOrderAt_comp hg, hgo]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
have neg : ¬MeromorphicAt (f ∘ g) x
Tactic: rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
have pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
Tactic: by_cases hf : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
have neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
Tactic: by_cases hf : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
have neg : ¬MeromorphicAt (g • f) x
Tactic: rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
⊢ E
have pos : (h₁ : MeromorphicAt f x) → E
Tactic: by_cases h₁ : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
pos : (h₁ : MeromorphicAt f x) → E
⊢ E
have neg : (h₁ : ¬MeromorphicAt f x) → E
Tactic: by_cases h₁ : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
⊢ E
have pos : (h₂ : meromorphicOrderAt f x = ⊤) → E
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
pos : (h₂ : meromorphicOrderAt f x = ⊤) → E
⊢ E
have neg : (h₂ : ¬meromorphicOrderAt f x = ⊤) → E
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ MeromorphicAt f x
have rw : MeromorphicAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x
Tactic: rw [MeromorphicAt.meromorphicAt_congr h]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicTrailingCoeffAt f x = g x
have h₁f : MeromorphicAt f x
Tactic: have h₁f : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x = g x
have pos : ∀ (h₃ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f x = g x
Tactic: by_cases h₃ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
pos : ∀ (h₃ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f x = g x
⊢ meromorphicTrailingCoeffAt f x = g x
have neg : ∀ (h₃ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f x = g x
Tactic: by_cases h₃ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f x = g x
have pos : ∀ (h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ g z), 0 = g x
Tactic: simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
      MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₁f : MeromorphicAt f x
h₃ : meromorphicOrderAt f x = ⊤
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ g z
⊢ 0 = g x
have pos : 0 =ᶠ[𝓝 x] g
Tactic: apply EventuallyEq.eq_of_nhds (f := 0)