mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
⊢ False

Tactic:
have := congr_arg (coeff n) H

Goal state after:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (X ^ (φ.order.toNat + 1) * ψ)
⊢ False
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) → ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
· intro h
    choose a h using h
    exact ⟨mk a, by simpa using h⟩

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n : ℕ
⊢ ∀ (b : ℕ), n ≤ b → ↑n < (-X ^ (b + 1)).order

Tactic:
intro m

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
⊢ n ≤ m → ↑n < (-X ^ (m + 1)).order
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
a : σ → MvPowerSeries τ S
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(ε.comp (substAlgHom ha))

Tactic:
AlgHom.coe_comp,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
a : σ → MvPowerSeries τ S
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑ε ∘ ⇑(substAlgHom ha)
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case isFalse
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s.re ≤ ‖g n‖ / ↑n ^ s.re

Tactic:
· gcongr

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ ∑ᶠ (d : ℕ), (coeff d) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ d) - (coeff (0 + 1)) X = 0

Tactic:
finsum_eq_single (a := 1)

Goal state after:
case succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ (coeff 1) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ 1) - (coeff (0 + 1)) X = 0

case succ.zero.ha
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ ∀ (x : ℕ), x ≠ 1 → (coeff x) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ x) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a b : σ → R
f : MvPowerSeries σ R
⊢ (rescaleAlgHom (a * b)) f = ((rescaleAlgHom b).comp (rescaleAlgHom a)) f

Tactic:
simp [rescaleAlgHom_apply, rescale_rescale]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - ∑ᶠ (i : ℕ), if i = 1 then (coeff i) P * k else 0) = 0

Tactic:
finsum_eq_single (a := 1)

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - if 1 = 1 then (coeff 1) P * k else 0) = 0

case ha
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∀ (x : ℕ), x ≠ 1 → (if x = 1 then (coeff x) P * k else 0) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
⊢ ∀ m < n + 1, (coeff m) (mk P.substInvFun - B) = 0

Tactic:
intro m

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m✝ : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
m : ℕ
⊢ m < n + 1 → (coeff m) (mk P.substInvFun - B) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

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₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), f₀' x = f₁' x
y : E × E
hy : Prod.map f₀ f₀ y = Prod.map f₁ f₁ y
⊢ (fun p ↦ f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) y = (fun p ↦ f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) y

Tactic:
simp_all [Prod.map]

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✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
refine hV.trans <| .of_forall fun x ↦ ?_

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
x : α
⊢ (fun x ↦ ↑C * egauge 𝕜 V (g x)) x ≤ (fun x ↦ egauge 𝕜 (id (c⁻¹ • V)) (g x)) x
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
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (insert x (s \ {x})) x ↔ HasFDerivWithinAt f f' s x

Tactic:
insert_sdiff_singleton,

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (insert ?m.91 (s \ {y})) x ↔ HasFDerivWithinAt f f' s x

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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ E

Tactic:
insert_sdiff_singleton,

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case h.h.h.h.h.h.hq
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * (↑ε * egauge 𝕜 V (g x))

pp: case h.h.h.h.h.h.hq.h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ c x = 0 → V.Nonempty

pp: case h.h.h.h.h.h.hq.h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ c x = 0 → U.Nonempty

Tactic:
· gcongr

Goal state after:
case h.h.h.h.h.h.hq.h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ c x = 0 → V.Nonempty

case h.h.h.h.h.h.hq.h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ c x = 0 → U.Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
f' : E →L[𝕜] F
x : E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[univ] x) (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0)

Tactic:
nhdsWithin_univ

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
f' : E →L[𝕜] F
x : E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0)
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₀ : 0 < ↑r
a✝ : ℝ
ha✝ : a✝ ∈ Ioo (-1) 1
hp✝ : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a✝ ^ x
this✝ :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : ↑a ∈ Ioo 0 1
hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n
this : ↑r < ↑(r / a)
n : ℕ
⊢ ‖p n‖ * ↑(r / a) ^ n ≤ C

