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

Goal state before:
pp: case base
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ S 1 ≤ (I + 1) * a

pp: case succ
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a

Tactic:
·

Goal state after:
case base
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ S 1 ≤ (I + 1) * a
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun n ↦ (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))

Tactic:
add_sub_cancel_left

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

Goal state before:
pp: case succ
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a

Tactic:
·

Goal state after:
case succ
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
st : ∀ y ∈ t, y ∈ s → y = x
yr : 0 ∈ eball 0 (ENNReal.ofReal r)
⊢ x + 0 = x

pp: case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : y ∈ eball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
st : ∀ y ∈ t, y ∈ s → y = x
yr : 0 ∈ eball 0 (ENNReal.ofReal r)
⊢ x + 0 = x
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : y ∈ eball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
yr : y ∈ eball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
ys : x + y ∈ s
⊢ x + y = x
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hac
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ (r * S n) ^ 2 - (r * S n) ^ (n + 1) ≤ (r * S n) ^ 2

pp: case hdb
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ 1 / 2 ≤ 1 - r * S n

Tactic:
·

Goal state after:
case hac
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ (r * S n) ^ 2 - (r * S n) ^ (n + 1) ≤ (r * S n) ^ 2
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ insert x (s ∩ u)

pp: case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ y ∈ eball 0 t

Tactic:
·

Goal state after:
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ insert x (s ∩ u)
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hdb
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ 1 / 2 ≤ 1 - r * S n

Tactic:
·

Goal state after:
case hdb
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ 1 / 2 ≤ 1 - r * S n
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case a.inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
yr : ‖0‖ < r ∧ edist 0 0 < t
⊢ x + 0 ∈ insert x (s ∩ u)

pp: case a.inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
⊢ x + y ∈ insert x (s ∩ u)

Tactic:
·

Goal state after:
case a.inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
yr : ‖0‖ < r ∧ edist 0 0 < t
⊢ x + 0 ∈ insert x (s ∩ u)
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case a.inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
⊢ x + y ∈ insert x (s ∩ u)

Tactic:
·

Goal state after:
case a.inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
⊢ x + y ∈ insert x (s ∩ u)
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ y ∈ eball 0 t

Tactic:
·

Goal state after:
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ y ∈ eball 0 t
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p s x r → ∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r

pp: case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ (∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r) → HasFPowerSeriesWithinOnBall f p s x r

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p s x r → ∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ EqOn f (fun y ↦ p.sum (y - x)) (insert x s ∩ eball x r)

pp: case mp.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesOnBall (fun y ↦ p.sum (y - x)) p x r

Tactic:
·

Goal state after:
case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ EqOn f (fun y ↦ p.sum (y - x)) (insert x s ∩ eball x r)
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ f y = (fun y ↦ p.sum (y - x)) y

pp: case mp.refine_1.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ y - x ∈ eball 0 p.radius

Tactic:
·

Goal state after:
case mp.refine_1.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ f y = (fun y ↦ p.sum (y - x)) y
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1.refine_2.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
e1 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f (x + (y - x)))
⊢ f y = (fun y ↦ p.sum (y - x)) y

pp: case mp.refine_1.refine_2.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s

pp: case mp.refine_1.refine_2.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r

Tactic:
·

Goal state after:
case mp.refine_1.refine_2.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
e1 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f (x + (y - x)))
⊢ f y = (fun y ↦ p.sum (y - x)) y
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1.refine_2.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s

pp: case mp.refine_1.refine_2.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r

Tactic:
·

Goal state after:
case mp.refine_1.refine_2.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1.refine_2.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r

Tactic:
·

Goal state after:
case mp.refine_1.refine_2.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
⊢ y - x ∈ eball 0 r