awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x
have contrapose : ∀ (hf₁ : MeromorphicAt (f₁ + f₂) x), MeromorphicAt f₁ x
Tactic: contrapose hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have this : ¬MeromorphicAt (f₁ + f₂) x
Tactic: have : ¬ (MeromorphicAt (f₁ + f₂) x) := by
      contrapose hf₁
      simpa using hf₁.sub hf₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have neg : ∀ (h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have pos : f₁ + f₂ =ᶠ[𝓝[≠] x] f₁
Tactic: rw [meromorphicOrderAt_congr]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₁
have h₁ : ∀ (a : 𝕜), f₂ a = 0 → (f₁ + f₂) a = f₁ a
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have neg : ∀ (n₂ : ℤ) (hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x)
  (meromorphicOrderAt_add_eq_left_of_lt :
    ∀ (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
      meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x)
  (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Tactic: lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂
Cleared hypotheses: h, h₁f₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
have neg : ∀ (n₁ : ℤ) (hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x)
  (meromorphicOrderAt_add_eq_left_of_lt :
    ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
      meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ))
  (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)), meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
Tactic: lift meromorphicOrderAt f₁ x to ℤ using h.ne_top with n₁ hn₁
Cleared hypotheses: meromorphicOrderAt_add_eq_left_of_lt, h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
have neg : ∀ (g₁ : 𝕜 → E) (h₁g₁ : AnalyticAt 𝕜 g₁ x) (h₂g₁ : g₁ x ≠ 0) (h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z),
  meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
Tactic: obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
have neg : ∀ (g₂ : 𝕜 → E) (h₁g₂ : AnalyticAt 𝕜 g₂ x) (h₂g₂ : g₂ x ≠ 0) (h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z),
  meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
Tactic: obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
have neg : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z
Tactic: rw [meromorphicOrderAt_eq_int_iff (hf₁.add hf₂)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z
have neg : AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x
Tactic: refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
neg : AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z
have neg₁ : (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x ≠ 0
Tactic: refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
neg : AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x
neg₁ : (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x ≠ 0
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z
have neg₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
  (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) z
Tactic: refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x
have apply : AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁)) x
Tactic: apply h₁g₁.add (AnalyticAt.smul _ h₁g₂)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) z
have h₁ : ∀ (a : 𝕜),
  f₁ a = (a - x) ^ n₁ • g₁ a →
    f₂ a = (a - x) ^ n₂ • g₂ a →
      Membership.mem (γ := Set 𝕜) {x}ᶜ a →
        (f₁ + f₂) a = (a - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) a
Tactic: filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x
have rw : meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₂ x
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
have inl : ∀ (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x),
  meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
Tactic: rcases lt_or_lt_iff_ne.mpr h with h | h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
inl :
  ∀ (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x),
    meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
have inr : ∀ (h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x),
  meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
Tactic: rcases lt_or_lt_iff_ne.mpr h with h | h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) ↔
    ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mp : (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) →
  ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
mp :
  (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) →
    ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) ↔
    ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mpr : (∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) →
  ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have this : PreconnectedSpace.{u_1} (↑U : Type u_1)
Tactic: have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mp : ∀ (h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅)
  (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: rcases isClopen_iff.1 hf.isClopen_setOf_meromorphicOrderAt_eq_top with h | h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
mp :
  ∀ (h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅)
    (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mp₁ : ∀ (h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ)
  (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: rcases isClopen_iff.1 hf.isClopen_setOf_meromorphicOrderAt_eq_top with h | h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
⊢ meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have this₁ : u ∉ ∅
Tactic: have : u ∉ (∅ : Set U) := by exact fun a => a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
this : u ∉ ∅
⊢ meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have this₁ : u ∉ {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤}
Tactic: rw [← h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mp : ∀ (u : (↑U : Type u_1)) (hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) (u : (↑U : Type u_1)),
  meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: obtain ⟨u, hU⟩ := h₂f
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU_1 : IsConnected U
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have this₁ : Membership.mem (γ := Set (↑U : Type u_1)) univ u
Tactic: have : u ∈ univ := by trivial
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU_1 : IsConnected U
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : Membership.mem (γ := Set (↑U : Type u_1)) univ u
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have this₁ : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} u
Tactic: rw [← h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have mpr : ∀ (v : 𝕜) (hv : v ∈ U), ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: obtain ⟨v, hv⟩ := hU.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
v : 𝕜
hv : v ∈ U
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have w : (↑U : Type u_1)
Tactic: use ⟨v, hv⟩, h₂f ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
v : 𝕜
hv : v ∈ U
w : (↑U : Type u_1)
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have h : meromorphicOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) v hv) : 𝕜) ≠ ⊤
Tactic: use ⟨v, hv⟩, h₂f ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
y : 𝕜
hU : IsPreconnected U
h₁x : x ∈ U
hy : y ∈ U
h₂x : meromorphicOrderAt f x ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have w : (↑U : Type u_1)
Tactic: use ⟨x, h₁x⟩