mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
⊢ (i < n → ¬k i = 0) → 1 ≤ degree (k i)

Tactic:
hi'

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)

Tactic:
← not_lt,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬degree (k i) < 1
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ Summable f ↔ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
Summable,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ a, HasSum f a) ↔ ∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff k) (φ * ∏ x ∈ s, (1 - f x)) = (coeff k) φ

Tactic:
exact ih t.2

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

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

Tactic:
Summable,

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∃ a, HasSum f a) ↔ ∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
by
  simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n ↦ f (n + 1)) x =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)

Tactic:
cantorFunction

Goal state after:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n ↦ f (n + 1)) x =
    (bif f 0 then 1 else 0) + c * ∑' (n : ℕ), cantorFunctionAux c (fun n ↦ f (n + 1)) n
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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
n : σ →₀ ℕ
hn : n ∈ Set.Finite.toFinset h2
⊢ Finsupp.degree n ≤ Finsupp.degree d

Tactic:
simp only [map_sum, Set.Finite.mem_toFinset, Function.mem_support, ne_eq] at hn

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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
n : σ →₀ ℕ
hn : ¬(∑ x ∈ range k, (coeff n) ((homogeneousComponent x) f)) • (coeff d) (n.prod fun s e ↦ a s ^ e) = 0
⊢ Finsupp.degree n ≤ Finsupp.degree d
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
| order (subst f φ)

Tactic:
order_eq_order

Goal state after:
R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
| (subst f φ).order
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ f.order ≤ order (subst f φ)

Tactic:
order_eq_order

Goal state after:
R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ MvPowerSeries.order f ≤ (subst f φ).order
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ

Tactic:
rintro a ⟨x, hx, rfl⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x ↦ (a * c) • x) x) / ‖c‖ₑ ≤ ‖a‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.succ.zero
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
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (0 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (0 + 1)) - if 0 + 1 = 1 then k else 0

pp: case e_a.succ.succ
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 (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0

Tactic:
· simp [← sub_eq_add_neg]

Goal state after:
case e_a.succ.succ
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 (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : y ∈ closedBall 0 ↑r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
mem_closedBall_zero_iff,

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖ ≤ ↑r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Summable fun i ↦ (aeval ⋯) (x i)

Tactic:
exact hx.map _ (continuous_aeval _)

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Semiring 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
st : s ⊆ t
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
rw [uniqueDiffWithinAt_iff] at *

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Semiring 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝] s
st : s ⊆ t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ x ∈ closure[inst✝] t
Module: Mathlib.Analysis.Calculus.FDeriv.Const

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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 {x} x

Tactic:
exact hasFDerivWithinAt_singleton f x

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
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)

Tactic:
simp [egauge_prod_mk, *]

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
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)

Tactic:
simp [egauge_prod_mk, *]

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

Goal state before:
pp: case h₂
α : 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
x : α
hx : ↑‖f x‖₊ ≤ ↑C * ↑‖g x‖₊
⊢ ↑‖f x‖₊ ≤ ↑C * ↑‖g x‖₊

Tactic:
exact mod_cast hx

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
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:
NNReal.coe_div,

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 / ↑a) ^ n ≤ C
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case mp
𝕜 : 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
⊢ p.radius = ∞ → ∀ (r : ℝ≥0), Summable fun n ↦ ‖p n‖ * ↑r ^ n

Tactic:
intro h r

Goal state after:
case mp
𝕜 : 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
⊢ Summable fun n ↦ ‖p n‖ * ↑r ^ n
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
y : E
x✝ : y ∈ Metric.eball 0 ∞
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (p.sum (0 + y))

Tactic:
by rw [zero_add]; exact p.hasSum_of_finite hn y

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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → F
⊢ (p.comp (p.rightInv i x) (n + 2)) v = (id 𝕜 F ((p 0) 0) (n + 2)) v

Tactic:
have N : 0 < n + 2 := by simp
    simp [comp_rightInv_aux1 N, h, rightInv, comp_rightInv_aux2, -Set.toFinset_ofPred]

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

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
⊢ (ofFn fun j ↦ (a.sigmaCompositionAux b j).length) = b.blocks

Tactic:
conv_rhs => rw [← ofFn_getElem (xs := b.blocks)]

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
⊢ (ofFn fun j ↦ (a.sigmaCompositionAux b j).length) = ofFn fun i ↦ b.blocks[↑i]
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r

Tactic:
exact hasFPowerSeriesWithinOnBall_pi_iff hr

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
by
  by_cases h : DifferentiableWithinAt 𝕜 f s x
  · exact h.hasFDerivWithinAt.neg.fderivWithin hxs
  · rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]
    simpa

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
x a : E
⊢ DifferentiableAt 𝕜 (fun x ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

Tactic:
by
  simp [DifferentiableAt, hasFDerivAt_comp_add_right]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Finite ι
⊢ Continuous compContinuousLinearMapCLM

Tactic:
by
  rcases nonempty_fintype ι
  refine UniformConvergenceCLM.isUniformInducing_postcomp (.id 𝕜)
    (toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] G) →L[𝕜] _)
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing _ |>.isInducing
    |>.continuous_iff |>.mpr ?_
  change Continuous <|
    (toContinuousMultilinearMapCLM 𝕜 : (F [⋀^ι]→L[𝕜] G) →L[𝕜] _).precomp _ ∘
      ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜
        (fun _ : ι ↦ E) (fun _ ↦ F) G ∘
      (fun f _ ↦ f)
  fun_prop

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Tactic:
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x

Tactic:
refine ⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H =>
      ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun m hm ↦ ?_⟩⟩

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
m : ℕ
hm : ↑m ≤ 0
⊢ ContinuousOn (fun x ↦ p x m) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c : 𝕜
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (c - z)) s = fun x ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - x)

Tactic:
by
  ext a
  have : (fun z : 𝕜 => f (c - z)) = fun z => (fun w => f (c + w)) (-z) := by
    simp only [sub_eq_add_neg]
  rw [this, iteratedFDerivWithin_comp_neg (f := fun w => f (c + w)) n a,
    iteratedFDerivWithin_comp_add_left]
  ring_nf

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: case pos
𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

pp: case neg
𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

Tactic:
· exact (h.hasDerivWithinAt.pow' n).derivWithin hsx

Goal state after:
case neg
𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i
Module: Mathlib.Analysis.Calculus.DiffContOnCl

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
exact continuousOn_singleton f x

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
⊢ 0 ≤ derivWithin g s x

Tactic:
by_cases hx : AccPt x (𝓟 s)

Goal state after:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
hx : AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
hx : ¬AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x