awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
have obtain : ∀ (n : ℕ) (h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
  ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
have this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
Tactic: have : ∀ᶠ y in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y :=
    nhdsWithin_le_nhds h.eventually_continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
have h₁ : ∀ (y : 𝕜) (hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y)
  (h'y : Membership.mem (γ := Set 𝕜) {x}ᶜ y), ContinuousAt f y
Tactic: filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ ContinuousAt f y
have h'y₁ : ¬y = x
Tactic: simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at h'y
Cleared hypotheses: h'y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
⊢ ContinuousAt f y
have this₁ : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
Tactic: have : ContinuousAt (fun z ↦ ((z - x) ^ n)⁻¹) y :=
    ContinuousAt.inv₀ (by fun_prop) (by simp [sub_eq_zero, h'y])
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this_1 : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
⊢ ContinuousAt f y
have h₁ : (fun (x_1 : 𝕜) ↦ ((x_1 - x) ^ n)⁻¹ • (x_1 - x) ^ n • f x_1) =ᶠ[𝓝 y] f
Tactic: apply (this.smul hy).congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this_1 : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
⊢ (fun (x_1 : 𝕜) ↦ ((x_1 - x) ^ n)⁻¹ • (x_1 - x) ^ n • f x_1) =ᶠ[𝓝 y] f
have h₁ : ∀ (z : 𝕜) (hz : z ≠ x), ((z - x) ^ n)⁻¹ • (z - x) ^ n • f z = f z
Tactic: filter_upwards [eventually_ne_nhds h'y] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
have obtain : ∀ (n : ℕ) (h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
  ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
have h₁ : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
Tactic: apply AnalyticAt.eventually_analyticAt at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
have refine_1 : 𝓝[≠] x ≤ 𝓝 x
Tactic: refine (h.filter_mono ?_).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
refine_1 : 𝓝[≠] x ≤ 𝓝 x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
have refine_2 : ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Tactic: refine (h.filter_mono ?_).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
    AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
have refine_2 : ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
  Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
    AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Tactic: rw [eventually_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
have refine_2 : ∀ (x_1 : 𝕜),
  Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
    AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Tactic: apply Filter.Eventually.of_forall
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y
have hy₁ : ¬y = x
Tactic: rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy
Cleared hypotheses: hy, hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y
have this : AnalyticAt 𝕜 ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹ y
Tactic: have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
      (pow_ne_zero _ (sub_ne_zero_of_ne hy))
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹ y
⊢ AnalyticAt 𝕜 f y
have refine_2 : ∀ (x_1 : 𝕜),
  x_1 ≠ x →
    HSMul.hSMul (β := 𝕜 → E) ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_2 : 𝕜) ↦ x) ^ n)⁻¹
        (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 =
      f x_1
Tactic: apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have refine_1 : MeromorphicAt f x →
  ∀ (n : ℕ) (hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
    ∀ᶠ (x_2 : 𝕜) in 𝓝 x,
      Membership.mem (γ := Set 𝕜) {x}ᶜ x_2 → f x_2 = HPow.hPow (β := ℤ) (x_2 - x) (-(↑n : ℤ)) • (x_2 - x) ^ n • f x_2
Tactic: refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
refine_1 :
  MeromorphicAt f x →
    ∀ (n : ℕ) (hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
      ∀ᶠ (x_2 : 𝕜) in 𝓝 x,
        Membership.mem (γ := Set 𝕜) {x}ᶜ x_2 → f x_2 = HPow.hPow (β := ℤ) (x_2 - x) (-(↑n : ℤ)) • (x_2 - x) ^ n • f x_2
⊢ MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have refine_2 : (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x
Tactic: refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
n : ℕ
hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = HPow.hPow (β := ℤ) (x_1 - x) (-(↑n : ℤ)) • (x_1 - x) ^ n • f x_1
have refine_1 : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), f z = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) • (z - x) ^ n • f z
Tactic: filter_upwards with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
n : ℕ
hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ f z = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) • (z - x) ^ n • f z
have match_scalars : 1 = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) * ((z - x) ^ n * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x
have refine_2 : (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) →
  ∀ (n : ℤ) (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g x) (hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    MeromorphicAt.{u_1, u_3} (E := E) (fun (x_2 : 𝕜) ↦ (x_2 - x) ^ n • g x_2) x
Tactic: refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv f) x
have h₁ : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x
have obtain : ∀ (n : ℤ) (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
  MeromorphicAt (deriv f) x
Tactic: obtain ⟨n, g, h₁g, h₂g⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
have h : ∀ (z₀ : 𝕜) (h₁ : AnalyticAt 𝕜 g z₀) (h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀),
  deriv (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z₀ = ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
Tactic: filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
⊢ DifferentiableAt 𝕜 g z₀
have funProp : IsBoundedLinearMap.{u_1, u_1, u_3} 𝕜 (F := E) fun (a : 𝕜) ↦ g a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
⊢ deriv (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z₀ = ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
have h : HSMul.hSMul (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x ^ n) (z₀ - x)) (g z₀) + (z₀ - x) ^ n • deriv g z₀ =
  ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
Tactic: rw [deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x
have this : EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
  ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
Tactic: have : _root_.deriv (fun z ↦ (z - x) ^ n • g z)
      =ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • _root_.deriv g z := by
    filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
    rw [deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this :
  EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
⊢ MeromorphicAt (deriv f) x
have rw : MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z) x
Tactic: rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
    MeromorphicAt.meromorphicAt_congr this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[n] f) x
have zero : MeromorphicAt (deriv^[0] f) x
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
zero : MeromorphicAt (deriv^[0] f) x
⊢ MeromorphicAt (deriv^[n] f) x
have succ : ∀ (n : ℕ) (IH : MeromorphicAt (deriv^[n] f) x), MeromorphicAt (deriv^[n + 1] f) x
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ MeromorphicAt (g • f) x ↔ MeromorphicAt f x
have refine : ∀ (hfg : MeromorphicAt (g • f) x), MeromorphicAt f x
Tactic: refine ⟨fun hfg ↦ ?_, hg.meromorphicAt.smul⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
⊢ MeromorphicAt f x
have refine : g⁻¹ • g • f =ᶠ[𝓝[≠] x] f
Tactic: refine (hg.inv hg').meromorphicAt.smul hfg |>.congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
⊢ g⁻¹ • g • f =ᶠ[𝓝[≠] x] f
have h : ∀ (z : 𝕜) (hz : g z ≠ 0), (g⁻¹ • g • f) z = f z
Tactic: filter_upwards [(hg.continuousAt.mono_left nhdsWithin_le_nhds).eventually_ne hg'] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
⊢ MeromorphicAt (f ∘ g) x
have obtain : ∀ (r : ℕ) (hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)),
  MeromorphicAt (f ∘ g) x
Tactic: obtain ⟨r, hr⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
⊢ MeromorphicAt (f ∘ g) x
have pos : ∀ (hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤), MeromorphicAt (f ∘ g) x
Tactic: by_cases hg' : analyticOrderAt (g · - g x) x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
pos : ∀ (hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤), MeromorphicAt (f ∘ g) x
⊢ MeromorphicAt (f ∘ g) x
have neg : ∀ (hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤), MeromorphicAt (f ∘ g) x
Tactic: by_cases hg' : analyticOrderAt (g · - g x) x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x
have pos : (fun (x_1 : 𝕜) ↦ f (g x)) =ᶠ[𝓝[≠] x] f ∘ g
Tactic: refine .congr (.const (f (g x)) x) ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
⊢ (fun (x_1 : 𝕜) ↦ f (g x)) =ᶠ[𝓝[≠] x] f ∘ g
have h : ∀ (z : 𝕜) (hz : g z - g x = 0), f (g x) = (f ∘ g) z
Tactic: filter_upwards [nhdsWithin_le_nhds <| analyticOrderAt_eq_top.mp hg'] with z hz