mathlib-initiative/mathlib-tactics huggingface dataset:
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
ha : HasSubst a
f g : MvPowerSeries σ R
⊢ subst a (f * g) = subst a f * subst a g

Tactic:
by
  simp only [← substAlgHom_apply ha, map_mul]

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

Goal state before:
pp: case pos
σ : 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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : d = 0
⊢ (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0

pp: case neg
σ : 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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0

Tactic:
· simp [hd, hf]

Goal state after:
case neg
σ : 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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a b : ℝ
h1 : #↑((fun x ↦ x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))

Tactic:
rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]

Goal state after:
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 = ⇑(aeval ⋯)

Tactic:
rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]

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

Goal state before:
pp: case pos
σ : 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 τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : Finsupp.degree d < k
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) =
    (coeff d) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f)

Tactic:
coeff_subst,

Goal state after:
case pos
σ : 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 τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : Finsupp.degree d < k
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) =
    ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ ↑((truncTotal (x s)) (a s)) ^ e)

case pos.ha
σ : 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 τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : Finsupp.degree d < k
⊢ HasSubst fun i ↦ ↑((truncTotal (x i)) (a i))
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
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ (MvPowerSeries.coeff e) (MvPowerSeries.subst (fun x ↦ a) f) =
    ∑ᶠ (d : ℕ), (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)

Tactic:
MvPowerSeries.coeff_subst ha.const f e,

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e ↦ a ^ e) =
    ∑ᶠ (d : ℕ), (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Tactic:
obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
⊢ LSeriesSummable f s
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
⊢ LSeriesSummable f s

Tactic:
obtain ⟨m, hm⟩ := eventually_atTop.mp hC

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
⊢ LSeriesSummable f s
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
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
⊢ (substAlgHom ha) ↑p = (Polynomial.aeval a) p

Tactic:
rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom,
    MvPowerSeries.subst_coe, ← AlgHom.comp_apply]
  apply AlgHom.congr_fun
  apply Polynomial.algHom_ext
  simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
⊢ r ≤ ‖0‖ₑ

Tactic:
apply le_of_forall_gt

Goal state after:
case inr
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
⊢ ∀ (c : ℝ≥0∞), ‖0‖ₑ < c → r < c
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
hf : ∀ᶠ (x : ι) in cofinite, ∀ i ∈ Set.Iic n, (f x) i = 1 i
⊢ ∃ a, ∀ (k l : Finset ι), a ⊆ k → a ⊆ l → (∏ b ∈ k, f b) n = (∏ b ∈ l, f b) n

Tactic:
eventually_iff_exists_mem

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
hf : ∃ v ∈ cofinite, ∀ y ∈ v, ∀ i ∈ Set.Iic n, (f y) i = 1 i
⊢ ∃ a, ∀ (k l : Finset ι), a ⊆ k → a ⊆ l → (∏ b ∈ k, f b) n = (∏ b ∈ l, f b) n
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : ι → 𝕜
hr₀ : 0 < r
hI : ∅.Finite
hU : ∀ i ∈ ∅, Balanced 𝕜 (U i)
hI₀ : ∅ = univ ∨ (∃ i ∈ ∅, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
hr : ⨆ i ∈ ∅, egauge 𝕜 (U i) (x i) < r
hc : ∀ i ∈ ∅, x i ∈ c i • U i
hcr : ∀ i ∈ ∅, ‖c i‖ₑ < r
⊢ IsEmpty ι ∨ (𝓝[≠] 0).NeBot

Tactic:
by simpa [@eq_comm _ ∅] using hI₀

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
refine eq_univ_of_forall fun y ↦ ?_

Goal state after:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ y ∈ tangentConeAt 𝕜 s 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
s : Set E
c : F
x✝¹ x✝ : E
⊢ (fderivWithin 𝕜 (fun x ↦ c) s x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
fderivWithin_const_apply,

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
s : Set E
c : F
x✝¹ x✝ : E
⊢ 0 x✝ = (0 x✝¹) x✝
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 : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V ((⇑g ∘ f) x)

Tactic:
intro U hU

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 : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V ((⇑g ∘ f) x)
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
h : f =o[𝕜; l] g
c : α → 𝕜
⊢ (fun x ↦ c x • f x) =o[𝕜; l] fun x ↦ c x • g x

Tactic:
by
  simp only [isLittleOTVS_iff] at *
  peel h with U hU V hV ε hε x hx
  simp only at *
  rw [egauge_smul_right, egauge_smul_right, mul_left_comm]
  · gcongr
  all_goals exact fun _ ↦ Filter.nonempty_of_mem ‹_›

Goal state after:
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]

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
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ 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
L : Filter (E × E)
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAtFilter f f' L
⊢ (fun p ↦ f p.1 - f p.2) =O[𝕜; L] fun p ↦ p.1 - p.2

Tactic:
simpa using hf.isLittleOTVS.isBigOTVS.fun_add f'.isBigOTVS_comp

Goal state after:
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
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[s] x) (𝓝 0)

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_tendsto, Function.comp_def]

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n = p n

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]
  rfl

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 α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (1 x)

