awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z
hf'' : f z = (z - z₀) ^ n • h z
h₁ : g z = ((z - z₀) ^ n * ((z - z₀) ^ m)⁻¹) • h z
⊢ g z = (z - z₀) ^ (n - m) • h z
have h₂ : ((z - z₀) ^ n *
      ((z - z₀) ^
          sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
    h z =
  ((z - z₀) ^ n * ((z - z₀) ^ m)⁻¹) • h z
Tactic: rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by lia), ← hf']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
have pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = analyticOrderAt g z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
have neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = analyticOrderAt g z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
have pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt g z₀
Tactic: refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt g z₀
have pos : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
Tactic: simp only [natCast_le_analyticOrderAt, hf, hf.congr hfg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
have pos : ∀ (x : 𝕜 → E), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • x z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • x z
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
have neg : 0 = analyticOrderAt g z₀
Tactic: rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt fun hg ↦ hf <| hg.congr hfg.symm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : ¬AnalyticAt 𝕜 f z₀
neg : 0 = analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
have neg₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt fun hg ↦ hf <| hg.congr hfg.symm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
have pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
have neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
have pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ analyticOrderAt (-f) z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt f z₀
Tactic: refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ (↑n : ℕ∞) ≤ analyticOrderAt (-f) z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt f z₀
have pos : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (-f) z = (z - z₀) ^ n • g z) ↔
  ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: simp only [natCast_le_analyticOrderAt, hf, hf.neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
have neg : analyticOrderAt (-f) z₀ = 0
Tactic: rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : ¬AnalyticAt 𝕜 f z₀
neg : analyticOrderAt (-f) z₀ = 0
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
have neg₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
have pos : ∀ (hf : AnalyticAt 𝕜 f z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
have neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
have pos : ∀ (hg : AnalyticAt 𝕜 g z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
Tactic: by_cases hg : AnalyticAt 𝕜 g z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos : ∀ (hg : AnalyticAt 𝕜 g z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
have neg : ∀ (hg : ¬AnalyticAt 𝕜 g z₀), min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
Tactic: by_cases hg : AnalyticAt 𝕜 g z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
have pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) → (↑n : ℕ∞) ≤ analyticOrderAt (f + g) z₀
Tactic: refine ENat.forall_natCast_le_iff_le.mp fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
n : ℕ
⊢ (↑n : ℕ∞) ≤ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) → (↑n : ℕ∞) ≤ analyticOrderAt (f + g) z₀
have pos : ((∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z) →
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • g_1 z
Tactic: simp only [le_min_iff, natCast_le_analyticOrderAt, hf, hg, hf.add hg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
n : ℕ
⊢ ((∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
      ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z) →
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • g_1 z
have pos : ((∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z) →
  ∀ (F : 𝕜 → E) (hF : AnalyticAt 𝕜 F z₀) (hF' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • F z) (G : 𝕜 → E)
    (hG : AnalyticAt 𝕜 G z₀) (hG' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • G z),
    ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • (F + G) z
Tactic: refine fun ⟨⟨F, hF, hF'⟩, ⟨G, hG, hG'⟩⟩ ↦ ⟨F + G, hF.add hG, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
n : ℕ
h :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
F : 𝕜 → E
hF : AnalyticAt 𝕜 F z₀
hF' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • F z
G : 𝕜 → E
hG : AnalyticAt 𝕜 G z₀
hG' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • G z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • (F + G) z
have h : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x : 𝕜 |
      Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ f z = (z - z₀) ^ n • F z) x} x →
        Membership.mem (γ := Set 𝕜)
          {x : 𝕜 |
            Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ g z = (z - z₀) ^ n • G z) x} x →
              Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ (f + g) z = (z - z₀) ^ n • (F + G) z) x} x}
          x}
    a
Tactic: filter_upwards [hF', hG'] with z using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
n : ℕ
h_1 :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ∧
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
F : 𝕜 → E
hF : AnalyticAt 𝕜 F z₀
hF' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • F z
G : 𝕜 → E
hG : AnalyticAt 𝕜 G z₀
hG' : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • G z
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ f z = (z - z₀) ^ n • F z) x} x →
          Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ g z = (z - z₀) ^ n • G z) x} x →
                Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ (f + g) z = (z - z₀) ^ n • (F + G) z) x} x}
            x}
      a
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • (F + G) z
have h₁ : ∀ (a : 𝕜), f a = (a - z₀) ^ n • F a → g a = (a - z₀) ^ n • G a → (f + g) a = (a - z₀) ^ n • (F + G) a
Tactic: filter_upwards [hF', hG'] with z using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀
have rw : analyticOrderAt (g + f) z₀ = analyticOrderAt g z₀
Tactic: rw [add_comm, analyticOrderAt_add_eq_left_of_lt hgf]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
rw : analyticOrderAt (g + f) z₀ = analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀
have rw₁ : analyticOrderAt g z₀ = analyticOrderAt g z₀
Tactic: rw [add_comm, analyticOrderAt_add_eq_left_of_lt hgf]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
have inl : ∀ (hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀),
  analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
