-- Mathlib/Analysis/Analytic/Order.lean
theorem order_mul {f g : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    (hf.mul hg).order = hf.order + hg.order

Proof state:
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ⋯.order = hf.order + hg.order

Tactic:
rw [← ENat.coe_toNat h₂f, ← ENat.coe_toNat h₂g, ← ENat.coe_add, (hf.mul hg).order_eq_nat_iff]

Result:
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ∃ g_1,
    AnalyticAt 𝕜 g_1 z₀ ∧
      g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • g_1 z

Proof state:
case right.left
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ (g₁ * g₂) z₀ ≠ 0

Tactic:
simp

Result:
case right.left
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ¬g₁ z₀ = 0 ∧ ¬g₂ z₀ = 0

Proof state:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
⊢ ⋯.order = hf.order + hg.order

Tactic:
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := hf.order_ne_top_iff.1 h₂f

Result:
case neg.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
⊢ ⋯.order = hf.order + hg.order

Proof state:
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ∃ g_1,
    AnalyticAt 𝕜 g_1 z₀ ∧
      g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • g_1 z

Tactic:
use g₁ * g₂, by exact h₁g₁.mul h₁g₂

Result:
case right
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ (g₁ * g₂) z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Proof state:
case neg.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
⊢ ⋯.order = hf.order + hg.order

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := hg.order_ne_top_iff.1 h₂g

Result:
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ⋯.order = hf.order + hg.order

Proof state:
case right
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ (g₁ * g₂) z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Tactic:
constructor

Result:
case right.left
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ (g₁ * g₂) z₀ ≠ 0

case right.right
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Proof state:
case right.right.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = (fun z => (z - z₀) ^ hf.order.toNat • g₁ z) y
h₂t : IsOpen t
h₃t : z₀ ∈ t
s : Set 𝕜
h₁s : ∀ y ∈ s, g y = (fun z => (z - z₀) ^ hg.order.toNat • g₂ z) y
h₂s : IsOpen s
h₃s : z₀ ∈ s
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Tactic:
exact eventually_nhds_iff.2
  ⟨t ∩ s, fun y hy ↦ (by simp [h₁t y hy.1, h₁s y hy.2]; ring), h₂t.inter h₂s, h₃t, h₃s⟩

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : hf.order = ⊤
⊢ ⋯.order = hf.order + hg.order

Tactic:
simp [hf.order_mul_of_order_eq_top hg h₂f, h₂f]

Result:
no goals

Proof state:
case right.left
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h₂f : ¬hf.order = ⊤
h₂g : ¬hg.order = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ z₀
h₂g₁ : g₁ z₀ ≠ 0
h₃g₁ : f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g₁ z
g₂ : 𝕜 → 𝕜
h₁g₂ : AnalyticAt 𝕜 g₂ z₀
h₂g₂ : g₂ z₀ ≠ 0
h₃g₂ : g =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hg.order.toNat • g₂ z
⊢ ¬g₁ z₀ = 0 ∧ ¬g₂ z₀ = 0

Tactic:
tauto

Result:
no goals