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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
⊢ aeval ⋯ = ε

Tactic:
apply DFunLike.ext'
  rw [coe_aeval]
  refine (eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm
  intro p
  trans ε.comp (coeToMvPowerSeries.algHom R) p
  · simp
  conv_lhs => rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]
  simp

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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha) ↑((MvPolynomial.monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n

Tactic:
substAlgHom_coe,

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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ (MvPolynomial.aeval a) ((MvPolynomial.monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a
⊢ #ℚ ^ #ℕ = 𝔠

Tactic:
mk_nat,

Goal state after:
case a
⊢ #ℚ ^ ℵ₀ = 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case e'_3
⊢ 𝔠 = 2 ^ #ℕ

Tactic:
mk_nat,

Goal state after:
case e'_3
⊢ 𝔠 = 2 ^ ℵ₀
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: τ : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : DiscreteTopology S
a : MvPowerSeries τ S
⊢ HasSubst a ↔ HasEval a

Tactic:
rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]

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

Goal state before:
pp: τ : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : DiscreteTopology S
a : MvPowerSeries τ S
⊢ HasSubst a ↔ HasEval a

Tactic:
by
  rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]

Goal state after:
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 : τ →₀ ℕ
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)

Tactic:
rw [Function.HasFiniteSupport]
  convert (MvPowerSeries.coeff_subst_finite ha.const f e).image
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv
  rw [← Equiv.preimage_eq_iff_eq_image, ← Function.support_comp_eq_preimage]
  apply congr_arg
  rw [← Equiv.eq_comp_symm]
  ext
  simp [coeff]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = 0

Tactic:
rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]

Goal state after:
case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬∃ a, (q ^ k) ^ a = q ^ 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
⊢ (substAlgHom ha) ↑Polynomial.X = a

Tactic:
substAlgHom_coe,

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
⊢ (Polynomial.aeval a) Polynomial.X = a
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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ ↑(i ()) * MvPowerSeries.weightedOrder w a ≤ (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i

Tactic:
simp [Finsupp.weight_apply, Finsupp.sum_fintype]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : x ∈ s
⊢ egauge 𝕜 s x ≤ 1

Tactic:
by
  rw [← one_smul 𝕜 s] at h
  simpa using egauge_le_of_mem_smul h

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
f : ℕ → R
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | f 0 = 0}

Tactic:
rintro ⟨f, rfl⟩; simp

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 : ℕ
⊢ X ∣ B

Tactic:
rwa [X_dvd_iff]

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

Goal state before:
pp: case right
α : 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 : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V ((⇑g ∘ f) x)

Tactic:
filter_upwards with a

Goal state after:
case right
α : 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 : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
⊢ egauge 𝕜 U (f a) ≤ egauge 𝕜 V ((⇑g ∘ f) a)
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
⊢ (fun x ↦ (f x, g x)) =O[𝕜; l] k

Tactic:
rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)]

Goal state after:
α : 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
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
· have A := H.hasDerivWithinAt.Ici_of_Ioi
    have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
    simpa using (uniqueDiffOn_Ici x).eq self_mem_Ici A B

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
n : ℕ
v : Fin n → E
⊢ (p.compContinuousLinearMap 0 n) v = (constFormalMultilinearSeries 𝕜 E ((p 0) 0) n) v

