mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
⊢ (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1)) =
    1

Tactic:
by
    ext n
    split_ifs with hq
    · by_cases hn : ∃ k, q ^ k = n
      · obtain ⟨a, rfl⟩ := hn
        simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']
      · simp [hn, one_apply_ne (fun H ↦ hn ⟨0, H.symm⟩)]
    · simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) (subst X f)

Tactic:
coeff_subst HasSubst.X f e,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ X s ^ e)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h2 : (fun x ↦ a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)

Tactic:
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case isTrue
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : n = 0
⊢ 0 ≤ 0

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

Tactic:
· next => rfl

Goal state after:
case isFalse
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < (f ^ (k * (n + 1) + m)).order

Tactic:
grw [pow_add, ← order_mul_ge, pow_mul, ← le_order_pow_of_constantCoeff_eq_zero _
    (by rwa [map_pow]), ← _root_.le_add_right le_rfl, Nat.cast_lt]

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ n' < n + 1
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
b : S⟦X⟧
hb : HasSubst b
f : R⟦X⟧
e : ℕ
⊢ (coeff e) (subst b f) = ∑ᶠ (d : ℕ), (coeff d) f • (coeff e) (b ^ d)

Tactic:
simp [PowerSeries.coeff, coeff_subst hb]

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

pp: case succ.zero.hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ HasSubst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i)

Tactic:
· rw [finsum_eq_single (a := 1)]
      · simp [substInvFun]
      · rintro (_ | _ | _) _ <;> simp_all [substInvFun, mul_pow, coeff_mul_X_pow']

Goal state after:
case succ.zero.hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ HasSubst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i)
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x

Tactic:
rw [tangentConeAt_def]

Goal state after:
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ {y | ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)}
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: case refine_1
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ Tendsto Prod.snd (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) (𝓝 0)

pp: case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ ∀ᶠ (n : R × E) in comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0, x + n.2 ∈ s

pp: case refine_3
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ Tendsto (fun n ↦ n.1 • n.2) (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) (𝓝 y)

Tactic:
· refine (tendsto_snd (f := ⊤)).mono_left <| inf_le_right.trans <| ?_
    gcongr
    apply nhdsWithin_le_nhds

Goal state after:
case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ ∀ᶠ (n : R × E) in comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0, x + n.2 ∈ s

case refine_3
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ Tendsto (fun n ↦ n.1 • n.2) (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) (𝓝 y)
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)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ Q = subst Q (subst P.substInv P)

Tactic:
subst_substInv_right _ hP,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ Q = subst Q X
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
f : E → F
x : E
h : x ∉ tsupport f
⊢ fderiv 𝕜 f x = 0

Tactic:
rw [notMem_tsupport_iff_eventuallyEq] at h
  simp [h.fderiv_eq]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖deriv f x₀‖ ≤ ↑C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitzOn 𝕜 hs hlip

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝¹⁵ : Semiring 𝕜
inst✝¹⁴ : AddCommMonoid E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module 𝕜 E
inst✝¹¹ : Module 𝕜 F
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : ContinuousAdd E
inst✝⁷ : ContinuousAdd F
inst✝⁶ : ContinuousConstSMul 𝕜 E
inst✝⁵ : ContinuousConstSMul 𝕜 F
𝕜' : Type
inst✝⁴ : DivisionSemiring 𝕜'
inst✝³ : Module 𝕜' F
inst✝² : ContinuousConstSMul 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : T2Space F
a : 𝕜'
f : FormalMultilinearSeries 𝕜 E F
z : E
⊢ a • f.sum z = (a • f).sum z

