awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
hx :
  Norm.norm (E := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) ≠ 0
⊢ log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ (u : 𝕜), (↑(D u) : ℝ) * log ‖x - u‖ + log ‖g x‖
have hy : ‖g x‖ ≠ 0
Tactic: rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
        (((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt)
          h₁x h₂x h),
    ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).meromorphicTrailingCoeffAt_smul
      h₁g.meromorphicAt, h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g,
    norm_smul, log_mul, log_norm_meromorphicTrailingCoeffAt hD]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ Norm.norm (E := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) ≠ 0
have hx : ¬Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) 0
Tactic: simp only [ne_eq, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ ¬Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) 0
have hx : meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x ≠ ⊤
Tactic: apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero
      ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ f =ᶠ[𝓝[≠] x] 0
have rw : ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: rw [← hf.frequently_zero_iff_eventuallyEq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have apply : ∀ (x : 𝕜), x ∈ U ∧ x ∈ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = 0 x) x} ∪ Uᶜ → f x = 0
Tactic: apply ((accPt_iff_frequently_nhdsNE.1 h₂x).and_eventually <| eventually_mem_set.2
    (mem_codiscreteWithin_iff_forall_mem_nhdsNE.1 h x h₁x)).mono
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
⊢ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0
have h : ∀ (x : 𝕜) (h₁x : AnalyticAt 𝕜 f x) (h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)), f x ≠ 0
Tactic: filter_upwards [h₁f.analyticAt_mem_codiscreteWithin,
    h₁f.codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top h₂f] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
x : 𝕜
h₁x : AnalyticAt 𝕜 f x
h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)
⊢ f x ≠ 0
have this : meromorphicOrderAt f x ≠ ⊤
Tactic: have := h₂f x h₂x.1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ f =ᶠ[𝓝[≠] x] g
have rw : (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, (f - g) z = 0
Tactic: rw [eventuallyEq_iff_sub, ← (hf.sub hg).frequently_zero_iff_eventuallyEq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, (f - g) z = 0
have simp_rw : (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z - g z = 0
Tactic: simp_rw [Pi.sub_apply, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] g
⊢ f =ᶠ[𝓝[≠] x] g
have rw : ∀ (h : f - g =ᶠ[codiscreteWithin U] 0), f - g =ᶠ[𝓝[≠] x] 0
Tactic: rw [eventuallyEq_iff_sub] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∀ᶠ (x : 𝕜) in 𝓝ˢ U, f =ᶠ[𝓝[≠] x] g
have rw : ∃ (t : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g
Tactic: rw [eventually_nhdsSet_iff_exists]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∃ (t : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g
have h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧
  U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} x → f =ᶠ[𝓝[≠] x] g
Tactic: use {x | f =ᶠ[𝓝[≠] x] g}
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧
    U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} x → f =ᶠ[𝓝[≠] x] g
have h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
Tactic: simp only [Set.mem_setOf_eq, imp_self, implies_true, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
have h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
have h₂ : U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
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
x : 𝕜
⊢ MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have mp : MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
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
x : 𝕜
mp : MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have mpr : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0 → MeromorphicNFAt f x
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
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
⊢ MeromorphicAt f x
have apply : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: apply MeromorphicAt.congr _ (h₃g.filter_mono nhdsWithin_le_nhds).symm
-- 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 : 𝕜
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
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have hf : MeromorphicAt f x
Tactic: have hf : MeromorphicAt f x := by
        apply MeromorphicAt.congr _ (h₃g.filter_mono nhdsWithin_le_nhds).symm
        fun_prop
-- 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 : 𝕜
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
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)
have rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: rw [meromorphicOrderAt_eq_int_iff hf]
-- 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 : 𝕜
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
hf : MeromorphicAt f x
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: use g, h₁g, h₂g
-- 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 : 𝕜
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
hf : MeromorphicAt f x
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
Tactic: have : meromorphicOrderAt f x = n := by
        rw [meromorphicOrderAt_eq_int_iff hf]
        use g, h₁g, h₂g
        exact eventually_nhdsWithin_of_eventually_nhds h₃g
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have pos : ∀ (hn : 0 ≤ n), AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: by_cases! hn : 0 ≤ n
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
pos : ∀ (hn : 0 ≤ n), AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have neg : ∀ (hn : n < 0), AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: by_cases! hn : 0 ≤ n
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have pos : AnalyticAt 𝕜 f x
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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 f x
have pos : AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: rw [analyticAt_congr h₃g]
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : n < 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have neg : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: right
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : n < 0
⊢ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
have right : meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: use hf
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
⊢ MeromorphicNFAt f x
have pos : ∀ (h₂f : analyticOrderAt f x = ⊤), MeromorphicNFAt f x
Tactic: by_cases h₂f : analyticOrderAt f 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
x : 𝕜
h : AnalyticAt 𝕜 f x
pos : ∀ (h₂f : analyticOrderAt f x = ⊤), MeromorphicNFAt f x
⊢ MeromorphicNFAt f x
have neg : ∀ (h₂f : ¬analyticOrderAt f x = ⊤), MeromorphicNFAt f x
Tactic: by_cases h₂f : analyticOrderAt f x = ⊤
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : analyticOrderAt f x = ⊤
⊢ MeromorphicNFAt f x
have h₂f₁ : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
Tactic: rw [analyticOrderAt_eq_top] at h₂f
Cleared hypotheses: 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
x : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
⊢ MeromorphicNFAt f x
have pos : ¬f =ᶠ[𝓝 x] 0 →
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: tauto
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
⊢ MeromorphicNFAt f x
have neg : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: right
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
have h₁ : ∃ (g : 𝕜 → E),
  AnalyticAt 𝕜 g x ∧
    g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
Tactic: use analyticOrderNatAt f x
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
have this : analyticOrderAt f x ≠ ⊤
Tactic: have : analyticOrderAt f x ≠ ⊤ := h₂f
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
this : analyticOrderAt f x ≠ ⊤
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
have this₁ : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
Tactic: rw [← ENat.coe_toNat_eq_self, eq_comm, h.analyticOrderAt_eq_natCast] at this
Cleared hypotheses: this
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
this : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
have h₁ : ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
  (h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z),
  ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
Cleared hypotheses: this
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
have right : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
Tactic: use g, h₁g, h₂g
-- 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 : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ MeromorphicNFAt f x
have mpr : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: right
-- 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 : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
have mpr : ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x)
  (meromorphicNFAt_iff_analyticAt_or :
    MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0)
  (h₂ : (↑n : WithTop ℤ) < 0),
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: lift meromorphicOrderAt f x to ℤ using LT.lt.ne_top h₂ with n hn
Cleared hypotheses: 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
have mpr : ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff h₁).1 hn.symm