awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
h₁f₁ : f x = 0
⊢ f x = g x
have h₁g₁ : g x = 0
Tactic: simp only [not_not] at *
Cleared hypotheses: h₁f, h₁g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : f x = 0
h₁g : g x = 0
⊢ f x = g x
have neg : 0 = g x
Tactic: rw [h₁f, h₁g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : f x = 0
h₁g : g x = 0
neg : 0 = g x
⊢ f x = g x
have neg₁ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [h₁f, h₁g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
⊢ MeromorphicNFAt f x ↔ MeromorphicNFAt g x
have mp : MeromorphicNFAt f x → MeromorphicNFAt g x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
mp : MeromorphicNFAt f x → MeromorphicNFAt g x
⊢ MeromorphicNFAt f x ↔ MeromorphicNFAt g x
have mpr : MeromorphicNFAt g x → MeromorphicNFAt f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicNFAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
⊢ MeromorphicNFAt (g • f) x
have inl : ∀ (h₁f : f =ᶠ[𝓝 x] 0), MeromorphicNFAt (g • f) x
Tactic: rcases hf with h₁f | ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicNFAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
inl : ∀ (h₁f : f =ᶠ[𝓝 x] 0), MeromorphicNFAt (g • f) x
⊢ MeromorphicNFAt (g • f) x
have inr : ∀ (n : ℤ) (g_f : 𝕜 → E) (h₁g_f : AnalyticAt 𝕜 g_f x) (h₂g_f : g_f x ≠ 0)
  (h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f), MeromorphicNFAt (g • f) x
Tactic: rcases hf with h₁f | ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₁f : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (g • f) x
have inl : g • f =ᶠ[𝓝 x] 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₁f : f =ᶠ[𝓝 x] 0
⊢ g • f =ᶠ[𝓝 x] 0
have h : ∀ (a : 𝕜), f a = 0 a → (g • f) a = 0 a
Tactic: filter_upwards [h₁f]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
⊢ MeromorphicNFAt (g • f) x
have inr : ∃ (n : ℤ) (g_1 : 𝕜 → E),
  AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_1
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
⊢ ∃ (n : ℤ) (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_1
have right : (g • g_f) x ≠ 0 ∧ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f
Tactic: use n, g • g_f, h₁g.smul h₁g_f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
⊢ (g • g_f) x ≠ 0 ∧ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f
have right : (g • g_f) x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
right : (g • g_f) x ≠ 0
⊢ (g • g_f) x ≠ 0 ∧ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f
have right₁ : g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
⊢ g • f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f
have h : ∀ (a : 𝕜),
  f a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f) a →
    (g • f) a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f) a
Tactic: filter_upwards [h₃g_f]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
y : 𝕜
hy : f y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f) y
⊢ (g • f) y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g • g_f) y
have h : g y • (y - x) ^ n • g_f y = (y - x) ^ n • g y • g_f y
Tactic: simp only [Pi.smul_apply', hy, Pi.pow_apply]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f
y : 𝕜
hy : f y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g_f) y
⊢ g y • (y - x) ^ n • g_f y = (y - x) ^ n • g y • g_f y
have h : (y - x) ^ n • g y • g_f y = (y - x) ^ n • g y • g_f y
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
⊢ f =ᶠ[𝓝 x] g⁻¹ • g • f
have h : ∀ a ∈ g ⁻¹' {0}ᶜ, f a = (g⁻¹ • g • f) a
Tactic: filter_upwards [h₁g.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.mpr h₂g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
y : 𝕜
hy : y ∈ g ⁻¹' {0}ᶜ
⊢ f y = (g⁻¹ • g • f) y
have hy₁ : ¬g y = 0
Tactic: rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage,
        Set.mem_singleton_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
⊢ MeromorphicNFAt f x
have this : f =ᶠ[𝓝 x] g⁻¹ • g • f
Tactic: have : f =ᶠ[𝓝 x] g⁻¹ • g • f := by
      filter_upwards [h₁g.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.mpr h₂g)]
      intro y hy
      rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage,
        Set.mem_singleton_iff] at hy
      simp [hy]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
