awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg : ∀ (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
-- 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
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
neg neg₁ :
  ∀ (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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₂ : ∀ (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
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
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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₃ : ∀ (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
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
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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₄ : ∀ (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
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
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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (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
neg₄ :
  ∀ (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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₅ : ∀ (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
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
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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (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
neg₄ :
  ∀ (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
neg₅ :
  ∀ (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
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ s, f i) x
have neg₆ : ∀ (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 (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}
⊢ MeromorphicNFAt (E := 𝕜) (fun (a : 𝕜) ↦ ∏ i ∈ s, f i a) x
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
Tactic: convert! meromorphicNFAt_prod h₁f h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
have pos : ∀ (h₃f : Function.HasFiniteMulSupport f), MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
Tactic: by_cases h₃f : Function.HasFiniteMulSupport f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
pos : ∀ (h₃f : Function.HasFiniteMulSupport f), MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
have neg : ∀ (h₃f : ¬Function.HasFiniteMulSupport f), MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
Tactic: by_cases h₃f : Function.HasFiniteMulSupport f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
have pos : MeromorphicNFAt (E := 𝕜) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f, f i) x
Tactic: simp_rw [finprod_eq_prod f h₃f]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
⊢ MeromorphicNFAt (f ^ n) x
have pos : ∀ (hn : n = 0), MeromorphicNFAt (f ^ n) x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
pos : ∀ (hn : n = 0), MeromorphicNFAt (f ^ n) x
⊢ MeromorphicNFAt (f ^ n) x
have neg : ∀ (hn : ¬n = 0), MeromorphicNFAt (f ^ n) x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
⊢ MeromorphicNFAt (f ^ n) x
have pos : MeromorphicNFAt (E := 𝕜) 1 x
Tactic: simp_all only [zpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
⊢ MeromorphicNFAt (E := 𝕜) 1 x
have pos : AnalyticAt 𝕜 (F := 𝕜) 1 x
Tactic: apply AnalyticAt.meromorphicNFAt
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : ¬n = 0
⊢ MeromorphicNFAt (f ^ n) x
have neg : ∀ (hf : f =ᶠ[𝓝 x] 0), MeromorphicNFAt (f ^ n) x
Tactic: rcases hf with hf | hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : ¬n = 0
neg : ∀ (hf : f =ᶠ[𝓝 x] 0), MeromorphicNFAt (f ^ n) x
⊢ MeromorphicNFAt (f ^ n) x
have neg₁ : ∀
  (hf :
    ∃ (n : ℤ) (g : 𝕜 → 𝕜),
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g),
  MeromorphicNFAt (f ^ n) x
Tactic: rcases hf with hf | hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (f ^ n) x
have neg : f ^ n =ᶠ[𝓝 x] 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ f ^ n =ᶠ[𝓝 x] 0
have h : ∀ (z : 𝕜) (hz : f z = 0 z), (f ^ n) z = 0 z
Tactic: filter_upwards [hf] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf :
  ∃ (n : ℤ) (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt (f ^ n) x
have neg : ∀ (m : ℤ) (g : 𝕜 → 𝕜) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
  (h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g), MeromorphicNFAt (f ^ n) x
Tactic: obtain ⟨m, g, h₁g, h₂g, h₃g⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ MeromorphicNFAt (f ^ n) x
have neg : ∃ (n_1 : ℤ) (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n_1 • g
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ ∃ (n_1 : ℤ) (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n_1 • g
have right : (g ^ n) x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
Tactic: use n * m, g ^ n, h₁g.zpow h₂g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ (g ^ n) x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
have right : (g ^ n) x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
right : (g ^ n) x ≠ 0
⊢ (g ^ n) x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
have right₁ : f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ (g ^ n) x ≠ 0
have right : g x ^ n ≠ 0
Tactic: rw [Pi.pow_apply]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
have h : ∀ (z : 𝕜) (hz : f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g) z),
  (f ^ n) z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n) z
Tactic: filter_upwards [h₃g] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicNFAt f x
⊢ MeromorphicNFAt f⁻¹ x
have inl : ∀ (h : f =ᶠ[𝓝 x] 0), MeromorphicNFAt f⁻¹ x
Tactic: rcases hf with h | ⟨n, g, h₁, h₂, h₃⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicNFAt f x
inl : ∀ (h : f =ᶠ[𝓝 x] 0), MeromorphicNFAt f⁻¹ x
⊢ MeromorphicNFAt f⁻¹ x
have inr : ∀ (n : ℤ) (g : 𝕜 → 𝕜) (h₁ : AnalyticAt 𝕜 g x) (h₂ : g x ≠ 0)
  (h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g), MeromorphicNFAt f⁻¹ x
Tactic: rcases hf with h | ⟨n, g, h₁, h₂, h₃⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt f⁻¹ x
have inl : f⁻¹ =ᶠ[𝓝 x] 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ f⁻¹ =ᶠ[𝓝 x] 0
have h₁ : ∀ (x : 𝕜) (hx : f x = 0 x), f⁻¹ x = 0 x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt f⁻¹ x
have inr : ∃ (n : ℤ) (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f⁻¹ =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
Tactic: right