awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
h₁ :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      HPow.hPow (β := ℤ) (z - x) 0 •
        Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ z
⊢ g =ᶠ[𝓝[≠] x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₃g₁ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
Tactic: rw [hn] at h₃g
Cleared hypotheses: h₃g, this, h₃f, hn, h₀, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
h₁ :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      HPow.hPow (β := ℤ) (z - x) 0 •
        Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ z
⊢ g =ᶠ[𝓝[≠] x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₃g₁ : f =ᶠ[𝓝 x] g
Tactic: simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂
Cleared hypotheses: h₃g, h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
h₁ :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      HPow.hPow (β := ℤ) (z - x) 0 •
        Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ z
h₃g₁ : f =ᶠ[𝓝 x] g
⊢ g =ᶠ[𝓝[≠] x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₃ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
  f z =
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry z
Tactic: simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂
Cleared hypotheses: h₃g, h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update (β := fun (a : 𝕜) ↦ E) f x
      (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x)
      x =
    g x
have this₁ : g =ᶠ[𝓝 x]
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
    AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry
Tactic: have : g =ᶠ[𝓝 x]
              Classical.choose ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f) := by
            obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
            rw [← h₁g.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₀.continuousAt]
            rw [hn] at h₃g
            simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂
            exact (h₃g.filter_mono nhdsWithin_le_nhds).symm.trans h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this_1 : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this :
  g =ᶠ[𝓝 x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
⊢ Function.update (β := fun (a : 𝕜) ↦ E) f x
      (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x)
      x =
    g x
have pos : Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
    AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x =
  g x
Tactic: simp only [Function.update_self]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : ¬meromorphicOrderAt f x = 0
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
have neg : (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x =
  (if h : True then
      Function.update (β := fun (a : 𝕜) ↦ E) f x
        (if h_1 : meromorphicOrderAt f x = 0 then
          Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
            AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
        else 0)
    else 0)
    x
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : ¬meromorphicOrderAt f x = 0
⊢ (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x =
    (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x
have neg : HPow.hPow (α := 𝕜) 0 n = 0 ∨ g x = 0
Tactic: simp only [Pi.smul_apply', Pi.pow_apply, sub_self, h₃f, ↓reduceDIte, smul_eq_zero,
            Function.update_self, smul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : ¬meromorphicOrderAt f x = 0
⊢ HPow.hPow (α := 𝕜) 0 n = 0 ∨ g x = 0
have neg : HPow.hPow (α := 𝕜) 0 n = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : ¬meromorphicOrderAt f x = 0
⊢ HPow.hPow (α := 𝕜) 0 n = 0
have neg : n ≠ 0
Tactic: apply zero_zpow n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : ¬meromorphicOrderAt f x = 0
hn : n = 0
⊢ False
have this₁ : meromorphicOrderAt f x = (↑0 : WithTop ℤ)
Tactic: rw [hn] at this
Cleared hypotheses: this, h₃f, hn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
⊢ LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) ↔ AnalyticOnNhd 𝕜 f U
have mp : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) → AnalyticOnNhd 𝕜 f U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
mp : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) → AnalyticOnNhd 𝕜 f U
⊢ LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) ↔ AnalyticOnNhd 𝕜 f U
have mpr : AnalyticOnNhd 𝕜 f U → LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
⊢ AnalyticAt 𝕜 f x
have mp : 0 ≤ meromorphicOrderAt f x
Tactic: rw [← (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
⊢ 0 ≤ meromorphicOrderAt f x
have this : LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: have := h x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ U),
  LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
pos :
  ∀ (hx : x ∈ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ U),
  LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
have pos : 0 ≤ meromorphicOrderAt f x
Tactic: simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
        MeromorphicOn.divisor_apply, untop₀_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ U ∩ f ⁻¹' {0} = Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)
have h : ∀ (u : 𝕜),
  u ∈ U ∩ f ⁻¹' {0} ↔
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
⊢ u ∈ U ∩ f ⁻¹' {0} ↔
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
have h : u ∈ U ∩ f ⁻¹' {0} →
  Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
h :
  u ∈ U ∩ f ⁻¹' {0} →
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
⊢ u ∈ U ∩ f ⁻¹' {0} ↔
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
have h₁ : Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u →
  u ∈ U ∩ f ⁻¹' {0}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
⊢ u ∈ U ∩ f ⁻¹' {0}
have hu₁ : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
Tactic: simp only [Function.mem_support, ne_eq] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ u ∈ U ∩ f ⁻¹' {0}
have h : u ∈ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h : u ∈ U
⊢ u ∈ U ∩ f ⁻¹' {0}
have h₁ : u ∈ f ⁻¹' {0}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ f u = 0
have this : ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0
Tactic: have := h₁f ((MeromorphicOn.divisor f U).supportWithinDomain hu)
        |>.meromorphicOrderAt_eq_zero_iff.not
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
this : ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0
⊢ f u = 0
have hu₁ : ¬meromorphicOrderAt f u = 0 ∧ ¬meromorphicOrderAt f u = ⊤
Tactic: simp only [h₁f.meromorphicOn, (MeromorphicOn.divisor f U).supportWithinDomain hu,
        MeromorphicOn.divisor_apply, WithTop.untop₀_eq_zero, not_or] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
have mp : MeromorphicNFOn (g • f) U → MeromorphicNFOn f U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
mp : MeromorphicNFOn (g • f) U → MeromorphicNFOn f U
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
have mpr : MeromorphicNFOn f U → MeromorphicNFOn (g • f) U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt f z
have mp : MeromorphicNFAt (g • f) z
Tactic: rw [← meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g z hz) (h₂g z hz)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (g • f) z
have mpr : g z ≠ 0
Tactic: apply (h hz).smul_analytic (h₁g z hz)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U
have rw : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
Tactic: rw [← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U
have rw : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
Tactic: rw [mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
⊢ MeromorphicNFOn (E := 𝕜) (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) U
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
Tactic: convert! meromorphicNFOn_prod h₁f h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
⊢ 𝕜 → E
have pos : (h₁f : MeromorphicOn f U) → 𝕜 → E
Tactic: by_cases h₁f : MeromorphicOn f U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
pos : (h₁f : MeromorphicOn f U) → 𝕜 → E
⊢ 𝕜 → E
have neg : (h₁f : ¬MeromorphicOn f U) → 𝕜 → E
Tactic: by_cases h₁f : MeromorphicOn f U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
⊢ E
have pos : (hz : z ∈ U) → E
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
pos : (hz : z ∈ U) → E
⊢ E
have neg : (hz : z ∉ U) → E
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U
have this : U ∈ Filter.codiscreteWithin U
Tactic: have : U ∈ Filter.codiscreteWithin U := by simp
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
this : U ∈ Filter.codiscreteWithin U
⊢ f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U
have h : ∀ (a : 𝕜) (h₁a : AnalyticAt 𝕜 f a) (h₂a : a ∈ U), f a = toMeromorphicNFOn f U a
Tactic: filter_upwards [hf.analyticAt_mem_codiscreteWithin, this] with a h₁a h₂a