-- 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
𝕜 : 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:
by_cases h₂g : hg.order = ⊤

Result:
case pos
𝕜 : 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

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

Proof state:
case right.right.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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Tactic:
obtain ⟨s, h₁s, h₂s, h₃s⟩ := eventually_nhds_iff.1 h₃g₂

Result:
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

Proof state:
𝕜 : 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
⊢ AnalyticAt 𝕜 (g₁ * g₂) z₀

Tactic:
exact h₁g₁.mul h₁g₂

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 = ⊤
h₂g : hg.order = ⊤
⊢ ⋯.order = hf.order + hg.order

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

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃g₁

Result:
case right.right.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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f * g) z = (z - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) z

Proof state:
𝕜 : 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
y : 𝕜
hy : y ∈ t ∩ s
⊢ (f * g) y = (y - z₀) ^ (hf.order.toNat + hg.order.toNat) • (g₁ * g₂) y

Tactic:
simp [h₁t y hy.1, h₁s y hy.2]

Result:
𝕜 : 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
y : 𝕜
hy : y ∈ t ∩ s
⊢ (y - z₀) ^ hf.order.toNat * g₁ y * ((y - z₀) ^ hg.order.toNat * g₂ y) =
    (y - z₀) ^ (hf.order.toNat + hg.order.toNat) * (g₁ y * g₂ y)

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

Tactic:
by_cases h₂f : hf.order = ⊤

Result:
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

case neg
𝕜 : 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

Proof state:
𝕜 : 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
y : 𝕜
hy : y ∈ t ∩ s
⊢ (y - z₀) ^ hf.order.toNat * g₁ y * ((y - z₀) ^ hg.order.toNat * g₂ y) =
    (y - z₀) ^ (hf.order.toNat + hg.order.toNat) * (g₁ y * g₂ y)

Tactic:
ring

Result:
no goals