-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
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
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), AnalyticAt 𝕜 (F := 𝕜) (∏ x ∈ s.erase τ, f x) 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),
    Ne.{u_1 + 1} (α := 𝕜) ((∏ x ∈ s.erase τ, f x) x) 0
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), AnalyticAt 𝕜 (F := 𝕜) (∏ x ∈ s.erase τ, f x) x
neg₁₀ 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),
    Ne.{u_1 + 1} (α := 𝕜) ((∏ x ∈ s.erase τ, f x) 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

Premises used: Finset.prod_apply, meromorphicNFAt_mul_iff_left, Finset.prod_ne_zero_iff, Finset.filter_eq_empty_iff, Not