mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rw [fderiv, ← hasFDerivWithinAt_univ]
  rw [← differentiableWithinAt_univ] at h
  exact h.hasFDerivWithinAt

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case funProp.discharger
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ↑r ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
⊢ 0 < ↑r

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
⊢ 0 < ε * ↑δ / ↑‖c‖₊

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : ∀ᶠ (n : ℕ) in atTop, p n = 0
r : ℝ≥0
n : ℕ
hn : p n = 0
⊢ (fun _x ↦ 0) n = (fun n ↦ ‖p n‖ * ↑r ^ n) n

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ↑C * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
⊢ 0 < ↑r / (↑C * ↑‖c‖₊)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
this : ∀ (n : ℕ), HasSum (fun s ↦ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)
⊢ Summable fun x ↦ ‖p (x.fst - x.snd.card + x.snd.card)‖₊ * r ^ x.snd.card * r' ^ (x.fst - x.snd.card)

Tactic:
refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
this : ∀ (n : ℕ), HasSum (fun s ↦ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)
⊢ Summable fun x ↦
    ∑' (y : Finset (Fin x)),
      ‖p (⟨x, y⟩.fst - ⟨x, y⟩.snd.card + ⟨x, y⟩.snd.card)‖₊ * r ^ ⟨x, y⟩.snd.card * r' ^ (⟨x, y⟩.fst - ⟨x, y⟩.snd.card)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
x✝ : ℕ
⊢ 0 ≤ ‖p x✝‖ * ↑r ^ x✝

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
n : ℕ
hp : ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ 0 ≤ ‖p n‖ * ↑r ^ n

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / ↑r ^ n

Tactic:
exact hCp n

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

Goal state before:
pp: case hb
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ↑‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖u‖ ^ n ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun i ↦ Ei i.castSucc) (Ei (last n) →L[𝕜] G) :=
  { toFun := fun m ↦ (f.curryRight m).mkContinuous (‖f‖ * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }
m : (i : Fin n) → Ei i.castSucc
⊢ 0 ≤ ‖f‖ * ∏ i, ‖m i‖

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
hc : c n = 0
⊢ ofScalars E c n = 0

Tactic:
rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
⊢ ofScalars E 0 = 0

Tactic:
by
  simp [FormalMultilinearSeries.ext_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x✝ : ℕ
hm : n ≤ x✝
⊢ n + k ≤ k + x✝

Tactic:
by grw [hm, add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ (ofScalars E c).radius = ↑r

Tactic:
convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ r = r⁻¹⁻¹
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
hy : ‖y‖ₑ < r
⊢ ∃ r', ‖y‖₊ < r' ∧ ↑r' < r

Tactic:
simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 hy

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
_hi : i ∉ Finset.range (n - k)
⊢ 0 ≤ ‖p (i + k)‖ * ↑r' ^ (i + k)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ 0 ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖

Tactic:
positivity

Goal state after:
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 : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
⊢ 0 ≤ (I + 1) * a

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : 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
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : 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
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity

Goal state after:
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 : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ 0 ≤ (r * S n) ^ (n + 1)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity

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

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
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 : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := ⟨a, ⋯⟩
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : k ∈ Ico 1 (n + 1)
⊢ 0 ≤ a ^ k * ‖p.rightInv i x k‖

Tactic:
positivity

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

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
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 : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := ⟨a, ⋯⟩
n : ℕ
hn : 1 ≤ n
this : ∀ k ∈ Ico 1 (n + 1), 0 ≤ a ^ k * ‖p.rightInv i x k‖
⊢ n ∈ Ico 1 (n + 1)

Tactic:
simp [hn]

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

Goal state before:
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 : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
hfg

Goal state after:
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 : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (g (x + y))

case mpr.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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ x + y ∈ insert x s ∩ eball x r
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
⊢ HasSum (fun n ↦ (q.comp p n) fun _j ↦ y) (g (f (x + y)))

Tactic:
apply D.sigma

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := ⋯
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
⊢ ∀ (b : ℕ), HasSum (fun c ↦ (q.compAlongComposition p ⟨b, c⟩.snd) fun _j ↦ y) ((q.comp p b) fun _j ↦ y)
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: 𝕜 : 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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ 0 < ENNReal.ofReal e

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ u = v ↔ (ofFn fun i ↦ (u.snd i).blocks) = ofFn fun i ↦ (v.snd i).blocks

Tactic:
by
  refine ⟨fun H => by rw [H], fun H => ?_⟩
  rcases u with ⟨a, b⟩
  rcases v with ⟨a', b'⟩
  dsimp at H
  obtain rfl : a = a' := by
    ext1
    have :
      map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
        map List.sum (ofFn fun i : Fin (Composition.length a') => (b' i).blocks) := by
      rw [H]
    simp only [map_ofFn] at this
    change
      (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
        ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
    simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this
  ext1
  · rfl
  · simp only [heq_eq_eq, ofFn_inj] at H ⊢
    ext1 i
    ext1
    exact congrFun H i

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := ⋯
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
A : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (f (x + y))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
⊢ (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) =ᶠ[atTop] fun a ↦
    q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)

Tactic:
filter_upwards [Ici_mem_atTop (0, 1)]

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
A : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (f (x + y))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
⊢ ∀ a ∈ Set.Ici (0, 1),
    q.partialSum a.1 (∑ a ∈ Ico 1 a.2, (p a) fun _b ↦ y) = q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)