awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt f x
have rw : MeromorphicAt (g + f) x ↔ MeromorphicAt f x
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hfg : f =ᶠ[𝓝[≠] x] g
⊢ MeromorphicAt g x
have rcases : ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt g x
Tactic: rcases hf with ⟨m, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ MeromorphicAt g x
have refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x
Tactic: refine ⟨m + 1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x
have this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
Tactic: have : AnalyticAt 𝕜 (fun z ↦ z - x) x := analyticAt_id.sub analyticAt_const
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x
have refine : EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z
Tactic: refine (this.fun_smul hf).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z
have rw : ∀ (hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1) (m : ℕ)
  (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x)
  (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x),
  EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z
Tactic: rw [eventuallyEq_nhdsWithin_iff] at hfg
Cleared hypotheses: hfg, m, hf, this
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z
have h : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z), (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
Tactic: filter_upwards [hfg] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
have h : ∀ (hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, Membership.mem (γ := Set 𝕜) {z}ᶜ x → f x = g x)
  (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
  (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ z_1 - z) z) (hz : Membership.mem (γ := Set 𝕜) {z}ᶜ z → f z = g z),
  (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z
Tactic: rcases eq_or_ne z x with rfl | hn
Cleared hypotheses: x, hfg, hf, this, hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
h :
  ∀ (hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, Membership.mem (γ := Set 𝕜) {z}ᶜ x → f x = g x)
    (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
    (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ z_1 - z) z) (hz : Membership.mem (γ := Set 𝕜) {z}ᶜ z → f z = g z),
    (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
have h₁ : ∀ (hn : z ≠ x), (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
Tactic: rcases eq_or_ne z x with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
have h : (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z
Tactic: rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
hn : z ≠ x
h : (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
have h₁ : (z - x) • (z - x) ^ m • g z = ((z - x) * (z - x) ^ m) • g z
Tactic: rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
hn : z ≠ x
h : (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z
h₁ : (z - x) • (z - x) ^ m • g z = ((z - x) * (z - x) ^ m) • g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
have h₂ : (z - x) • (z - x) ^ m • g z = (z - x) • (z - x) ^ m • g z
Tactic: rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
⊢ MeromorphicAt f⁻¹ x
have rcases : ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt f⁻¹ x
Tactic: rcases hf with ⟨m, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ MeromorphicAt f⁻¹ x
have pos : ∀ (h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0), MeromorphicAt f⁻¹ x
Tactic: by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
pos : ∀ (h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0), MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f⁻¹ x
have neg : ∀ (h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0), MeromorphicAt f⁻¹ x
Tactic: by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
⊢ MeromorphicAt f⁻¹ x
have pos : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f⁻¹
Tactic: refine (MeromorphicAt.const 0 x).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f⁻¹
have pos : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → 0 = f⁻¹ x_1
Tactic: rw [eventuallyEq_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → 0 = f⁻¹ x_1
have h : ∀ (z : 𝕜) (hfz : (z - x) ^ m • f z = 0 z) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), 0 = f⁻¹ z
Tactic: filter_upwards [h_eq] with z hfz hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ 0 = f⁻¹ z
have h : 0 = (f z)⁻¹
Tactic: rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
      inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
h : 0 = (f z)⁻¹
⊢ 0 = f⁻¹ z
have h₁ : Eq.{u_2 + 1} (α := 𝕜') 0 0⁻¹
Tactic: rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
      inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
h : 0 = (f z)⁻¹
h₁ : Eq.{u_2 + 1} (α := 𝕜') 0 0⁻¹
⊢ 0 = f⁻¹ z
have h₂ : Eq.{u_2 + 1} (α := 𝕜') 0 0
Tactic: rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
      inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
⊢ MeromorphicAt f⁻¹ x
have neg : ∀ (n : ℕ) (g : 𝕜 → 𝕜') (hg_an : AnalyticAt 𝕜 g x) (hg_ne : g x ≠ 0)
  (hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z), MeromorphicAt f⁻¹ x
Tactic: obtain ⟨n, g, hg_an, hg_ne, hg_eq⟩ := hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h_eq
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
⊢ MeromorphicAt f⁻¹ x
have this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
Tactic: have : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x :=
      (analyticAt_id.sub analyticAt_const).pow _
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
⊢ MeromorphicAt f⁻¹ x
have neg : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (i : 𝕜) ↦ (i - x) ^ (m + 1) • g⁻¹ i) fun (z : 𝕜) ↦
  (z - x) ^ (n + 1) • f⁻¹ z
Tactic: refine ⟨n + 1, (this.fun_smul <| hg_an.inv hg_ne).congr ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (i : 𝕜) ↦ (i - x) ^ (m + 1) • g⁻¹ i) fun (z : 𝕜) ↦
    (z - x) ^ (n + 1) • f⁻¹ z
have h : ∀ (z : 𝕜) (hfg : (z - x) ^ m • f z = (z - x) ^ n • g z) (hg_ne' : g z ≠ 0),
  (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
Tactic: filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
have h : ∀ (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
  (h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 z) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) 0) (hg_an : AnalyticAt 𝕜 g z)
  (hg_ne : g z ≠ 0) (hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1)
  (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ (m + 1)) z) (hfg : (z - z) ^ m • f z = (z - z) ^ n • g z),
  (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z
Tactic: rcases eq_or_ne z x with rfl | hz_ne
Cleared hypotheses: x, hf, h_eq, hg_an, hg_ne, hg_eq, this, hfg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
h :
  ∀ (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
    (h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 z) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) 0)
    (hg_an : AnalyticAt 𝕜 g z) (hg_ne : g z ≠ 0)
    (hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1)
    (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ (m + 1)) z)
    (hfg : (z - z) ^ m • f z = (z - z) ^ n • g z), (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
have h₁ : ∀ (hz_ne : z ≠ x), (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
Tactic: rcases eq_or_ne z x with rfl | hz_ne
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
have hfg₁ : Eq.{u_2 + 1} (α := 𝕜') ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ m • f z)) ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ n • g z))
Tactic: replace hfg := congr_arg (·⁻¹) hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : Eq.{u_2 + 1} (α := 𝕜') ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ m • f z)) ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ n • g z))
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
have hfg₁ : ((z - x) ^ m)⁻¹ • (f z)⁻¹ = ((z - x) ^ n)⁻¹ • (g z)⁻¹
Tactic: simp only [smul_inv₀] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : ((z - x) ^ m)⁻¹ • (f z)⁻¹ = ((z - x) ^ n)⁻¹ • (g z)⁻¹
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
have hfg₁ : (z - x) ^ n • (f z)⁻¹ = (z - x) ^ m • (g z)⁻¹
Tactic: rw [inv_smul_eq_iff₀ (pow_ne_zero m (sub_ne_zero.mpr hz_ne)), smul_comm,
        eq_inv_smul_iff₀ (pow_ne_zero n (sub_ne_zero.mpr hz_ne))] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℕ
⊢ MeromorphicAt (f ^ n) x
have zero : MeromorphicAt (HPow.hPow (β := ℕ) f 0) x
Tactic: induction n with
  | zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
  | succ m hm => simpa only [pow_succ] using hm.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℕ
zero : MeromorphicAt (HPow.hPow (β := ℕ) f 0) x
⊢ MeromorphicAt (f ^ n) x
have succ : ∀ (m : ℕ) (hm : MeromorphicAt (f ^ m) x), MeromorphicAt (f ^ (m + 1)) x
Tactic: induction n with
  | zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
  | succ m hm => simpa only [pow_succ] using hm.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℤ
⊢ MeromorphicAt (f ^ n) x
have ofNat : ∀ (m : ℕ), MeromorphicAt (f ^ Int.ofNat m) x
Tactic: cases n with
  | ofNat m => simpa only [Int.ofNat_eq_natCast, zpow_natCast] using hf.pow m
  | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℤ
ofNat : ∀ (m : ℕ), MeromorphicAt (f ^ Int.ofNat m) x
⊢ MeromorphicAt (f ^ n) x
have negSucc : ∀ (m : ℕ), MeromorphicAt (f ^ Int.negSucc m) x
Tactic: cases n with
  | ofNat m => simpa only [Int.ofNat_eq_natCast, zpow_natCast] using hf.pow m
  | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)
Cleared hypotheses: n