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
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (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
simp_rw :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    ((z - x) ^ (max m n - m) * (z - x) ^ m) • f z + ((z - x) ^ (max m n - n) * (z - x) ^ n) • g z
simp_rw₁ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m + m) • f z + (z - x) ^ (max m n - n + n) • g z
simp_rw₂ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ max m n • f z + (z - x) ^ (max m n - n + n) • g z
simp_rw₃ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ max m n • f z + (z - x) ^ max m n • g z
⊢ Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
have simp_rw₄ : Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f z + g z)) fun (z : 𝕜) ↦
  (z - x) ^ max m n • f z + (z - x) ^ max m n • g z
Tactic: simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]
-- 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
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (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.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) x
have this : Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
  (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
Tactic: have : (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ (max m n - m) •
      ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) := by
    simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]
-- 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
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (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
this :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) x
have rw : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E)
  (fun (z : 𝕜) ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x
Tactic: rw [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
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f • g) x
have rcases : ∀ (m : ℕ) (hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f • 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
hg : MeromorphicAt g x
m : ℕ
hf : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ MeromorphicAt (f • g) x
have rcases : ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f • g) x
Tactic: rcases hg with ⟨n, hg⟩
Cleared hypotheses: hg
-- 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
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
have refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f • g) z) x
Tactic: refine ⟨m + n, ?_⟩
-- 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
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.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f • g) z) x
have 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
Tactic: convert! hf.smul hg using 2 with z
-- 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
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 • g) z =
    HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z
have h : (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m * f z) • (z - x) ^ n • g z
Tactic: simp
-- 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 g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f * g) x
have rcases : ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f * 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
𝕜' : 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
⊢ MeromorphicAt (f * g) x
have rcases : ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f * g) x
Tactic: rcases hg with ⟨n, hg⟩
Cleared hypotheses: hg
-- 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 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
have refine : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f * g) z) x
Tactic: refine ⟨m + 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 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.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ (m + n) • (f * g) z) x
have 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
Tactic: convert! hf.mul hg using 2 with z
-- 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 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 * g) z =
    HMul.hMul (α := 𝕜 → 𝕜') (β := 𝕜 → 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z
have h : (z - x) ^ (m + n) • (f z * g z) = (z - x) ^ n • (z - x) ^ m • (f z * g z)
Tactic: simp
-- 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 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, F i) x
have empty : MeromorphicAt.{u_1, u_2} (E := 𝕜') 1 x
Tactic: rw [Finset.prod_empty]
-- 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 𝕜 𝕜'
ι : 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.{u_1, u_2} (E := 𝕜') (∏ i ∈ insert a s, F i) x
have insert : MeromorphicAt (F a * ∏ x ∈ s, F x) x
Tactic: rw [Finset.prod_insert ha]
-- 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 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ s, MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
have empty : ∀ (hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x),
  MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, 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)))
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 𝕜 𝕜'
ι : 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
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
have 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 a s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ insert a 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)))
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 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ s, MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
have empty : ∀ (hf : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (F σ) x),
  MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ ∅, 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)))
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 𝕜 𝕜'
ι : 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
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ s, F i) x
have 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 a s, MeromorphicAt (F σ) x), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ i ∈ insert a 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)))
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 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (F σ) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (fun (z : 𝕜) ↦ ∏ n ∈ s, F n z) x
have h₁ : ∀ (x : 𝕜), Eq.{u_2 + 1} (α := 𝕜') (∏ n ∈ s, F n x) ((∏ i ∈ s, F i) x)
Tactic: convert! prod h (s := s)
-- 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 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
have pos : ∀ (h₂f : Function.HasFiniteMulSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
Tactic: by_cases h₂f : Function.HasFiniteMulSupport F
-- 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 𝕜 𝕜'
ι : 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
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
have neg : ∀ (h₂f : ¬Function.HasFiniteMulSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∏ᶠ (i : ι), F i) x
Tactic: by_cases h₂f : Function.HasFiniteMulSupport F
-- 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
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, G n) x
have empty : MeromorphicAt.{u_1, u_3} (E := E) 0 x
Tactic: simp only [Finset.sum_empty]
-- 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
ι : 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.{u_1, u_3} (E := E) (∑ n ∈ insert σ s, G n) x
have insert : MeromorphicAt (G σ + ∑ x ∈ s, G x) x
Tactic: rw [Finset.sum_insert hσ]
-- 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
ι : 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
have empty : ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x),
  MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, 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τ)))
Cleared hypotheses: h
-- 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
ι : 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
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x
have 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 σ s, MeromorphicAt (G σ_1) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ insert σ 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τ)))
Cleared hypotheses: h
-- 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
ι : 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
have empty : ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (G σ) x),
  MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ ∅, 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τ)))
Cleared hypotheses: h
-- 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
ι : 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
⊢ MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ s, G n) x
have 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 σ s, MeromorphicAt (G σ_1) x), MeromorphicAt.{u_1, u_3} (E := E) (∑ n ∈ insert σ 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τ)))
Cleared hypotheses: h
-- 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
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ∑ n ∈ s, G n z) x
have h₁ : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := E) (∑ n ∈ s, G n x) ((∑ n ∈ s, G n) x)
Tactic: convert! sum h (s := s)
-- 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 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
have pos : ∀ (h₂f : Function.HasFiniteSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
Tactic: by_cases h₂f : Function.HasFiniteSupport F
-- 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 𝕜 𝕜'
ι : 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
⊢ MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
have neg : ∀ (h₂f : ¬Function.HasFiniteSupport F), MeromorphicAt.{u_1, u_2} (E := 𝕜') (∑ᶠ (i : ι), F i) x
Tactic: by_cases h₂f : Function.HasFiniteSupport F
-- 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 : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt (-f) x
have h : -f = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f
Tactic: convert! (MeromorphicAt.const (-1 : 𝕜) x).smul hf using 1
-- 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 : 𝕜 → E
hf : MeromorphicAt f x
⊢ -f = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f
have h : ∀ (z : 𝕜), (-f) z = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f z
Tactic: ext1 z
-- 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
hg : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x
have h : f - g = f + -g
Tactic: convert! hf.add hg.neg using 1
-- 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
hg : MeromorphicAt g x
⊢ f - g = f + -g
have h : ∀ (z : 𝕜), (f - g) z = (f + -g) z
Tactic: ext1 z
-- 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
hg : MeromorphicAt g x
z : 𝕜
⊢ (f - g) z = (f + -g) z
have h : f z - g z = (f + -g) z
Tactic: simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]
-- 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
hg : MeromorphicAt g x
z : 𝕜
h : f z - g z = (f + -g) z
⊢ (f - g) z = (f + -g) z
have h₁ : f z - g z = f z + (-g) z
Tactic: simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]
-- 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
hg : MeromorphicAt g x
z : 𝕜
h : f z - g z = (f + -g) z
h₁ : f z - g z = f z + (-g) z
⊢ (f - g) z = (f + -g) z
have h₂ : f z - g z = f z + -g z
Tactic: simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]