awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (hs :
    ∀ (hf : ∀ i ∈ s, MeromorphicAt (f i) x),
      meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x)
  (hf : ∀ i ∈ insert a s, MeromorphicAt (f i) x),
  meromorphicOrderAt (E := 𝕜) (∏ i ∈ insert a s, f i) x = ∑ i ∈ insert a s, meromorphicOrderAt (f i) x
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.prod_insert ha, meromorphicOrderAt_mul
      (hf a (Finset.mem_insert_self a s))
      (MeromorphicAt.prod (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))]
    congr
    rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (fun (a : 𝕜) ↦ ∏ i ∈ s, f i a) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
Tactic: convert! meromorphicOrderAt_prod hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have induction : meromorphicOrderAt (HPow.hPow (β := ℕ) f 0) x = (↑0 : WithTop ℤ) * meromorphicOrderAt f x
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
induction : meromorphicOrderAt (HPow.hPow (β := ℕ) f 0) x = (↑0 : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have succ : ∀ (n : ℕ),
  meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x →
    meromorphicOrderAt (f ^ (n + 1)) x = (↑(n + 1) : WithTop ℤ) * meromorphicOrderAt f x
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (HPow.hPow (β := ℕ) f 0) x = (↑0 : WithTop ℤ) * meromorphicOrderAt f x
have simp : meromorphicOrderAt (E := 𝕜) 1 x = 0
Tactic: simp only [pow_zero, CharP.cast_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0
have rw : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
Tactic: rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
rw : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0
have rw₁ : MeromorphicAt (E := 𝕜) 1 x
Tactic: rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ (n + 1)) x = (↑(n + 1) : WithTop ℤ) * meromorphicOrderAt f x
have simp : (↑n : WithTop ℤ) * meromorphicOrderAt f x + meromorphicOrderAt f x =
  HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * meromorphicOrderAt f x
Tactic: simp only [pow_add, pow_one, meromorphicOrderAt_mul (hf.pow n) hf, hn, Nat.cast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ (↑n : WithTop ℤ) * meromorphicOrderAt f x + meromorphicOrderAt f x =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * meromorphicOrderAt f x
have top : HMul.hMul (α := WithTop ℤ) (↑n : WithTop ℤ) ⊤ + ⊤ = HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * ⊤
Tactic: cases meromorphicOrderAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
top : HMul.hMul (α := WithTop ℤ) (↑n : WithTop ℤ) ⊤ + ⊤ = HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * ⊤
⊢ (↑n : WithTop ℤ) * meromorphicOrderAt f x + meromorphicOrderAt f x =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * meromorphicOrderAt f x
have coe : ∀ (a : ℤ),
  (↑n : WithTop ℤ) * (↑a : WithTop ℤ) + (↑a : WithTop ℤ) =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * (↑a : WithTop ℤ)
Tactic: cases meromorphicOrderAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
a : ℤ
⊢ (↑n : WithTop ℤ) * (↑a : WithTop ℤ) + (↑a : WithTop ℤ) =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * (↑a : WithTop ℤ)
have coe : (↑n : ℤ) * a + a = (↑(n + 1) : ℤ) * a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have pos : ∀ (hn : n = 0), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
pos : ∀ (hn : n = 0), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have neg : ∀ (hn : ¬n = 0), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have pos : meromorphicOrderAt (E := 𝕜) 1 x = 0
Tactic: simp only [hn, zpow_zero, WithTop.coe_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0
have pos : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
Tactic: rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
pos : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0
have pos₁ : MeromorphicAt (E := 𝕜) 1 x
Tactic: rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have pos : ∀ (h : meromorphicOrderAt f x = ⊤), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
Tactic: by_cases h : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
pos : ∀ (h : meromorphicOrderAt f x = ⊤), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have neg : ∀ (h : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
Tactic: by_cases h : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have pos : meromorphicOrderAt (f ^ n) x = ⊤
Tactic: simp only [h, ne_eq, WithTop.coe_eq_zero, hn, not_false_eq_true, WithTop.mul_top]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ⊤
have pos : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0
Tactic: rw [meromorphicOrderAt_eq_top_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0
have h₁ : ∀ (a : 𝕜), f a = 0 → (f ^ n) a = 0
Tactic: filter_upwards [h]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have neg : ∀ (g : 𝕜 → 𝕜) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
  (h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z),
  meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
have neg : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • g z
Tactic: rw [← WithTop.coe_untop₀_of_ne_top h, ← WithTop.coe_mul,
    meromorphicOrderAt_eq_int_iff (hf.zpow n)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • g z
have right : (g ^ n) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
Tactic: use g ^ n, h₁g.zpow h₂g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ (g ^ n) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
have right : (g ^ n) x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
right : (g ^ n) x ≠ 0
⊢ (g ^ n) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
have right₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
have h₁ : ∀ (a : 𝕜),
  f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a →
    (f ^ n) a = (a - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) a
Tactic: filter_upwards [h₃g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
⊢ (f ^ n) y = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y
have h₁ : ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n * g y ^ n = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y
Tactic: rw [Pi.pow_apply, hy, smul_eq_mul, mul_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
⊢ ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n * g y ^ n =
    (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y
have h₁ : ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
⊢ ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀)
have h₁ : ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = (y - x) ^ ((meromorphicOrderAt f x).untop₀ * n)
Tactic: rw [mul_comm, zpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₁ : ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = (y - x) ^ ((meromorphicOrderAt f x).untop₀ * n)
⊢ ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀)
have h₂ : ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n = ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n
Tactic: rw [mul_comm, zpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Tactic: by_cases hf : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Tactic: by_cases hf : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : ¬MeromorphicAt f x
⊢ ¬MeromorphicAt f⁻¹ x
have contrapose : ∀ (hf : MeromorphicAt f⁻¹ x), MeromorphicAt f x
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have this : ¬MeromorphicAt f⁻¹ x
Tactic: have : ¬ MeromorphicAt (f⁻¹) x := by
      contrapose hf
      simpa using hf.inv
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have pos : ∀ (h₂f : meromorphicOrderAt f x = ⊤), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Tactic: by_cases h₂f : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
pos : ∀ (h₂f : meromorphicOrderAt f x = ⊤), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have neg : ∀ (h₂f : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Tactic: by_cases h₂f : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have pos : meromorphicOrderAt f⁻¹ x = ⊤
Tactic: rw [h₂f, ← LinearOrderedAddCommGroupWithTop.neg_top, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = ⊤
have pos : ∀ (h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0
Tactic: rw [meromorphicOrderAt_eq_top_iff] at *
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0
have h : ∀ (a : 𝕜), f a = 0 → f⁻¹ a = 0
Tactic: filter_upwards [h₂f]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
have neg : ∀ (a : ℤ) (ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x), meromorphicOrderAt f⁻¹ x = -(↑a : WithTop ℤ)
Tactic: lift meromorphicOrderAt f x to ℤ using h₂f with a ha
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
⊢ meromorphicOrderAt f⁻¹ x = -(↑a : WithTop ℤ)
have neg : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z
Tactic: apply (meromorphicOrderAt_eq_int_iff hf.inv).2
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z
have neg : ∀ (g : 𝕜 → 𝕜) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z),
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 ha.symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ z
Tactic: use g⁻¹, h₁g.inv h₂g, inv_eq_zero.not.2 h₂g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ z
have right : ∀ (h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1),
  ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f⁻¹ x_1 = HPow.hPow (β := ℤ) (x_1 - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ x_1
Tactic: rw [eventually_nhdsWithin_iff] at *
Cleared hypotheses: h₃g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f⁻¹ x_1 = HPow.hPow (β := ℤ) (x_1 - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ x_1
have h : ∀ (a_1 : 𝕜),
  (Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f a_1 = (a_1 - x) ^ a • g a_1) →
    Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f⁻¹ a_1 = (a_1 - x) ^ (-a) • g⁻¹ a_1
Tactic: filter_upwards [h₃g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1
a_1 : 𝕜
h₁a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f a_1 = (a_1 - x) ^ a • g a_1
h₂a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1
⊢ f⁻¹ a_1 = (a_1 - x) ^ (-a) • g⁻¹ a_1
have h : (g a_1)⁻¹ * ((a_1 - x) ^ a)⁻¹ = ((a_1 - x) ^ a)⁻¹ * (g a_1)⁻¹
Tactic: simp only [Pi.inv_apply, h₁a h₂a, smul_eq_mul, mul_inv_rev, zpow_neg]