Tactic: obtain hfg | hgf := hfg.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
inl :
  ∀ (hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀),
    analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
have inr : ∀ (hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀),
  analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
Tactic: obtain hfg | hgf := hfg.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : analyticOrderAt f z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = ⊤
have rw : ∀ (hf : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t),
  ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Tactic: rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
⊢ ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
have obtain : ∀ (t : Set 𝕜) (h₁t : ∀ y ∈ t, f y = 0) (h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
  (h₃t : z₀ ∈ t),
  ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Tactic: obtain ⟨t, h₁t, h₂t, h₃t⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hg : analyticOrderAt g z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = ⊤
have rw : ∀ (hg : ∃ (t : Set 𝕜), (∀ y ∈ t, g y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t),
  ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Tactic: rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hg : ∃ (t : Set 𝕜), (∀ y ∈ t, g y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
⊢ ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
have obtain : ∀ (t : Set 𝕜) (h₁t : ∀ y ∈ t, g y = 0) (h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
  (h₃t : z₀ ∈ t),
  ∃ (t : Set 𝕜), (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Tactic: obtain ⟨t, h₁t, h₂t, h₃t⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have pos : ∀ (hf' : analyticOrderAt f z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: by_cases hf' : analyticOrderAt f z₀ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
pos : ∀ (hf' : analyticOrderAt f z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have neg : ∀ (hf' : ¬analyticOrderAt f z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: by_cases hf' : analyticOrderAt f z₀ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have pos : ∀ (hg' : analyticOrderAt g z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: by_cases hg' : analyticOrderAt g z₀ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
pos : ∀ (hg' : analyticOrderAt g z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have neg : ∀ (hg' : ¬analyticOrderAt g z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: by_cases hg' : analyticOrderAt g z₀ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have neg : ∀ (f' : 𝕜 → 𝕜) (h₁f' : AnalyticAt 𝕜 f' z₀) (h₂f' : f' z₀ ≠ 0)
  (h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z),
  analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: obtain ⟨f', h₁f', h₂f', h₃f'⟩ := hf.analyticOrderAt_ne_top.1 hf'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have neg : ∀ (g' : 𝕜 → E) (h₁g' : AnalyticAt 𝕜 g' z₀) (h₂g' : g' z₀ ≠ 0)
  (h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z),
  analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
Tactic: obtain ⟨g', h₁g', h₂g', h₃g'⟩ := hg.analyticOrderAt_ne_top.1 hg'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
have neg : ∃ (g_1 : 𝕜 → E),
  AnalyticAt 𝕜 g_1 z₀ ∧
    g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • g_1 z
Tactic: rw [← Nat.cast_analyticOrderNatAt hf', ← Nat.cast_analyticOrderNatAt hg', ← ENat.coe_add,
      (hf.smul hg).analyticOrderAt_eq_natCast]