awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Basic
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
hg : MeromorphicAt g x
rcases : ∀ (m : ℕ) (hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f • g) x
⊢ MeromorphicAt (f • g) x

Tactic:
rcases hf with ⟨m, hf⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
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
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
rcases :
  ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f • g) x
⊢ MeromorphicAt (f • g) x

Tactic:
rcases hg with ⟨n, hg⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt (f • g) x

Tactic:
⟨m + n, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f • g) z) x
⊢ MeromorphicAt (f • g) x

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) fun (z : 𝕜) ↦ (z - x) ^ n • g z)
    x

Tactic:
hf.smul hg

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
h :
  ∀ (z : 𝕜),
    (z - x) ^ (m + n) • (f • g) z =
      HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f • g) z) x

Tactic:
convert! hf.smul hg using 2 with z

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
z : 𝕜
h : (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m * f z) • (z - x) ^ n • g z
⊢ (z - x) ^ (m + n) • (f • g) z =
    HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
z : 𝕜
⊢ (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m * f z) • (z - x) ^ n • g z

Tactic:
module
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
rcases :
  ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f * g) x
⊢ MeromorphicAt (f * g) x

Tactic:
rcases hf with ⟨m, hf⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hg : MeromorphicAt g x
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
rcases :
  ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f * g) x
⊢ MeromorphicAt (f * g) x

Tactic:
rcases hg with ⟨n, hg⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt (f * g) x

Tactic:
⟨m + n, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
refine : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f * g) z) x
⊢ MeromorphicAt (f * g) x

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (HMul.hMul (α := 𝕜 → 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) fun (z : 𝕜) ↦ (z - x) ^ n • g z) x

Tactic:
hf.mul hg

Premises used: AnalyticAt.mul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
h :
  ∀ (z : 𝕜),
    (z - x) ^ (m + n) • (f * g) z =
      HMul.hMul (α := 𝕜 → 𝕜') (β := 𝕜 → 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f * g) z) x

Tactic:
convert! hf.mul hg using 2 with z

Premises used: AnalyticAt.mul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
z : 𝕜
h : (z - x) ^ (m + n) • (f z * g z) = (z - x) ^ n • (z - x) ^ m • (f z * g z)
⊢ (z - x) ^ (m + n) • (f * g) z =
    HMul.hMul (α := 𝕜 → 𝕜') (β := 𝕜 → 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
z : 𝕜
⊢ (z - x) ^ (m + n) • (f z * g z) = (z - x) ^ n • (z - x) ^ m • (f z * g z)

Tactic:
module
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x
empty : MeromorphicAt.{u_1, u_2} (E := 𝕜') 1 x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, F i) x

Tactic:
rw [Finset.prod_empty]

Premises used: Finset.prod_empty
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') 1 x

Tactic:
apply MeromorphicAt.const

Premises used: MeromorphicAt.const
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s_1 : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (hf : ∀ σ ∈ s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
hf : ∀ σ ∈ Insert.insert a s, MeromorphicAt (F σ) x
insert : MeromorphicAt (F a * ∏ x ∈ s, F x) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ Insert.insert a s, F i) x

Tactic:
rw [Finset.prod_insert ha]

Premises used: Finset.prod_insert
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s_1 : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (hf : ∀ σ ∈ s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
hf : ∀ σ ∈ insert a s, MeromorphicAt (F σ) x
⊢ MeromorphicAt (F a * ∏ x ∈ s, F x) x

Tactic:
apply (hf a (Finset.mem_insert_self a s)).mul
      (hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))

Premises used: MeromorphicAt.mul, Finset.mem_insert_self, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ s, MeromorphicAt (F σ) x
empty :
  ∀ (hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x),
    MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, F i) x
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (hs : ∀ (hf : ∀ σ ∈ s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x)
    (hf : ∀ σ ∈ Insert.insert a s, MeromorphicAt (F σ) x),
    MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ Insert.insert a s, F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x

Tactic:
induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty]
    apply MeromorphicAt.const
  | insert a s ha hs =>
    rw [Finset.prod_insert ha]
    apply (hf a (Finset.mem_insert_self a s)).mul
      (hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))

Premises used: Finset.prod_empty, MeromorphicAt.const, Insert.insert
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ s, MeromorphicAt (F σ) x
empty :
  ∀ (hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x),
    MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, F i) x
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (hs : ∀ (hf : ∀ σ ∈ s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x)
    (hf : ∀ σ ∈ Insert.insert a s, MeromorphicAt (F σ) x),
    MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ Insert.insert a s, F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty]
    apply MeromorphicAt.const
  | insert a s ha hs =>
    rw [Finset.prod_insert ha]
    apply (hf a (Finset.mem_insert_self a s)).mul
      (hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))

Premises used: Finset.prod_empty, MeromorphicAt.const, Insert.insert
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x

Tactic:
prod h (s := s)