Tactic:
rw [NNReal.coe_div, div_pow, ← mul_div_assoc, div_le_iff₀ (pow_pos ha.1 n)]

Goal state after:
𝕜 : 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₀ : 0 < ↑r
a✝ : ℝ
ha✝ : a✝ ∈ Ioo (-1) 1
hp✝ : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a✝ ^ x
this✝ :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : ↑a ∈ Ioo 0 1
hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n
this : ↑r < ↑(r / a)
n : ℕ
⊢ ‖p n‖ * ↑r ^ n ≤ C * ↑a ^ n
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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin (0 + x) k)
⊢ HasSum (fun c ↦ (p.changeOriginSeriesTerm k c.fst ↑c.snd ⋯) fun x_1 ↦ x) (p.changeOrigin x k)

Tactic:
rw [zero_add] at this

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
⊢ HasSum (fun c ↦ (p.changeOriginSeriesTerm k c.fst ↑c.snd ⋯) fun x_1 ↦ x) (p.changeOrigin x k)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (init m)) (m (last n))‖ ≤ ‖f‖ * ∏ i, ‖m i‖

Tactic:
rw [prod_univ_castSucc, ← mul_assoc]

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (init m)) (m (last n))‖ ≤ (‖f‖ * ∏ i, ‖m i.castSucc‖) * ‖m (last n)‖
Module: Mathlib.Analysis.Analytic.Linear

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 →L[𝕜] F
x : E
⊢ ∀ (m : ℕ), 2 ≤ m → f.fpowerSeries x m = 0

Tactic:
intro m

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 →L[𝕜] F
x : E
m : ℕ
⊢ 2 ≤ m → f.fpowerSeries x m = 0
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 : ℕ → 𝕜
f : E →L[𝕜] E
| (ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E ∘SL f)

Tactic:
← ContinuousLinearMap.neg_comp

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| (ofScalars E c).compContinuousLinearMap ((-ContinuousLinearMap.id 𝕜 E) ∘SL f)
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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
⊢ ∀ {m : ℕ}, n ≤ k + m → p.changeOriginSeries k m = 0

Tactic:
intro m

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
⊢ n ≤ k + m → p.changeOriginSeries k m = 0
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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
⊢ ∀ b ∉ Finset.range (n - k), ((p.changeOriginSeries k b) fun x_1 ↦ x) = 0

Tactic:
intro m

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
m : ℕ
⊢ m ∉ Finset.range (n - k) → ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
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
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
⊢ ∀ x_1 ∈ Finset.range (n - k), ((p.changeOriginSeries k x_1) fun x_2 ↦ x) = 0

Tactic:
intro m

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
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
m : ℕ
⊢ m ∈ Finset.range (n - k) → ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
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 < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
cases hc' <;> aesop

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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun i ↦ 0
zero_mem : 0 ∈ Metric.eball 0 r
i : ℕ
hi : i ≠ 0
this : 0 < i
⊢ ((pf i) fun x ↦ 0) = 0

Tactic:
exact ContinuousMultilinearMap.map_coord_zero _ (⟨0, this⟩ : Fin i) rfl

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
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  simpa using hf.uniform_geometric_approx' h

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
x : E
hf : HasFPowerSeriesWithinAt f p univ x
n : ℕ
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝 0] fun y ↦ ‖y‖ ^ n

Tactic:
simpa using hf.isBigO_sub_partialSum_pow n

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < n
⊢ id 𝕜 E x n = 0

Tactic:
by
  match n with
    | 0 => contradiction
    | 1 => contradiction
    | n + 2 => rfl

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card ι + 1), b ≠ Fintype.card ι → ((f.toFormalMultilinearSeries b) fun x ↦ y) = 0

Tactic:
intro m

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
⊢ m ∈ Finset.range (Fintype.card ι + 1) → m ≠ Fintype.card ι → ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0