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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
hne : ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0
⊢ f ⁻¹' {0}ᶜ ∈ codiscreteWithin U

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
hne : ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0
⊢ f ⁻¹' {0}ᶜ ∈ codiscreteWithin U
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
⊢ (∀ z ∈ s, analyticOrderAt f z = ⊤) ↔ EqOn f 0 s

Tactic:
refine ⟨(EventuallyEq.eq_of_nhds <| analyticOrderAt_eq_top.mp <| · · ·), fun hzero z hz ↦ ?_⟩
  apply analyticOrderAt_eq_top.mpr
  filter_upwards [hs.mem_nhds hz]
  exact fun _ ↦ hzero.eq_of_mem

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

Goal state before:
pp: case refine_1
𝕜 : 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 ≤ 𝓝 x

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, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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 ≤ 𝓝 x
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, 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, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case neg.refine_2
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
⊢ ContinuousWithinAt (fun y ↦ ε * ‖y.2 - y.1‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)

Tactic:
have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by grw [inter_subset_right]

Goal state after:
case neg.refine_2
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
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ ContinuousWithinAt (fun y ↦ ε * ‖y.2 - y.1‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
Module: Mathlib.Analysis.Meromorphic.Basic

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

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

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
x✝ : MeromorphicAt f x
n : ℕ
hn : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ (-↑n) • (x_1 - x) ^ n • 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 : 𝕜
f : 𝕜 → E
⊢ (∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ (∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x
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
⊢ multichoose 1 (n + 1) = 1

Tactic:
show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm,

Goal state after:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ multichoose (0 + 1) (n + 1) = 0 + 1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case pos
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

pp: case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : k ≤ n
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : k ≤ n
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : k ≤ n
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt f (x + c)

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt f (x + c)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt f (x + c)

Tactic:
show f = ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) by aesop

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)
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 c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ 0 ^ y) (0 ^ y * log 0) y

pp: case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y ↦ x ^ y) (x ^ y * log x) y

Tactic:
·

Goal state after:
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ 0 ^ y) (0 ^ y * log 0) y
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
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))

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 δ
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
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y ↦ x ^ y) (x ^ y * log x) y

Tactic:
·

Goal state after:
case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y ↦ x ^ y) (x ^ y * log x) y
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ U + {c}
⊢ MeromorphicAt f y

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) y

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ U + {c}
⊢ MeromorphicAt 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
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) y

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

pp: case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
·

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

pp: case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
·

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t y

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
⊢ ContinuousWithinAt f t y

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t y
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case pos
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : k = 0
⊢ choose 0 k = 1

pp: case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : k = 0
⊢ choose 0 k = 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0

Tactic:
·

Goal state after:
case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
⊢ ContinuousWithinAt f t y

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
⊢ ContinuousWithinAt f t y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inl
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
·

Goal state after:
case inl
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r = ?inl.convert_3 / (r + 1)

pp: case inl.convert_3
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ℂ

pp: case inl.convert_4
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) ?inl.convert_3 ↑x

Tactic:
·

Goal state after:
case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r = ?inl.convert_3 / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inl.convert_4
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) (↑x ^ r * (r + 1)) ↑x

Tactic:
·

Goal state after:
case inl.convert_4
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) (↑x ^ r * (r + 1)) ↑x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r * (r + 1) = (r + 1) * ↑x ^ (r + 1 - 1) * ?inl.convert_4.convert_2

pp: case inl.convert_4.convert_2
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ℂ

pp: case inl.convert_4.convert_5
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y) ?inl.convert_4.convert_2 ↑x

pp: case inl.convert_4.convert_6
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ∈ slitPlane

Tactic:
·

Goal state after:
case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r * (r + 1) = (r + 1) * ↑x ^ (r + 1 - 1) * ?inl.convert_4.convert_2