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

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    (coeff x.1) (f a) * (coeff x.2) (∏ x ∈ s, f x) =
      ∑ i ∈ Finset.map { toFun := fun f ↦ (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff (i i_1)) (f i_1)

Tactic:
simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      (coeff a_1) (f a) * (coeff b) (∏ x ∈ s, f x) =
        ∑ x ∈ (s.finsuppAntidiag b).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a a_1 x_1)) (f x_1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ Function.Injective toMvPowerSeries

Tactic:
intro x y h
  ext
  simp_rw [← coeff_coe, h]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) (x * ↑n)

Tactic:
hnd

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) ((algebraMap R K) ↑d)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ↑(ofClass (valuation K v)).valueGroup = ↑(ofClass Valued.v).valueGroup

Tactic:
valueGroup_eq K v

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ↑(ofClass Valued.v).valueGroup = ↑(ofClass Valued.v).valueGroup
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ Tendsto (fun x ↦ a ^ x * b ^ x) atTop (𝓝 0)
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ Tendsto (fun x ↦ a ^ x * b ^ x) atTop (𝓝 0)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ ∀ (x : R), ContinuousAt (⇑C) x

Tactic:
refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i ↦ (coeff d) (C i)) (𝓝 r) (𝓝 ((coeff d) (C r)))
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
⊢ ∏' (i : ℕ), (1 - X ^ (i + 1)) ≠ 0

Tactic:
by_contra! h
  obtain h := PowerSeries.ext_iff.mp h 0
  simp [coeff_zero_eq_constantCoeff, (multipliable_one_sub_X_pow R).map_tprod _
    (continuous_constantCoeff R)] at h

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f ^ i)) atTop (𝓝 ((coeff d) 0))

Tactic:
coeff_zero,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f ^ i)) atTop (𝓝 0)
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ (2 ^ ℵ₀) ^ ℵ₀ = 2 ^ ℵ₀

Tactic:
← power_mul,

Goal state after:
⊢ 2 ^ (ℵ₀ * ℵ₀) = 2 ^ ℵ₀
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_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 0 = 0

Tactic:
simp [Nat.ne_zero_of_lt hq]

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

Goal state before:
pp: case e'_3
⊢ 𝔠 = #(ℕ → Bool)

pp: case a.convert_1
⊢ ℝ

pp: case a.convert_2
⊢ 0 < ?a.convert_1✝

pp: case a.convert_3
⊢ ?a.convert_1✝ < 1 / 2

Tactic:
· rw [← power_def, mk_bool, mk_nat, two_power_aleph0]

Goal state after:
case a.convert_1
⊢ ℝ

case a.convert_2
⊢ 0 < ?a.convert_1✝

case a.convert_3
⊢ ?a.convert_1✝ < 1 / 2
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case h
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
⊢ ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re

Tactic:
by_contra! ⟨n, hn₀, hn⟩

Goal state after:
case h
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
⊢ False
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 τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))

Tactic:
by_cases hd : d.degree < k

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
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))

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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : ¬Finsupp.degree d < k
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))
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⟧
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n

Tactic:
by
  rw [← coe_substAlgHom ha, map_pow]

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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)))

Tactic:
by_cases hd : d.degree < k

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 τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)))

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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : ¬Finsupp.degree d < k
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)))
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 τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)))

Tactic:
simp_rw [coeff_truncTotal _ hd, coeff_subst ha]

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 τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
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) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ egauge 𝕜 (s ∪ t) x = min (egauge 𝕜 s x) (egauge 𝕜 t x)

Tactic:
by
  unfold egauge
  simp [smul_set_union, iInf_or, iInf_inf_eq]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ n * (coeff e) f

Tactic:
rw [← hf e he, Finsupp.degree_apply]

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)
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:
by
      rw [subst_substInv_right _ hP, subst_X hQ]

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
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x

Tactic:
by
  rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]

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✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing ⇑f'
⊢ (fun p ↦ f p.1 - f p.2) ~[L] fun p ↦ f' (p.1 - p.2)

Tactic:
rw [IsEquivalent, ← isLittleOTVS_iff_isLittleO (𝕜 := 𝕜)]
  exact hf.isLittleOTVS.trans_isBigOTVS <| f'.isThetaTVS_comp hf' |>.symm.isBigOTVS

Goal state after:
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
b : Option ι → G × ((i : ι) → E i)
⊢ ‖{ toFun := fun p ↦ (B (p none).1) fun i ↦ (p (some i)).2 i, map_update_add' := ⋯, map_update_smul' := ⋯ } b‖ ≤
    ‖B‖ * ∏ i, ‖b i‖

Tactic:
simp only [MultilinearMap.coe_mk, Fintype.prod_option]

Goal state after:
𝕜 : 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
b : Option ι → G × ((i : ι) → E i)
⊢ ‖(B (b none).1) fun i ↦ (b (some i)).2 i‖ ≤ ‖B‖ * (‖b none‖ * ∏ i, ‖b (some i)‖)
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
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
← hasFPowerSeriesWithinAt_univ

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
hf : HasFPowerSeriesWithinAt f p univ x
⊢ HasFPowerSeriesWithinAt f p s x
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
x : E
f : E → F
p : FormalMultilinearSeries 𝕜 E F
U : Set E
hU : U ∈ 𝓝 x
⊢ HasFPowerSeriesWithinAt f p U x ↔ HasFPowerSeriesAt f p x

Tactic:
← hasFPowerSeriesWithinAt_univ

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
f : E → F
p : FormalMultilinearSeries 𝕜 E F
U : Set E
hU : U ∈ 𝓝 x
⊢ HasFPowerSeriesWithinAt f p U x ↔ HasFPowerSeriesWithinAt f p univ x
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
n : ℕ
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝 0] fun y ↦ ‖y‖ ^ n

Tactic:
← hasFPowerSeriesWithinAt_univ

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

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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
m : ℕ
hm : n ≤ m
⊢ -pf m = 0

Tactic:
hf.finite m hm,

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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
m : ℕ
hm : n ≤ m
⊢ -0 = 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓝 (x, x)] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
← hasFPowerSeriesWithinAt_univ

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
x : E
hf : HasFPowerSeriesWithinAt f p univ x
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓝 (x, x)] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ a_1 ∈ Ico 2 (n + 1), ∑ s ∈ Fintype.piFinset fun x ↦ Ico 1 n, ∏ j, r * (a ^ s j * p (s j)) =
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Tactic:
congr! with j

Goal state after:
case a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ∑ s ∈ Fintype.piFinset fun x ↦ Ico 1 n, ∏ j, r * (a ^ s j * p (s j)) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
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
hg : HasFPowerSeriesAt g q (f x)
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt (g ∘ f) (q.comp p) x

Tactic:
← hasFPowerSeriesWithinAt_univ

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
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ min p.radius q.radius

Tactic:
exact min_le_min hf.r_le hg.r_le

Goal state after:
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
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
⊢ HasFPowerSeriesAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) e

Tactic:
← hasFPowerSeriesWithinAt_univ

Goal state after:
𝕜 : 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
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e
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
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e

Tactic:
← hasFPowerSeriesWithinAt_univ

Goal state after:
𝕜 : 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
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z

Tactic:
simp only [pow_succ]
    exact hm.mul hf

Goal state after: