mathlib-initiative/mathlib-tactics huggingface dataset:
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 δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
⊢ s ×ˢ s ⊆ s ×ˢ s

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
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
⊢ ¬0 = ⊤

Tactic:
]

Goal state after:
case neg
𝕜 : 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
⊢ ¬0 = ⊤
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
hg : MeromorphicAt g x
⊢ MeromorphicAt (g + f) x ↔ MeromorphicAt f x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (g + f) x ↔ MeromorphicAt f x
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
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 ↑w = ⊤

Tactic:
· rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
          exact ENat.zero_ne_top

Goal state after:
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
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
⊢ (fun i ↦ (i - x) • (i - x) ^ m • f i) =ᶠ[𝓝 x] fun z ↦ (z - x) ^ (m + 1) • g z

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
⊢ (fun i ↦ (i - x) • (i - x) ^ m • f i) =ᶠ[𝓝 x] fun z ↦ (z - x) ^ (m + 1) • g z
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • g z = (z - x) • (z - x) ^ m • g z

Tactic:
]

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

Goal state before:
pp: case right
𝕜 : 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 : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
]

Goal state after:
case right
𝕜 : 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 : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → 0 = f⁻¹ x_1

Tactic:
]

Goal state after:
case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → 0 = f⁻¹ x_1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ (ContinuousLinearMap.pi fun i ↦ fderivWithin 𝕜 (fun x ↦ φ x i) s x) 1 = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
]

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ (ContinuousLinearMap.pi fun i ↦ fderivWithin 𝕜 (fun x ↦ φ x i) s x) 1 = fun i ↦ derivWithin (fun x ↦ φ x i) s x
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : ¬AccPt x (𝓟 s)
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
]

Goal state after:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : ¬AccPt x (𝓟 s)
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : ¬(fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : (z - x) ^ n • (f z)⁻¹ = (z - x) ^ m • (g z)⁻¹
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : ¬(fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : (z - x) ^ n • (f z)⁻¹ = (z - x) ^ m • (g z)⁻¹
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (-x * I) + cexp (x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℕ
⊢ MeromorphicAt (f ^ n) x

Tactic:
induction n with
  | zero => simpa only [pow_zero] using! MeromorphicAt.const 1 x
  | succ m hm => simpa only [pow_succ] using! hm.mul hf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos
⊢ deriv (iteratedDeriv n cos) = deriv (iteratedDeriv n cos)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ (fun x ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)

Tactic:
]

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ (fun x ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
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 : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
⊢ y ∈ {x}ᶜ → ContinuousAt f y

Tactic:
h'y

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
h'y : y ∈ {x}ᶜ
⊢ ContinuousAt f y
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Tactic:
]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ cos x✝ / sin x✝ = cos x✝ / sin x✝

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℝ
⊢ cos x✝ / sin x✝ = cos x✝ / sin x✝

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ -(sin x✝ / cos x✝) = -(sin x✝ / cos x✝)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv cos = -tan

Tactic:
ext
  rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℝ
⊢ -(sin x✝ / cos x✝) = -(sin x✝ / cos x✝)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℝ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ 1 • r ^ 0 = 1 • r ^ 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ r ^ 1 = r ^ 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ r = r

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((X + ↑k) * ascPochhammer ℕ k).smeval (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + (X * (ascPochhammer ℕ k).comp (X + 1)).smeval r

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((X + ↑k) * ascPochhammer ℕ k).smeval (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + (X * (ascPochhammer ℕ k).comp (X + 1)).smeval r
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)

Tactic:
rw [Nat.factorial, mul_smul, factorial_nsmul_multichoose_eq_ascPochhammer]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) +
      (↑↑k * (ascPochhammer ℕ k).smeval (r + 1) + 1 * (ascPochhammer ℕ k).smeval (r + 1)) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) +
      (↑↑k * (ascPochhammer ℕ k).smeval (r + 1) + 1 * (ascPochhammer ℕ k).smeval (r + 1)) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ↑k • (ascPochhammer ℕ k).smeval (r + 1) +
      (1 * (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)) =
    k • (ascPochhammer ℕ k).smeval (r + 1) +
      ((ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1))

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ↑k • (ascPochhammer ℕ k).smeval (r + 1) +
      (1 * (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)) =
    k • (ascPochhammer ℕ k).smeval (r + 1) +
      ((ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1))
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r =
    (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ deriv (fun x ↦ x ^ n) (z₀ - x) • g z₀ + (z₀ - x) ^ n • deriv g z₀ =
    (↑n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ deriv (fun x ↦ x ^ n) (z₀ - x) • g z₀ + (z₀ - x) ^ n • deriv g z₀ =
    (↑n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ ↑n + 1 + 1 = ↑n + 1 + 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this : (deriv fun z ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] fun z ↦ (↑n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
⊢ MeromorphicAt (fun z ↦ (↑n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this : (deriv fun z ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] fun z ↦ (↑n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
⊢ MeromorphicAt (fun z ↦ (↑n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z) x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r = (ascPochhammer ℕ n).smeval r

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X.smeval r - ↑n • r ^ 0) =
    (ascPochhammer ℕ n).smeval (X.smeval (r - ↑n) + 1 • (r - ↑n) ^ 0) * (r - ↑n)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X.smeval r - ↑n • r ^ 0) =
    (ascPochhammer ℕ n).smeval (X.smeval (r - ↑n) + 1 • (r - ↑n) ^ 0) * (r - ↑n)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℕ
⊢ 1 = 1

Tactic:
]

Goal state after: