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

Goal state before:
pp: case e'_10
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n)).compContinuousLinearMap
        Complex.ofRealCLM)

pp: case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
·

Goal state after:
case e'_10
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n)).compContinuousLinearMap
        Complex.ofRealCLM)
Module: Mathlib.Analysis.Analytic.RadiusLiminf

Goal state before:
pp: case a.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < p.radius
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑r ^ n| ≤ a ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))

Tactic:
·

Goal state after:
case a.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < p.radius
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑r ^ n| ≤ a ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
·

Goal state after:
case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
·

Goal state after:
case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := ⋯
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := ⋯
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ (p - q) n = 0

pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ AnalyticOn 𝕜 g s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := ⋯
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := ⋯
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ (p - q) n = 0
Module: Mathlib.Analysis.Analytic.RadiusLiminf

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
⊢ ↑r ≤ p.radius

Tactic:
·

Goal state after:
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
⊢ ↑r ≤ p.radius
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ AnalyticOn 𝕜 g s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ AnalyticOn 𝕜 g s
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_9
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
x✝ : ℝ
⊢ 1 / (r - x✝) ^ (a + 1) = (⇑Complex.reCLM ∘ (fun x ↦ 1 / (↑r - x) ^ (a + 1)) ∘ ⇑Complex.ofRealCLM) x✝

pp: case e'_10
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦
              (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a))).compContinuousLinearMap
        Complex.ofRealCLM)

pp: case e'_12
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ ‖r‖ₑ = ‖↑r‖ₑ / ‖Complex.ofRealCLM‖ₑ

Tactic:
·

Goal state after:
case e'_9
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
x✝ : ℝ
⊢ 1 / (r - x✝) ^ (a + 1) = (⇑Complex.reCLM ∘ (fun x ↦ 1 / (↑r - x) ^ (a + 1)) ∘ ⇑Complex.ofRealCLM) x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)

pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ (fun x ↦ ‖↑x ^ c‖) =ᶠ[𝓝 t] fun x ↦ x ^ c.re

Tactic:
·

Goal state after:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ (fun x ↦ ‖↑x ^ c‖) =ᶠ[𝓝 t] fun x ↦ x ^ c.re

Tactic:
·

Goal state after:
c : ℂ
t : ℝ
ht : 0 < t
⊢ (fun x ↦ ‖↑x ^ c‖) =ᶠ[𝓝 t] fun x ↦ x ^ c.re
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦
              (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a))).compContinuousLinearMap
        Complex.ofRealCLM)

pp: case e'_12
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ ‖r‖ₑ = ‖↑r‖ₑ / ‖Complex.ofRealCLM‖ₑ

Tactic:
·

Goal state after:
case e'_10
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦
              (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a))).compContinuousLinearMap
        Complex.ofRealCLM)
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ min r r' ≠ 0

pp: case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

pp: case refine_3
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ min r r' ≠ 0
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_12
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ ‖r‖ₑ = ‖↑r‖ₑ / ‖Complex.ofRealCLM‖ₑ

Tactic:
·

Goal state after:
case e'_12
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ ‖r‖ₑ = ‖↑r‖ₑ / ‖Complex.ofRealCLM‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case pos
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun x ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

pp: case neg
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun x ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
·

Goal state after:
case pos
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun x ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun x ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
·

Goal state after:
case neg
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun x ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_9
a b x✝ : ℝ
⊢ (b - a) / (1 - x✝) + a / (1 - x✝) ^ 2 = (((b - a) • fun x ↦ 1 / (1 - x)) + a • fun x ↦ 1 / (1 - x) ^ 2) x✝

pp: case e'_10
a b : ℝ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1

Tactic:
·

Goal state after:
case e'_9
a b x✝ : ℝ
⊢ (b - a) / (1 - x✝) + a / (1 - x✝) ^ 2 = (((b - a) • fun x ↦ 1 / (1 - x)) + a • fun x ↦ 1 / (1 - x) ^ 2) x✝
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℝ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1

Tactic:
·

Goal state after:
case e'_10
a b : ℝ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

pp: case refine_3
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y

Tactic:
·

Goal state after:
case refine_3
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h'
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

pp: case hs
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

pp: case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case h'
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case hs
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

pp: case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case hs
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)