Tactic:
cases n with
  | zero =>
    simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
      constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]
    congr
    apply Subsingleton.allEq
  | succ =>
    simp [FunLike.coe_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
⊢ Function.RightInverse (fun s ↦ ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩)
    fun s ↦ ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩

Tactic:
by
    rintro ⟨n, s⟩
    simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
⊢ p.changeOriginSeries 1 n = 0

Tactic:
apply Finset.sum_eq_zero (fun s hs ↦ ?_)

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 : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
⊢ p.changeOriginSeriesTerm 1 n ↑s ⋯ = 0
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
i : Fin (n + 1)
f : Ei i →L[𝕜] Ei (i.succAbove j) [×n]→L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ∏ j, ‖m j‖

Tactic:
rw [i.prod_univ_succAbove, ← mul_assoc]
  exact (f (m i)).le_of_opNorm_le (f.le_opNorm _) _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : T2Space E
x : Eᵐᵒᵖ
⊢ ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

Tactic:
simp [ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

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

Goal state before:
pp: 𝕜 : 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 : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
this : j_val = 0
⊢ ((Composition.single n hn).embedding ⟨j_val, j_property⟩) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩

Tactic:
rw! [this]

Goal state after:
𝕜 : 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 : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
this : j_val = 0
⊢ ((Composition.single n hn).embedding ⟨0, ⋯⟩) ⟨i, ⋯⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩
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 : ℕ
⊢ C * a ^ n * (‖y‖ / ↑r') ^ n ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
rw [mul_pow, mul_assoc]

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

Goal state before:
pp: case neg
𝕜 : 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 k) → Fin n := ⇑(c.embedding k)
⊢ p.applyComposition c (Function.update v j z) k = p.applyComposition c v k

Tactic:
change p (c.blocksFun k) (Function.update v j z ∘ r) = p (c.blocksFun k) (v ∘ r)

Goal state after:
case neg
𝕜 : 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 k) → Fin n := ⇑(c.embedding k)
⊢ (p (c.blocksFun k)) (Function.update v j z ∘ r) = (p (c.blocksFun k)) (v ∘ r)
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Tactic:
refine ⟨?_, AnalyticOnNhd.analyticOn⟩

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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOn 𝕜 f s → AnalyticOnNhd 𝕜 f s
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesOnBall g p x (min r (ENNReal.ofReal e))

Tactic:
· exact hg.mono (lt_min hg.r_pos (by positivity)) (min_le_left _ _)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s c

Tactic:
classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))

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 x ↦ x.1 - x.2) = (fun p ↦ p.1 - p.2) ∘ fun x ↦ (p, p) + x

Tactic:
simp [T, Function.comp_def]

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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Tactic:
by
  simpa [sub_eq_add_neg] using hasFDerivWithinAt_comp_add_right (-a)

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✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖f.mkContinuousAlternating C H‖ ≤ max C 0

Tactic:
dsimp only [mkContinuousAlternating]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableOn 𝕜 (fun x ↦ Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s

Tactic:
rw [differentiableOn_pi, Fin.forall_fin_succ, differentiableOn_pi]
  simp only [Fin.cons_zero, Fin.cons_succ]

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
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ (iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)

Tactic:
by
  simp only [iteratedFDerivWithin_succ_apply_right hs hz]
  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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
x₁ : E
h₁x₁ : ∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x
h₂x₁ : x₁ ∈ s
⊢ ftaylorSeriesWithin 𝕜 f₁ s x₁ = ftaylorSeriesWithin 𝕜 f s x₁

Tactic:
ext n : 1

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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
x₁ : E
h₁x₁ : ∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x
h₂x₁ : x₁ ∈ s
n : ℕ
⊢ ftaylorSeriesWithin 𝕜 f₁ s x₁ n = ftaylorSeriesWithin 𝕜 f s x₁ n
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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
⊢ ftaylorSeriesWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] ftaylorSeriesWithin 𝕜 f s

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 h, self_mem_nhdsWithin] with x₁ h₁x₁ h₂x₁
  ext n : 1
  apply (Filter.EventuallyEq.iteratedFDerivWithin (𝕜 := 𝕜) h₁x₁ n).eq_of_nhdsWithin h₂x₁

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case refl
𝕜 : 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
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
h2 : ↑k ≤ n
⊢ (tsupport fun x ↦ p x k) ⊆ tsupport fun x ↦ p x k

Tactic:
| refl =>

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
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
⊢ ftaylorSeries 𝕜 f₁ e₁ = ftaylorSeries 𝕜 f e₁

Tactic:
ext n : 1

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
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
n : ℕ
⊢ ftaylorSeries 𝕜 f₁ e₁ n = ftaylorSeries 𝕜 f e₁ n
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n✝ n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
pow_succ' _ (n + 1)

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n✝ n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt (f * f ^ (n + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x