awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
have right : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: use n, 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₃ : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
have h : ∀ (a : 𝕜),
  (Membership.mem (γ := Set 𝕜) {x}ᶜ a → f a = (a - x) ^ n • g a) →
    f a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) a
Tactic: filter_upwards [eventually_nhdsWithin_iff.1 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₃ : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
have pos : ∀ (h₁z : z = x), f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
Tactic: by_cases h₁z : z = 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₁ : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
pos : ∀ (h₁z : z = x), f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
have neg : ∀ (h₁z : ¬z = x), f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
Tactic: by_cases h₁z : z = 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₁ : 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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
have pos : f x = HPow.hPow (α := 𝕜) 0 n • g x
Tactic: simp only [h₁z, Pi.smul_apply', Pi.pow_apply, sub_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 : 𝕜
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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
⊢ f x = HPow.hPow (α := 𝕜) 0 n • g x
have pos : 0 = HPow.hPow (α := 𝕜) 0 n • g x
Tactic: rw [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
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
⊢ 0 = HPow.hPow (α := 𝕜) 0 n • g x
have apply : n ≠ 0
Tactic: apply (smul_eq_zero_of_left (zero_zpow n _) (g x)).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 : 𝕜
hf : MeromorphicNFAt f x
⊢ MeromorphicAt f x
have hf₁ : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: rw [meromorphicNFAt_iff_analyticAt_or] at hf
Cleared hypotheses: 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 : 𝕜
hf : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x
have inl : ∀ (h : AnalyticAt 𝕜 f x), MeromorphicAt f x
Tactic: rcases hf with h | h
Cleared hypotheses: 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 : 𝕜
hf : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
inl : ∀ (h : AnalyticAt 𝕜 f x), MeromorphicAt f x
⊢ MeromorphicAt f x
have inr : ∀ (h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0), MeromorphicAt f x
Tactic: rcases hf with h | h
Cleared hypotheses: hf
-- 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 : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
hf : MeromorphicAt f x
⊢ MeromorphicAt f x
have right : meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: obtain ⟨hf, _⟩ := h
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 : 𝕜
hf : MeromorphicNFAt f x
⊢ 0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x
have mp : 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 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 : 𝕜
hf : MeromorphicNFAt f x
mp : 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 f x
⊢ 0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x
have mpr : AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x
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
x : 𝕜
hf : MeromorphicNFAt f x
h₂f : 0 ≤ meromorphicOrderAt f x
⊢ AnalyticAt 𝕜 f x
have hf₁ : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Tactic: rw [meromorphicNFAt_iff_analyticAt_or] at hf
Cleared hypotheses: hf, 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 : 𝕜
hf : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
h₂f : 0 ≤ meromorphicOrderAt f x
⊢ AnalyticAt 𝕜 f x
have mp : ∀ (h : AnalyticAt 𝕜 f x), AnalyticAt 𝕜 f x
Tactic: rcases hf with h | ⟨_, h₃f, _⟩
Cleared hypotheses: 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 : 𝕜
hf : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
h₂f : 0 ≤ meromorphicOrderAt f x
mp : ∀ (h : AnalyticAt 𝕜 f x), AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x
have mp₁ : MeromorphicAt f x → ∀ (h₃f : meromorphicOrderAt f x < 0), f x = 0 → AnalyticAt 𝕜 f x
Tactic: rcases hf with h | ⟨_, h₃f, _⟩
Cleared hypotheses: 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₂f : 0 ≤ meromorphicOrderAt f x
left : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right : f x = 0
⊢ AnalyticAt 𝕜 f x
have mp : ∀ (h' : ¬AnalyticAt 𝕜 f x), False
Tactic: by_contra 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 : 𝕜
hf : MeromorphicNFAt f x
h₂f : AnalyticAt 𝕜 f x
⊢ 0 ≤ meromorphicOrderAt f x
have mpr : LE.le (α := WithTop ℤ) 0 (ENat.map Nat.cast (analyticOrderAt f x))
Tactic: rw [h₂f.meromorphicOrderAt_eq]
-- 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
⊢ {x : 𝕜 | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U
have h : ∀ (a : 𝕜) (ha : AnalyticAt 𝕜 f a), MeromorphicNFAt f a
Tactic: filter_upwards [hf.analyticAt_mem_codiscreteWithin] with _ ha
-- 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 : 𝕜
hf : MeromorphicNFAt f x
⊢ meromorphicOrderAt f x = 0 ↔ f x ≠ 0
have mp : 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 : 𝕜
hf : MeromorphicNFAt f x
mp : meromorphicOrderAt f x = 0 → f x ≠ 0
⊢ meromorphicOrderAt f x = 0 ↔ f x ≠ 0
have mpr : f x ≠ 0 → meromorphicOrderAt f x = 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
x : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
⊢ f x ≠ 0
have h₂f : AnalyticAt 𝕜 f x
Tactic: have h₂f := hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq h₁f.symm)
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
h₂f : AnalyticAt 𝕜 f x
⊢ f x ≠ 0
have mp : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0
Tactic: rw [← h₂f.analyticOrderAt_eq_zero, ← ENat.map_natCast_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 : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
h₂f : AnalyticAt 𝕜 f x
⊢ Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0
have mp : ∀ (h₁f : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0) (h₂f : AnalyticAt 𝕜 f x),
  Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0
Tactic: rwa [h₂f.meromorphicOrderAt_eq] at h₁f
Cleared hypotheses: 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
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
⊢ meromorphicOrderAt f x = 0
have mpr : ∀ (h₁ : f =ᶠ[𝓝 x] 0), meromorphicOrderAt f x = 0
Tactic: rcases id hf with h₁ | ⟨n, g, h₁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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
mpr : ∀ (h₁ : f =ᶠ[𝓝 x] 0), meromorphicOrderAt f x = 0
⊢ meromorphicOrderAt f x = 0
have mpr₁ : ∀ (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), meromorphicOrderAt f x = 0
Tactic: rcases id hf with h₁ | ⟨n, g, h₁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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
h₁ : f =ᶠ[𝓝 x] 0
⊢ meromorphicOrderAt f x = 0
have this : f x = 0 x
Tactic: have := h₁.eq_of_nhds
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
⊢ n = 0
have by_contra : ∀ (hContra : ¬n = 0), False
Tactic: by_contra hContra
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
hContra : ¬n = 0
⊢ False
have this : f x = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: have := h₃g.eq_of_nhds
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
hContra : ¬n = 0
this : f x = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
⊢ False
have this₁ : f x = 0
Tactic: simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
Cleared hypotheses: this
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
⊢ meromorphicOrderAt f x = 0
have this : n = 0
Tactic: have : n = 0 := by
        by_contra hContra
        have := h₃g.eq_of_nhds
        simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
        tauto
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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 : n = 0
⊢ meromorphicOrderAt f x = 0
have h₃g₁ : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
Tactic: simp only [this, zpow_zero] at h₃g
Cleared hypotheses: 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ meromorphicOrderAt f x = 0
have mpr : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
Tactic: apply (meromorphicOrderAt_eq_int_iff hf.meromorphicAt).2
-- 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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
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 : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (g z)
Tactic: simp only [zpow_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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g
have mp : f =ᶠ[𝓝[≠] x] g → 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
mp : f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g
have mpr : f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
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
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝 x] g
have t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
Tactic: have t₀ := meromorphicOrderAt_congr 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
⊢ f =ᶠ[𝓝 x] g
have pos : ∀ (cs : meromorphicOrderAt f x = 0), f =ᶠ[𝓝 x] g
Tactic: by_cases cs : meromorphicOrderAt f x = 0
-- 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
pos : ∀ (cs : meromorphicOrderAt f x = 0), f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝 x] g
have neg : ∀ (cs : ¬meromorphicOrderAt f x = 0), f =ᶠ[𝓝 x] g
Tactic: by_cases cs : meromorphicOrderAt f x = 0
-- 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
⊢ f =ᶠ[𝓝 x] g
have t₁ : 0 = meromorphicOrderAt g x
Tactic: rw [cs] at t₀
Cleared hypotheses: t₀, cs
-- 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
⊢ f =ᶠ[𝓝 x] g
have Z : ContinuousAt f x
Tactic: have Z := (hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq cs.symm)).continuousAt
-- 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
Z : ContinuousAt f x
⊢ f =ᶠ[𝓝 x] g
have W : ContinuousAt g x
Tactic: have W := (hg.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq t₀)).continuousAt
-- 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
⊢ f =ᶠ[𝓝 x] g
have neg : f x = g x
Tactic: apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬meromorphicOrderAt f x = 0 := cs
⊢ f x = g x
have h₁f₁ : ¬f x ≠ 0
Tactic: rw [hf.meromorphicOrderAt_eq_zero_iff] at h₁f
Cleared hypotheses: 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬meromorphicOrderAt f x = 0 := cs
⊢ f x = g x
have h₁g₁ : ¬g x ≠ 0
Tactic: rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g
Cleared hypotheses: 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
⊢ f x = g x
have h₁f₁ : f x = 0
Tactic: simp only [not_not] at *
Cleared hypotheses: h₁f, h₁g