mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ ⊤ = ⊤

pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (fun x ↦ g x - g z₀) z₀ ≠ 0

Tactic:
]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (fun x ↦ g x - g z₀) z₀ ≠ 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ g z₀ = g z₀

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖ * ‖↑n !‖⁻¹ * ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖ = ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
]

Goal state after:
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖ * ‖↑n !‖⁻¹ * ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖ = ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖ = ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖ ≠ 0

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0

Tactic:
]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖ ≠ 0

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖ ≠ 0

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ ≠ 0

case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ ≠ 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ g_1, AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ g_1, AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ↑n ! ≠ 0

Tactic:
]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ↑n ! ≠ 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0

Tactic:
]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval c (ascPochhammer 𝕂 n) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0

Tactic:
]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0

Tactic:
]

Goal state after:
case a
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ Polynomial.eval a (ascPochhammer 𝕂 n) ≠ 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ 0 = 0

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 (f ∘ g) z₀

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 (f ∘ g) z₀
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 f (g z₀)

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 f (g z₀)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ,
    ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t

Tactic:
]

Goal state after:
case left
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ,
    ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
this :
  (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
this :
  (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ fderiv ℝ f z = fderiv ℝ f z

pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ DifferentiableAt ℝ f z

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
⊢ DifferentiableAt ℝ f z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case left.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : analyticOrderAt f ↑z = ⊤
⊢ ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
]

Goal state after:
case left.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : analyticOrderAt f ↑z = ⊤
⊢ ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_4
inst✝⁴ : NormedRing R
inst✝³ : Module R E
inst✝² : IsBoundedSMul R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
z : 𝕜
⊢ ((z - x) ^ m * (z - x) ^ n) • f z • g z = ((z - x) ^ m * (z - x) ^ n) • f z • g z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ < ε
this : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ < ε
this : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case empty
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ ∅, MeromorphicAt (F σ) x
⊢ MeromorphicAt 1 x

Tactic:
]

Goal state after:
case empty
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ ∅, MeromorphicAt (F σ) x
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case insert
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s✝ : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ σ ∈ s, MeromorphicAt (F σ) x) → MeromorphicAt (∏ i ∈ s, F i) x
hf : ∀ σ ∈ insert a s, MeromorphicAt (F σ) x
⊢ MeromorphicAt (F a * ∏ x ∈ s, F x) x

Tactic:
]

Goal state after:
case insert
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s✝ : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ σ ∈ s, MeromorphicAt (F σ) x) → MeromorphicAt (∏ i ∈ s, F i) x
hf : ∀ σ ∈ insert a s, MeromorphicAt (F σ) x
⊢ MeromorphicAt (F a * ∏ x ∈ s, F x) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
ι : Type u_5
s✝ : Finset ι
G : ι → 𝕜 → E
x : 𝕜
σ : ι
s : Finset ι
hσ : σ ∉ s
hind : (∀ σ ∈ s, MeromorphicAt (G σ) x) → MeromorphicAt (∑ n ∈ s, G n) x
h : ∀ σ_1 ∈ insert σ s, MeromorphicAt (G σ_1) x
⊢ MeromorphicAt (G σ + ∑ x ∈ s, G x) x

Tactic:
]

Goal state after:
case insert
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
ι : Type u_5
s✝ : Finset ι
G : ι → 𝕜 → E
x : 𝕜
σ : ι
s : Finset ι
hσ : σ ∉ s
hind : (∀ σ ∈ s, MeromorphicAt (G σ) x) → MeromorphicAt (∑ n ∈ s, G n) x
h : ∀ σ_1 ∈ insert σ s, MeromorphicAt (G σ_1) x
⊢ MeromorphicAt (G σ + ∑ x ∈ s, G x) x
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬analyticOrderAt f ↑z = ⊤

Tactic:
]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬analyticOrderAt f ↑z = ⊤