awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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.insert a s, MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) x = ∑ i ∈ Insert.insert a s, meromorphicOrderAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
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))]

Premises used: Finset.prod_empty, MeromorphicAt.const, Insert.insert, meromorphicOrderAt_eq_int_iff, WithTop.coe_zero, Finset.sum_empty
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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.insert a s, MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) x = ∑ i ∈ Insert.insert a s, meromorphicOrderAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ 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))]

Premises used: Finset.prod_empty, MeromorphicAt.const, Insert.insert, meromorphicOrderAt_eq_int_iff, WithTop.coe_zero, Finset.sum_empty
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
meromorphicOrderAt_prod hf

Premises used: meromorphicOrderAt_prod
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
⊢ meromorphicOrderAt (E := 𝕜) (fun (a : 𝕜) ↦ ∏ i ∈ s, f i a) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
convert! meromorphicOrderAt_prod hf

Premises used: meromorphicOrderAt_prod
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
x_1 : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x_1) ((∏ i ∈ s, f i) x_1)

Tactic:
(Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
x_1 : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x_1) ((∏ i ∈ s, f i) x_1)

Tactic:
exact (Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
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
succ :
  ∀ (n : ℕ),
    meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x →
      meromorphicOrderAt (f ^ (n + 1)) x = (↑(n + 1) : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
induction n
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
simp : meromorphicOrderAt (E := 𝕜) 1 x = 0
⊢ meromorphicOrderAt (HPow.hPow (β := ℕ) f 0) x = (↑0 : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
simp only [pow_zero, CharP.cast_eq_zero, zero_mul]

Premises used: CharP.cast_eq_zero, MulZeroClass.zero_mul, pow_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
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
rw₁ : MeromorphicAt (E := 𝕜) 1 x
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0

Tactic:
rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]

Premises used: meromorphicOrderAt_eq_int_iff, WithTop.coe_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ Ne.{u_1 + 1} (α := 𝕜) (1 x) 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) (1 z)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
exact ⟨1, analyticAt_const, by simp⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt (E := 𝕜) 1 x

Tactic:
apply MeromorphicAt.const

Premises used: MeromorphicAt.const
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (HPow.hPow (β := ℕ) f 0) x = (↑0 : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
case zero =>
    simp only [pow_zero, CharP.cast_eq_zero, zero_mul]
    rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const

Premises used: CharP.cast_eq_zero, MulZeroClass.zero_mul, MeromorphicAt.const, meromorphicOrderAt_eq_int_iff, WithTop.coe_zero, pow_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
simp :
  (↑n : WithTop ℤ) * meromorphicOrderAt f x + meromorphicOrderAt f x =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ (n + 1)) x = (↑(n + 1) : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
simp only [pow_add, pow_one, meromorphicOrderAt_mul (hf.pow n) hf, hn, Nat.cast_add,
      Nat.cast_one]

Premises used: meromorphicOrderAt_mul, pow_add, Nat.cast_add, MeromorphicAt.pow, pow_one, Nat.cast_one
-- Module: Mathlib.Analysis.Meromorphic.Order
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 * ⊤
coe :
  ∀ (a : ℤ),
    (↑n : WithTop ℤ) * (↑a : WithTop ℤ) + (↑a : WithTop ℤ) =
      HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * (↑a : WithTop ℤ)
⊢ (↑n : WithTop ℤ) * meromorphicOrderAt f x + meromorphicOrderAt f x =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * meromorphicOrderAt f x

Tactic:
cases meromorphicOrderAt f x

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ HMul.hMul (α := WithTop ℤ) (↑n : WithTop ℤ) ⊤ + ⊤ = HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * ⊤

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
a : ℤ
coe : (↑n : ℤ) * a + a = (↑(n + 1) : ℤ) * a
⊢ (↑n : WithTop ℤ) * (↑a : WithTop ℤ) + (↑a : WithTop ℤ) =
    HAdd.hAdd (α := WithTop ℤ) (↑n : WithTop ℤ) 1 * (↑a : WithTop ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : ℤ) * a + a = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * a

Tactic:
ring
-- Module: Mathlib.Analysis.Meromorphic.Order
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
neg : ∀ (hn : ¬n = 0), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
pos : meromorphicOrderAt (E := 𝕜) 1 x = 0
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
simp only [hn, zpow_zero, WithTop.coe_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, zpow_zero, WithTop.coe_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
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
pos₁ : MeromorphicAt (E := 𝕜) 1 x
⊢ meromorphicOrderAt (E := 𝕜) 1 x = 0

Tactic:
rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]

Premises used: meromorphicOrderAt_eq_int_iff, WithTop.coe_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (1 x) 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) (1 z)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
exact ⟨1, analyticAt_const, by simp⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ MeromorphicAt (E := 𝕜) 1 x

Tactic:
apply MeromorphicAt.const

Premises used: MeromorphicAt.const
-- Module: Mathlib.Analysis.Meromorphic.Order
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
neg : ∀ (h : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
by_cases h : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
pos : meromorphicOrderAt (f ^ n) x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
simp only [h, ne_eq, WithTop.coe_eq_zero, hn, not_false_eq_true, WithTop.mul_top]

Premises used: WithTop.mul_top, WithTop.coe_eq_zero, ne_eq, not_false_eq_true
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
pos : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0
⊢ meromorphicOrderAt (f ^ n) x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at *

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
h₁ : ∀ (a : 𝕜), f a = 0 → (f ^ n) a = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = 0

Tactic:
filter_upwards [h]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
y : 𝕜
hy : f y = 0
⊢ (f ^ n) y = 0

Tactic:
simp [hy, zero_zpow n hn]

Premises used: zero_zpow
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
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
⊢ 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

Premises used: meromorphicOrderAt_ne_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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
neg :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • g z
⊢ meromorphicOrderAt (f ^ n) x = (↑n : WithTop ℤ) * meromorphicOrderAt f x

Tactic:
rw [← WithTop.coe_untop₀_of_ne_top h, ← WithTop.coe_mul,
    meromorphicOrderAt_eq_int_iff (hf.zpow n)]

Premises used: meromorphicOrderAt_eq_int_iff, WithTop.coe_untop₀_of_ne_top, MeromorphicAt.zpow, WithTop.coe_mul
-- Module: Mathlib.Analysis.Meromorphic.Order
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 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • g z

Tactic:
use g ^ n, h₁g.zpow h₂g

Premises used: AnalyticAt.zpow
-- Module: Mathlib.Analysis.Meromorphic.Order
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
right₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
⊢ (g ^ n) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.Order
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

Tactic:
simp_all [zpow_eq_zero_iff hn]

Premises used: zpow_eq_zero_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z

Tactic:
filter_upwards [h₃g]
-- Module: Mathlib.Analysis.Meromorphic.Order
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 * g y ^ n =
    (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y
⊢ (f ^ n) y = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y

Tactic:
rw [Pi.pow_apply, hy, smul_eq_mul, mul_zpow]

Premises used: mul_zpow, Pi.pow_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Meromorphic.Order
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) ^ (n * (meromorphicOrderAt f x).untop₀)
⊢ ((y - x) ^ (meromorphicOrderAt f x).untop₀) ^ n * g y ^ n =
    (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y

Tactic:
congr 1
-- Module: Mathlib.Analysis.Meromorphic.Order
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)
h₂ 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₀)

Tactic:
rw [mul_comm, zpow_mul]

Premises used: zpow_mul, mul_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
by_cases hf : MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : ¬MeromorphicAt f x
contrapose : ∀ (hf : MeromorphicAt f⁻¹ x), MeromorphicAt f x
⊢ ¬MeromorphicAt f⁻¹ x

Tactic:
contrapose hf
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x

Tactic:
simpa using hf.inv

Premises used: MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : ¬MeromorphicAt f x
⊢ ¬MeromorphicAt f⁻¹ x

Tactic:
have : ¬ MeromorphicAt (f⁻¹) x := by
      contrapose hf
      simpa using hf.inv
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : ¬MeromorphicAt f x
this : ¬MeromorphicAt f⁻¹ x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
simp [hf, this]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
pos : ∀ (h₂f : meromorphicOrderAt f x = ⊤), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
neg : ∀ (h₂f : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
by_cases h₂f : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
pos : meromorphicOrderAt f⁻¹ x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
rw [h₂f, ← LinearOrderedAddCommGroupWithTop.neg_top, neg_neg]

Premises used: neg_neg, LinearOrderedAddCommGroupWithTop.neg_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
pos : ∀ (h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0
⊢ meromorphicOrderAt f⁻¹ x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at *

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
h : ∀ (a : 𝕜), f a = 0 → f⁻¹ a = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0

Tactic:
filter_upwards [h₂f]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ (a : 𝕜), f a = 0 → f⁻¹ a = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x ≠ ⊤

Tactic:
h₂f
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
h₂f : ¬meromorphicOrderAt f x = ⊤
neg : ∀ (a : ℤ) (ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x), meromorphicOrderAt f⁻¹ x = -(↑a : WithTop ℤ)
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂f with a ha

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
neg :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z
⊢ meromorphicOrderAt f⁻¹ x = -(↑a : WithTop ℤ)

Tactic:
apply (meromorphicOrderAt_eq_int_iff hf.inv).2

Premises used: Iff.mpr, meromorphicOrderAt_eq_int_iff, MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
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
⊢ ∃ (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

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm