mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
rcases h with h | h

Goal state after:
case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order = p.order

Tactic:
refine eq_of_le_of_ge ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order ≤ p.order

case refine_2
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ } n = 1 n

Tactic:
simp [hn, one_apply_ne (fun H ↦ hn ⟨0, H.symm⟩)]

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠

Tactic:
mk_union_le

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
⊢ f * δ = f 1 • δ

Tactic:
by
  ext n
  by_cases hn : n = 1 <;>
  simp [hn, delta]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ ((ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f

Tactic:
rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
⊢ (coeff n) (subst (X ^ k) f) = (algebraMap R S) ((coeff (n / k)) f)

Tactic:
coeff_subst' (.X_pow hk),

Goal state after:
case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff n) ((X ^ k) ^ d) = (algebraMap R S) ((coeff (n / k)) f)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
⊢ (ofPowerSeries (q ^ k)) f = (ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)

Tactic:
by_cases hq : 1 < q
  · ext n
    by_cases hn : ∃ i, q ^ i = n
    · obtain ⟨i, rfl⟩ := hn
      rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]
      split_ifs with hn
      · obtain ⟨j, rfl⟩ := hn
        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
        simp [hk]
      · rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
        exact hn
    · rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
        Function.extend_apply', Function.extend_apply']
      contrapose! hn
      obtain ⟨i, rfl⟩ := hn
      exact ⟨k * i, pow_mul q k i⟩
  · simp [ofPowerSeries, hq, hk]

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

Goal state before:
pp: case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ (coeff n) (subst (X ^ k) f) = 0

Tactic:
coeff_subst' (.X_pow hk),

Goal state after:
case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff n) ((X ^ k) ^ d) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g)) =
    (coeff n) ((fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) * fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g)

Tactic:
rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ i ∈ Finset.antidiagonal n, (n.prod fun s m ↦ a s ^ m) * ((coeff i.1) f * (coeff i.2) g) =
    ∑ p ∈ Finset.antidiagonal n,
      ((coeff p.1) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) *
        (coeff p.2) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g
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:
by
  obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h
  obtain ⟨m, hm⟩ := eventually_atTop.mp hC
  let C' := max C (max' (insert 0 (image (fun n : ℕ ↦ ‖f n‖ / (n : ℝ) ^ (x - 1)) (range m)))
    (insert_nonempty 0 _))
  have hC'₀ : 0 ≤ C' := (le_max' _ _ (mem_insert.mpr (Or.inl rfl))).trans <| le_max_right ..
  have hCC' : C ≤ C' := le_max_left ..
  refine LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n hn₀ ↦ ?_⟩
  rcases le_or_gt m n with hn | hn
  · refine (hm n hn).trans ?_
    have hn₀ : (0 : ℝ) ≤ n := cast_nonneg _
    gcongr
    rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]
  · have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
    refine (div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_
    refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..
    exact mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivAt f 0 x

Tactic:
rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]

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

Tactic:
exact fderiv_of_notMem_tsupport _

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
s t : Set E
h : DifferentiableWithinAt 𝕜 f t x
st : s ⊆ t
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases h with ⟨f', hf'⟩

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
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x
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:
by
  unfold FormalMultilinearSeries.sum
  simp [tsum_const_smul'']

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
⊢ r - ‖y‖ₑ ≤ (p.changeOrigin y).radius

Tactic:
by
    apply le_trans _ p.changeOrigin_radius
    exact tsub_le_tsub hf.r_le le_rfl

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
s t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ s ∈ 𝓝[t] x

Tactic:
simp [← nhdsWithin_eq_iff_eventuallyEq.mpr hst, self_mem_nhdsWithin]

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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε

Tactic:
obtain ⟨r', yr', r'r⟩ : ∃ (r' : ℝ≥0), ‖y‖₊ < r' ∧ r' < r := by
    simp at hy
    simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 hy

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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
⊢ ∀ᶠ (x : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 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
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
this : Tendsto (fun k ↦ ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0)
⊢ ε / 4 > 0

Tactic:
by linarith

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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
this : ContinuousAt (fun z ↦ p.partialSum k z) y
⊢ ε / 4 > 0

Tactic:
by linarith

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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
I : ∀ (w : E), ‖w‖₊ < r' → ‖∑ i ∈ Finset.Ico k n, (p i) fun x ↦ w‖ ≤ ε / 4
⊢ ε / 4 + ε / 4 + ε / 4 < ε

Tactic:
by linarith

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
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 ?_ * _

Goal state after:
case hbc
𝕜 : 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 ≤ C * a ^ n
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ ∀ (m : ℕ), Fintype.card (Option ι) + 1 ≤ m → f.toFormalMultilinearSeriesOfMultilinear m = 0

pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ ∀ y ∈ Metric.eball 0 ∞,
    (∑ i ∈ Finset.range (Fintype.card (Option ι) + 1), (f.toFormalMultilinearSeriesOfMultilinear i) fun x ↦ y) =
      (f (0 + y).1) (0 + y).2

Tactic:
· intro m hm
    apply dif_neg
    exact Nat.ne_of_lt hm

Goal state after:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ ∀ y ∈ Metric.eball 0 ∞,
    (∑ i ∈ Finset.range (Fintype.card (Option ι) + 1), (f.toFormalMultilinearSeriesOfMultilinear i) fun x ↦ y) =
      (f (0 + y).1) (0 + y).2
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

Tactic:
| _ n IH
   => 

Goal state after:
case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x n = p.leftInv i x n
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv i x n

Tactic:
| _ n IH
   => 

Goal state after:
case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv i x n
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ∏ i, ∑ j ∈ Ico 1 n, r * (a ^ j * p j) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Tactic:
simp [prod_const, ← mul_sum, mul_pow]

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

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
f : E → F
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ fderivWithin 𝕜 (g ∘ f) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x

Tactic:
by
  subst hy; exact fderivWithin_comp _ hg hf h hxs

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

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))
⊢ fderivWithin 𝕜 (g' ∘ g ∘ f) s x = fderivWithin 𝕜 g' u (g (f x)) ∘SL fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x

Tactic:
exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
    h2g.comp h2f).fderivWithin hxs

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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ 0 ≤ -n

Tactic:
by linarith

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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ 0 ≤ -n

Tactic:
by linarith

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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
⊢ AnalyticWithinAt 𝕜 (fun x ↦ f x * (g x)⁻¹) s x

Tactic:
exact fa.mul (ga.inv g0)

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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f * g⁻¹) x

Tactic:
exact fa.mul (ga.inv g0)

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ ∀ {y : E},
    x + y ∈ insert x s →
      y ∈ Metric.eball 0 r → HasSum (fun n ↦ (pf.unshift z n) fun x ↦ y) (z + (f (x + y)) (x + y - x))

Tactic:
by
    intro y hy h'y
    apply HasSum.zero_add
    simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]
    exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy h'y)

Goal state after: