awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x < 0), (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
inr : ∀ (ho : 0 ≤ meromorphicOrderAt f x), (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x

Tactic:
rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | ho

Premises used: meromorphicOrderAt, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
inl : ∀ (x_1 : E), ¬Tendsto f (𝓝[≠] x) (𝓝 x_1)
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x

Tactic:
simp only [← not_lt, ho, not_true_eq_false, iff_false, not_exists]

Premises used: iff_false, not_exists, not_true_eq_false, not_lt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
inl : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Premises used: Filter.Tendsto.norm, not_tendsto_atTop_of_tendsto_nhds
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
inl : Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
rw [tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x

Tactic:
simp [ho, tendsto_nhds_of_meromorphicOrderAt_nonneg hf ho]

Premises used: tendsto_nhds_of_meromorphicOrderAt_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x = 0), (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
inr : ∀ (ho : meromorphicOrderAt f x ≠ 0), (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0

Tactic:
rcases eq_or_ne (meromorphicOrderAt f x) 0 with ho | ho

Premises used: meromorphicOrderAt, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0

Tactic:
simp [ho, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho]

Premises used: tendsto_ne_zero_of_meromorphicOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
inr : ∀ (x_1 : E), ¬x_1 = 0 → ¬Tendsto f (𝓝[≠] x) (𝓝 x_1)
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0

Tactic:
simp only [ne_eq, ho, iff_false, not_exists, not_and]

Premises used: iff_false, not_exists, ne_eq, not_and
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
inr : ∀ (ho : meromorphicOrderAt f x < 0), False
inr₁ : ∀ (ho : 0 < meromorphicOrderAt f x), False
⊢ False

Tactic:
rcases ho.lt_or_gt with ho | ho

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
inr : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Premises used: Filter.Tendsto.norm, not_tendsto_atTop_of_tendsto_nhds
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
inr : Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
rw [tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
inr : c = 0
⊢ False

Tactic:
apply c_ne
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
⊢ c = 0

Tactic:
tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)

Premises used: tendsto_zero_of_meromorphicOrderAt_pos, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
⊢ c = 0

Tactic:
exact tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)

Premises used: tendsto_zero_of_meromorphicOrderAt_pos, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : 0 < meromorphicOrderAt f x), Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
inr : ∀ (ho : meromorphicOrderAt f x ≤ 0), Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x

Tactic:
rcases lt_or_ge 0 (meromorphicOrderAt f x) with ho | ho

Premises used: meromorphicOrderAt, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : 0 < meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x

Tactic:
simp [ho, tendsto_zero_of_meromorphicOrderAt_pos ho]

Premises used: tendsto_zero_of_meromorphicOrderAt_pos
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≤ 0
inr : ¬Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x

Tactic:
simp only [← not_le, ho, not_true_eq_false, iff_false]

Premises used: not_le, iff_false, not_true_eq_false
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
inr : ∀ (ho : meromorphicOrderAt f x = 0), False
inr₁ : ∀ (ho : meromorphicOrderAt f x < 0), False
⊢ False

Tactic:
rcases ho.eq_or_lt with ho | ho

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
inr : ∀ (c : E) (c_ne : c ≠ 0) (h'c : Tendsto f (𝓝[≠] x) (𝓝 c)), False
⊢ False

Tactic:
obtain ⟨c, c_ne, h'c⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho

Premises used: tendsto_ne_zero_of_meromorphicOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
inr : c = 0
⊢ False

Tactic:
apply c_ne
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ c = 0

Tactic:
tendsto_nhds_unique h'c hc

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ c = 0

Tactic:
exact tendsto_nhds_unique h'c hc

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
inr : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ False

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds hc.norm

Premises used: Filter.Tendsto.norm, not_tendsto_atTop_of_tendsto_nhds
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
inr : Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
rw [tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₂ x
⊢ MeromorphicAt f₁ x

Tactic:
hf₁.congr hf₁₂.symm

Premises used: MeromorphicAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₂ x
⊢ MeromorphicAt f₁ x

Tactic:
exact hf₁.congr hf₁₂.symm

Premises used: MeromorphicAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt f₂ x

Tactic:
have : ¬ MeromorphicAt f₂ x := by
      contrapose hf₁
      exact hf₁.congr hf₁₂.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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₁, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] 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 h₁f₁ ⊢

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = 0

Tactic:
EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) hf₁₂.symm

Premises used: Eq, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = 0

Tactic:
exact EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) hf₁₂.symm

Premises used: Eq, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
neg : ∀ (n : ℤ) (hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
obtain ⟨n, hn : meromorphicOrderAt f₁ x = n⟩ := Option.ne_none_iff_exists'.mp h₁f₁

Premises used: Option.ne_none_iff_exists', meromorphicOrderAt, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
neg :
  ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z),
    meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
neg : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
rw [hn, eq_comm, meromorphicOrderAt_eq_int_iff (hf₁.congr hf₁₂)]

Premises used: meromorphicOrderAt_eq_int_iff, eq_comm, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z

Tactic:
use g, h₁g, h₂g
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
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 : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z

Tactic:
EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) hf₁₂.symm

Premises used: Eq, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
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 : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z

Tactic:
exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) hf₁₂.symm

Premises used: Eq, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
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
top : ∀ (hn : analyticOrderAt f x = ⊤), meromorphicOrderAt f x = ENat.map Nat.cast ⊤
coe : ∀ (a : ℕ) (hn : analyticOrderAt f x = (↑a : ℕ∞)), meromorphicOrderAt f x = ENat.map Nat.cast (↑a : ℕ∞)
⊢ meromorphicOrderAt f x = ENat.map Nat.cast (analyticOrderAt f x)

Tactic:
cases hn : analyticOrderAt f x

Premises used: analyticOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
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
hn : analyticOrderAt f x = ⊤
top : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ⊤

Tactic:
rw [ENat.map_top, meromorphicOrderAt_eq_top_iff]

Premises used: meromorphicOrderAt_eq_top_iff, ENat.map_top
-- Module: Mathlib.Analysis.Meromorphic.Order
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
hn : analyticOrderAt f x = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
(analyticOrderAt_eq_top.mp hn).filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, analyticOrderAt_eq_top, nhdsWithin_le_nhds, Iff.mp