Premises used: MeromorphicAt.prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (F σ) x
h₁ : ∀ (x : 𝕜), Eq.{u_2 + 1} (α := 𝕜') (∏ n ∈ s, F n x) ((∏ i ∈ s, F i) x)
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (fun (z : 𝕜) ↦ ∏ n ∈ s, F n z) x

Tactic:
convert! prod h (s := s)

Premises used: MeromorphicAt.prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (F σ) x
x_1 : 𝕜
⊢ Eq.{u_2 + 1} (α := 𝕜') (∏ n ∈ s, F n x_1) ((∏ i ∈ s, F i) x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
pos : ∀ (h₂f : Function.HasFiniteMulSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
neg : ∀ (h₂f : ¬Function.HasFiniteMulSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x

Tactic:
by_cases h₂f : Function.HasFiniteMulSupport F

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteMulSupport F
⊢ ∀ σ ∈ Finite.toFinset (s := Function.mulSupport F) h₂f, MeromorphicAt (F σ) x

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteMulSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x

Tactic:
simpa [finprod_eq_prod F h₂f] using prod (by aesop)

Premises used: MeromorphicAt.prod, finprod_eq_prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteMulSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x

Tactic:
finprod_of_not_hasFiniteMulSupport h₂f ▸ const (1 : 𝕜') x

Premises used: MeromorphicAt.const, Eq.rec, finprod_of_not_hasFiniteMulSupport, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteMulSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x

Tactic:
exact finprod_of_not_hasFiniteMulSupport h₂f ▸ const (1 : 𝕜') x
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x
empty : MeromorphicAt.{u_1, u_3} (E := E) 0 x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, G n) x

Tactic:
simp only [Finset.sum_empty]

Premises used: Finset.sum_empty
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) 0 x

Tactic:
analyticAt_const.meromorphicAt

Premises used: analyticAt_const, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) 0 x

Tactic:
exact analyticAt_const.meromorphicAt

Premises used: analyticAt_const, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s_1 : Finset ι
G : ι → 𝕜 → E
x : 𝕜
σ : ι
s : Finset ι
hσ : σ ∉ s
hind : ∀ (h : ∀ σ ∈ s, MeromorphicAt (G σ) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x
h : ∀ σ_1 ∈ Insert.insert σ s, MeromorphicAt (G σ_1) x
insert : MeromorphicAt (G σ + ∑ x ∈ s, G x) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ Insert.insert σ s, G n) x

Tactic:
rw [Finset.sum_insert hσ]

Premises used: Finset.sum_insert
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s_1 : Finset ι
G : ι → 𝕜 → E
x : 𝕜
σ : ι
s : Finset ι
hσ : σ ∉ s
hind : ∀ (h : ∀ σ ∈ s, MeromorphicAt (G σ) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x
h : ∀ σ_1 ∈ insert σ s, MeromorphicAt (G σ_1) x
⊢ MeromorphicAt (G σ + ∑ x ∈ s, G x) x

Tactic:
apply (h σ (Finset.mem_insert_self σ s)).add
      (hind (fun τ hτ ↦ h τ (Finset.mem_insert_of_mem hτ)))

Premises used: Finset.mem_insert_self, MeromorphicAt.add, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
empty :
  ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x),
    MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, G n) x
insert :
  ∀ (σ : ι) (s : Finset ι) (hσ : σ ∉ s)
    (hind : ∀ (h : ∀ σ ∈ s, MeromorphicAt (G σ) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x)
    (h : ∀ σ_1 ∈ Insert.insert σ s, MeromorphicAt (G σ_1) x),
    MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ Insert.insert σ s, G n) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticAt_const.meromorphicAt
  | insert σ s hσ hind =>
    rw [Finset.sum_insert hσ]
    apply (h σ (Finset.mem_insert_self σ s)).add
      (hind (fun τ hτ ↦ h τ (Finset.mem_insert_of_mem hτ)))

Premises used: Insert.insert, analyticAt_const, Finset.sum_empty, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
empty :
  ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x),
    MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, G n) x
insert :
  ∀ (σ : ι) (s : Finset ι) (hσ : σ ∉ s)
    (hind : ∀ (h : ∀ σ ∈ s, MeromorphicAt (G σ) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x)
    (h : ∀ σ_1 ∈ Insert.insert σ s, MeromorphicAt (G σ_1) x),
    MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ Insert.insert σ s, G n) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticAt_const.meromorphicAt
  | insert σ s hσ hind =>
    rw [Finset.sum_insert hσ]
    apply (h σ (Finset.mem_insert_self σ s)).add
      (hind (fun τ hτ ↦ h τ (Finset.mem_insert_of_mem hτ)))

Premises used: Insert.insert, analyticAt_const, Finset.sum_empty, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x

Tactic:
sum h (s := s)

Premises used: MeromorphicAt.sum
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
h₁ : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := E) (∑ n ∈ s, G n x) ((∑ n ∈ s, G n) x)
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ∑ n ∈ s, G n z) x

Tactic:
convert! sum h (s := s)

Premises used: MeromorphicAt.sum
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := E) (∑ n ∈ s, G n x_1) ((∑ n ∈ s, G n) x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
pos : ∀ (h₂f : Function.HasFiniteSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
neg : ∀ (h₂f : ¬Function.HasFiniteSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x

Tactic:
by_cases h₂f : Function.HasFiniteSupport F

Premises used: Function.HasFiniteSupport
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteSupport F
⊢ ∀ σ ∈ Finite.toFinset (s := Function.support F) h₂f, MeromorphicAt (F σ) x

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x

Tactic:
simpa [finsum_eq_sum F h₂f] using sum (by aesop)

Premises used: finsum_eq_sum, MeromorphicAt.sum
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x

Tactic:
finsum_of_not_hasFiniteSupport h₂f ▸ const (0 : 𝕜') x

Premises used: MeromorphicAt.const, Eq.rec, finsum_of_not_hasFiniteSupport, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteSupport F
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x

Tactic:
exact finsum_of_not_hasFiniteSupport h₂f ▸ const (0 : 𝕜') x