this : f =ᶠ[𝓝 x] g⁻¹ • g • f
⊢ MeromorphicNFAt f x
have rw : MeromorphicNFAt (g⁻¹ • g • f) x
Tactic: rw [meromorphicNFAt_congr this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
⊢ MeromorphicNFAt (f * g) x ↔ MeromorphicNFAt f x
have rw : MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x
Tactic: rw [mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
τ : ι
h₁τ : τ ∈ s
h₂τ : τ ∉ {σ ∈ s | f σ x = 0}
⊢ AnalyticAt 𝕜 (f τ) x
have rw : 0 ≤ meromorphicOrderAt (f τ) x
Tactic: rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
τ : ι
h₁τ : τ ∈ s
h₂τ : τ ∉ {σ ∈ s | f σ x = 0}
⊢ 0 ≤ meromorphicOrderAt (f τ) x
have apply : f τ x ≠ 0
Tactic: apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
Tactic: have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have pos : ∀ (h₄f : {σ ∈ s | f σ x = 0} = ∅), MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
Tactic: by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
pos : ∀ (h₄f : {σ ∈ s | f σ x = 0} = ∅), MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg : ∀ (h₄f : ¬{σ ∈ s | f σ x = 0} = ∅), MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
Tactic: by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
h₄f : ¬{σ ∈ s | f σ x = 0} = ∅
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have h₄f₁ : ¬∀ ⦃x_1 : ι⦄, x_1 ∈ s → ¬f x_1 x = 0
Tactic: rw [Finset.filter_eq_empty_iff] at h₄f
Cleared hypotheses: h₄f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
h₄f : ¬∀ ⦃x_1 : ι⦄, x_1 ∈ s → ¬f x_1 x = 0
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have h₄f₁ : ∃ x_1 ∈ s, f x_1 x = 0
Tactic: push Not at h₄f
Cleared hypotheses: h₄f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
h₄f : ∃ x_1 ∈ s, f x_1 x = 0
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg : ∀ (τ : ι) (h₁τ : τ ∈ s) (h₂τ : f τ x = 0), MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
Tactic: obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
Cleared hypotheses: h₄f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
μ : ι
hμ : μ ∈ s.erase τ
this : f μ x = 0
⊢ False
have this₁ : τ = μ
Tactic: have : τ = μ := h₂f (by aesop) (by aesop)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have this : ∀ {μ : ι} (hμ : μ ∈ s.erase τ), f μ x ≠ 0
Tactic: have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι} (hμ : μ ∈ s.erase τ), f μ x ≠ 0
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg : MeromorphicNFAt (f τ) x
Tactic: rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι} (hμ : μ ∈ s.erase τ), f μ x ≠ 0
neg : MeromorphicNFAt (f τ) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₁ : AnalyticAt 𝕜 (F := 𝕜) (∏ x ∈ s.erase τ, f x) x
Tactic: rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
this : ∀ {μ : ι} (hμ : μ ∈ s.erase τ), f μ x ≠ 0
neg : MeromorphicNFAt (f τ) x
neg₁ : AnalyticAt 𝕜 (F := 𝕜) (∏ x ∈ s.erase τ, f x) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₂ : Ne.{u_1 + 1} (α := 𝕜) ((∏ x ∈ s.erase τ, f x) x) 0
Tactic: rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have have : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
Tactic: classical
  have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
  by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
  · exact (Finset.analyticAt_prod _ (fun σ hσ ↦ h₃f hσ (by aesop))).meromorphicNFAt
  rw [Finset.filter_eq_empty_iff] at h₄f
  push Not at h₄f
  obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
  have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
  rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
  · apply h₁f τ h₁τ
  · apply Finset.analyticAt_prod _ (fun μ hμ ↦ h₃f (Finset.mem_of_mem_erase hμ) (by aesop))
  · rw [Finset.prod_apply, Finset.prod_ne_zero_iff]
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
have : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have have₁ : ∀ (h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x),
  MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
Tactic: classical
  have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
  by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
  · exact (Finset.analyticAt_prod _ (fun σ hσ ↦ h₃f hσ (by aesop))).meromorphicNFAt
  rw [Finset.filter_eq_empty_iff] at h₄f
  push Not at h₄f
  obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
  have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
  rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
  · apply h₁f τ h₁τ
  · apply Finset.analyticAt_prod _ (fun μ hμ ↦ h₃f (Finset.mem_of_mem_erase hμ) (by aesop))
  · rw [Finset.prod_apply, Finset.prod_ne_zero_iff]
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
have : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
have₁ :
  ∀ (h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x),
    MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have₂ : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x
have₃ have₄ :
  ∀ (h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x),
    MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have pos : ∀ (h₃f : ∀ {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}), AnalyticAt 𝕜 (f τ) x) (h₄f : {σ ∈ s | f σ x = 0} = ∅),
  MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
Tactic: classical
  have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
  by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
  · exact (Finset.analyticAt_prod _ (fun σ hσ ↦ h₃f hσ (by aesop))).meromorphicNFAt
  rw [Finset.filter_eq_empty_iff] at h₄f
  push Not at h₄f
  obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
  have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
  rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
  · apply h₁f τ h₁τ
  · apply Finset.analyticAt_prod _ (fun μ hμ ↦ h₃f (Finset.mem_of_mem_erase hμ) (by aesop))
  · rw [Finset.prod_apply, Finset.prod_ne_zero_iff]
    aesop