Tactic:
intro U hU

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (1 x)
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
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Tactic:
have x_add_y_mem_ball : x + y ∈ Metric.eball (0 : E) p.radius := by
    refine mem_eball_zero_iff.2 (lt_of_le_of_lt ?_ h)
    exact mod_cast nnnorm_add_le x y

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
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
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
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖c • p n‖ * ↑r ^ n ≤ ‖c‖ * C

Tactic:
norm_smul_le,

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
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖c‖ * ‖p n‖ * ↑r ^ n ≤ ‖c‖ * C
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 : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
⊢ ∀ [inst : DecidableEq (Option ι)] (m : Option ι → G × ((i : ι) → E i)) (i : Option ι) (c : 𝕜)
    (x : G × ((i : ι) → E i)),
    ((B (update m i (c • x) none).1) fun i_1 ↦ (update m i (c • x) (some i_1)).2 i_1) =
      c • (B (update m i x none).1) fun i_1 ↦ (update m i x (some i_1)).2 i_1

Tactic:
by
      intro inst v j c x
      match j with
      | none => simp
      | some j =>
        classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
x✝ : Fin n → E
h : Even n
⊢ ((ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E) n) x✝ =
    (ofScalars E (fun k ↦ (-1) ^ k * c k) n) x✝

Tactic:
simp [ofScalars, show ((-ContinuousLinearMap.id 𝕜 E : _) : E → E) = Neg.neg by rfl,
    ← List.map_ofFn, h.neg_one_pow]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
x✝ : Fin n → E
h : Odd n
⊢ ((ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E) n) x✝ =
    (ofScalars E (fun k ↦ (-1) ^ k * c k) n) x✝

Tactic:
simp [ofScalars, show ((-ContinuousLinearMap.id 𝕜 E : _) : E → E) = Neg.neg by rfl,
    ← List.map_ofFn, h.neg_one_pow]

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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
⊢ (ofScalars E c).radius = ∞

Tactic:
by
  refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_
  by_cases hrz : r' = 0
  · apply Summable.comp_nat_add (k := 1)
    simp [hrz]
  · refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
    · apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
      · simp only [norm_norm]
        exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
      · simp_all
    · filter_upwards [eventually_cofinite_ne 0] with n hn
      simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
      gcongr
      exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

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

Tactic:
refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n ys => ?_⟩

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
⊢ ‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n
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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n✝ : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
n : ℕ
⊢ ‖p n‖ * ↑r' ^ n * (‖y‖ / ↑r') ^ n ≤ C * a ^ n * (‖y‖ / ↑r') ^ n

Tactic:
gcongr ?_ * _; apply hp

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

Goal state before:
pp: case e'_5
𝕜 : 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ ↑rp < p.radius
hrq : rq < 1 ∧ ↑rq < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst
this : ∀ (n : ℕ), HasSum (fun c ↦ (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)
n : ℕ
⊢ 2 ^ n / 4 ^ (n + 1) = 1 / 4 * (1 / 2) ^ n

Tactic:
simp [field, pow_succ, mul_pow, show (4 : ℝ≥0) = 2 * 2 by norm_num]

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
⊢ insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x

Tactic:
apply inter_mem_nhdsWithin

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
⊢ Metric.eball (f x) rg ∈ 𝓝 (f x)