Tactic:
unfold FormalMultilinearSeries.sum

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝¹⁵ : Semiring 𝕜
inst✝¹⁴ : AddCommMonoid E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module 𝕜 E
inst✝¹¹ : Module 𝕜 F
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : ContinuousAdd E
inst✝⁷ : ContinuousAdd F
inst✝⁶ : ContinuousConstSMul 𝕜 E
inst✝⁵ : ContinuousConstSMul 𝕜 F
𝕜' : Type
inst✝⁴ : DivisionSemiring 𝕜'
inst✝³ : Module 𝕜' F
inst✝² : ContinuousConstSMul 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : T2Space F
a : 𝕜'
f : FormalMultilinearSeries 𝕜 E F
z : E
⊢ (a • ∑' (n : ℕ), (f n) fun x ↦ z) = ∑' (n : ℕ), ((a • f) n) fun x ↦ z
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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ f y = 0

Tactic:
hf.eq_partialSum' y hy 0 le_rfl,

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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ pf.partialSum 0 (y - x) = 0
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := ⇑(c.embedding (c.index j))
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
⊢ Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z

Tactic:
exact Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _

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

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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
⊢ b.length ≠ 1

Tactic:
simpa [Composition.eq_single_iff_length] using hb

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

Goal state before:
pp: case hab
𝕜 : 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := ⋯
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := ⋯
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := ⋯
n : ℕ
this : 0 < a
⊢ ‖y - (x, x)‖ ≤ ↑r'

Tactic:
apply hy'.le

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
y : 𝕜
x✝ : edist y 0 < p.radius
hyr : nndist y 0 < r.toNNReal
⊢ ‖y‖ < r

Tactic:
simpa [nndist_eq_nnnorm, Real.lt_toNNReal_iff_coe_lt] using hyr

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
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 : y = 0 ∨ x + y ∈ s
this : x + y = x
⊢ HasSum (fun n ↦ (constFormalMultilinearSeries 𝕜 E (f x) n) fun x ↦ y) (f (x + y))

Tactic:
simp only [this]

Goal state after:
𝕜 : 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 : y = 0 ∨ x + y ∈ s
this : x + y = x
⊢ HasSum (fun n ↦ (constFormalMultilinearSeries 𝕜 E (f x) n) fun x ↦ y) (f x)
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‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) ≤ I * a + I * C * ((r * S n) ^ 2 / (1 / 2))

Tactic:
gcongr
          · simp only [sub_le_self_iff]
            positivity
          · linarith only [rSn]

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
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)))
E : HasSum (fun n ↦ (q.comp p n) fun _j ↦ y) (g (f (x + y)))
⊢ HasSum (fun n ↦ (q.comp p n) fun x ↦ y) (g (f (x + y)))

Tactic:
exact E

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
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 : ℕ
a : Composition n
b : Composition a.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).sum = n

Tactic:
rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]

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

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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 ↦ b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x ↦ (p, p) + x) = fun x ↦
    (h.deriv (x.1 - x.2)) (x.2.1, x.1.2)

Tactic:
ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩

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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
⊢ ((fun p_1 ↦ b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x ↦ (p, p) + x) ((x₁, y₁), x₂, y₂) =
    (h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2)) (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ fderiv 𝕜 (⇑iso ∘ f) = fun x ↦ ↑↑iso ∘SL fderiv 𝕜 f x

Tactic:
ext x : 1
  exact LinearIsometryEquiv.comp_fderiv iso

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

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
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ fderiv 𝕜 (⇑iso ∘ f) = fun x ↦ ↑↑iso ∘SL fderiv 𝕜 f x

Tactic:
by
  ext x : 1
  exact LinearIsometryEquiv.comp_fderiv iso

Goal state after:
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
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
hm : ↑0 ≤ 0
⊢ ContinuousOn (fun x ↦ p x 0) s

Tactic:
have : EqOn (p · 0) ((continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s := fun x hx ↦
    (continuousMultilinearCurryFin0 𝕜 E F).eq_symm_apply.2 (H.2 x hx)

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
hm : ↑0 ≤ 0
this : EqOn (fun x ↦ p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
⊢ ContinuousOn (fun x ↦ p x 0) s
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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

Tactic:
have A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0) := fun y hy ↦
    (h.zero_eq y hy).symm
  suffices H : HasFDerivWithinAt (continuousMultilinearCurryFin0 𝕜 E F ∘ (p · 0))
    (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x from H.congr A (A x hx)
  rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
  have : ((0 : ℕ) : ℕ∞) < n := pos_iff_ne_zero.mpr hn
  convert! h.fderivWithin _ this x hx
  ext y v
  change (p x 1) (snoc 0 y) = (p x 1) (cons y v)
  congr with i
  rw [Unique.eq_default (α := Fin 1) i]
  rfl

Goal state after:
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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : (E [×n]→L[𝕜] E →L[𝕜] F) ≃ₗᵢ[𝕜] E [×n.succ]→L[𝕜] F := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) y
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (⇑I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x) (m 0)) (tail m)

Tactic:
rw [fderivWithin_congr A (A x hx)]

Goal state after:
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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m ≤ n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ p x m

Tactic:
simpa using H.cont

Goal state after:
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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ p x m) univ

Tactic:
simpa using H.cont

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : AnalyticWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
obtain ⟨p, hp⟩ := h
  exact hp.differentiableWithinAt

Goal state after:
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
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
n : ℕ
⊢ iteratedFDeriv 𝕜 n f₁ =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f₂

Tactic:
by
  simp_all [← nhdsWithin_univ, ← iteratedFDerivWithin_univ, EventuallyEq.iteratedFDerivWithin]

Goal state after:
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
f : E → F
n : ℕ
a x : E
⊢ iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)

Tactic:
simp [iteratedFDeriv_comp_add_right']

Goal state after: