awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Order
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₀
pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ analyticOrderAt (-f) z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Premises used: ENat.eq_of_forall_natCast_le_iff
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
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
⊢ (↑n : ℕ∞) ≤ analyticOrderAt (-f) z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt f z₀

Tactic:
simp only [natCast_le_analyticOrderAt, hf, hf.neg]

Premises used: natCast_le_analyticOrderAt, AnalyticAt.neg
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
⊢ ∀ (a : 𝕜 → E),
    (AnalyticAt 𝕜 a z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (-f) z = (z - z₀) ^ n • a z) ↔
      AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) ((Equiv.neg (𝕜 → E) : (a : 𝕜 → E) → 𝕜 → E) a) z₀ ∧
        ∀ᶠ (z : 𝕜) in 𝓝 z₀,
          f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((Equiv.neg (𝕜 → E) : (a : 𝕜 → E) → 𝕜 → E) a z : E)

Tactic:
simp [neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
⊢ (∃ (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:
exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]

Premises used: Equiv.neg, Equiv.exists_congr
-- Module: Mathlib.Analysis.Analytic.Order
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
neg₁ neg₂ : Eq (α := ℕ∞) 0 0
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]

Premises used: Iff.mpr, analyticAt_neg, Iff.not, analyticOrderAt_of_not_analyticAt
-- Module: Mathlib.Analysis.Analytic.Order
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₀
neg : ∀ (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₀

Tactic:
by_cases hf : AnalyticAt 𝕜 f z₀

Premises used: AnalyticAt
-- Module: Mathlib.Analysis.Analytic.Order
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₀
neg : ∀ (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₀

Tactic:
by_cases hg : AnalyticAt 𝕜 g z₀

Premises used: AnalyticAt
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
ENat.forall_natCast_le_iff_le.mp fun n ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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₀
pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) → (↑n : ℕ∞) ≤ analyticOrderAt (f + g) z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

Tactic:
refine ENat.forall_natCast_le_iff_le.mp fun n ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
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
⊢ (↑n : ℕ∞) ≤ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) → (↑n : ℕ∞) ≤ analyticOrderAt (f + g) z₀

Tactic:
simp only [le_min_iff, natCast_le_analyticOrderAt, hf, hg, hf.add hg]

Premises used: natCast_le_analyticOrderAt, AnalyticAt.add, le_min_iff
-- Module: Mathlib.Analysis.Analytic.Order
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

Tactic:
fun ⟨⟨F, hF, hF'⟩, ⟨G, hG, hG'⟩⟩ ↦ ⟨F + G, hF.add hG, ?_⟩

Premises used: Filter.Eventually, HSub.hSub, Exists, nhds, AnalyticAt.add, And, HPow.hPow, HAdd.hAdd, AnalyticAt, And.intro, Exists.intro, _private.0.le_analyticOrderAt_add.match_1, HSMul.hSMul, Eq
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
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
⊢ ((∃ (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:
refine fun ⟨⟨F, hF, hF'⟩, ⟨G, hG, hG'⟩⟩ ↦ ⟨F + G, hF.add hG, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜
⊢ f z = (z - z₀) ^ n • F z → g z = (z - z₀) ^ n • G z → (f + g) z = (z - z₀) ^ n • (F + G) z

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.Analytic.Order
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
h₁ h₂ : ∀ (z : 𝕜), f z = (z - z₀) ^ n • F z → g z = (z - z₀) ^ n • G z → (f + g) z = (z - z₀) ^ n • (F + G) z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f + g) z = (z - z₀) ^ n • (F + G) z

Tactic:
filter_upwards [hF', hG'] with z using by simp +contextual
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
simpa [sub_eq_add_neg] using le_analyticOrderAt_add (f := f) (g := -g)

Premises used: sub_eq_add_neg, le_analyticOrderAt_add
-- Module: Mathlib.Analysis.Analytic.Order
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₀ ≤ analyticOrderAt f z₀

Tactic:
simpa [hfg.not_ge] using le_analyticOrderAt_sub (f := f + g) (g := g) (z₀ := z₀)

Premises used: le_analyticOrderAt_sub, LT.lt.not_ge
-- Module: Mathlib.Analysis.Analytic.Order
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 z₀ ≤ analyticOrderAt (f + g) z₀

Tactic:
simpa [hfg.le] using le_analyticOrderAt_add (f := f) (g := g) (z₀ := z₀)

Premises used: LT.lt.le, le_analyticOrderAt_add
-- Module: Mathlib.Analysis.Analytic.Order
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₀
rw₁ rw₂ : analyticOrderAt g z₀ = analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀

Tactic:
rw [add_comm, analyticOrderAt_add_eq_left_of_lt hgf]

Premises used: analyticOrderAt_add_eq_left_of_lt, add_comm
-- Module: Mathlib.Analysis.Analytic.Order
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₀)
inr :
  ∀ (hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀),
    analyticOrderAt (f + g) z₀ = min (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

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg_1 : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
simpa [hfg.le] using analyticOrderAt_add_eq_left_of_lt hfg

Premises used: analyticOrderAt_add_eq_left_of_lt, LT.lt.le
-- Module: Mathlib.Analysis.Analytic.Order
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₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
simpa [hgf.le] using analyticOrderAt_add_eq_right_of_lt hgf

Premises used: LT.lt.le, analyticOrderAt_add_eq_right_of_lt
-- Module: Mathlib.Analysis.Analytic.Order
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₀ = ⊤
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
⊢ analyticOrderAt (f • g) z₀ = ⊤

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃ (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
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
y : 𝕜
hy : y ∈ t
⊢ (f • g) y = 0

Tactic:
simp [h₁t y hy]
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
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:
exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩
-- Module: Mathlib.Analysis.Analytic.Order
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₀ = ⊤
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
⊢ analyticOrderAt (f • g) z₀ = ⊤

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃ (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
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
t : Set 𝕜
h₁t : ∀ y ∈ t, g y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
y : 𝕜
hy : y ∈ t
⊢ (f • g) y = 0

Tactic:
simp [h₁t y hy]
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
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:
exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩
-- Module: Mathlib.Analysis.Analytic.Order
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₀
neg : ∀ (hf' : ¬analyticOrderAt f z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
by_cases hf' : analyticOrderAt f z₀ = ⊤

Premises used: analyticOrderAt
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
simp [analyticOrderAt_smul_eq_top_of_left, *]

Premises used: analyticOrderAt_smul_eq_top_of_left
-- Module: Mathlib.Analysis.Analytic.Order
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₀
neg : ∀ (hg' : ¬analyticOrderAt g z₀ = ⊤), analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
by_cases hg' : analyticOrderAt g z₀ = ⊤

Premises used: analyticOrderAt
-- Module: Mathlib.Analysis.Analytic.Order
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₀

Tactic:
simp [analyticOrderAt_smul_eq_top_of_right, *]

Premises used: analyticOrderAt_smul_eq_top_of_right
-- Module: Mathlib.Analysis.Analytic.Order
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₀ = ⊤
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₀
⊢ 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'

Premises used: AnalyticAt.analyticOrderAt_ne_top, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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
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₀
⊢ 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'

Premises used: AnalyticAt.analyticOrderAt_ne_top, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
rw [← Nat.cast_analyticOrderNatAt hf', ← Nat.cast_analyticOrderNatAt hg', ← ENat.coe_add,
      (hf.smul hg).analyticOrderAt_eq_natCast]

Premises used: Nat.cast_analyticOrderNatAt, AnalyticAt.smul, AnalyticAt.analyticOrderAt_eq_natCast, ENat.coe_add
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ∃ (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:
⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩

Premises used: AnalyticAt.smul, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Analytic.Order
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
neg : (f' • g') z₀ ≠ 0
neg₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
⊢ ∃ (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:
refine ⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