mathlib-initiative/mathlib-tactics huggingface dataset:
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 b : σ → R
⊢ rescale (a * b) = rescale a * rescale b

Tactic:
ext; simp [mul_comm, rescale_rescale]

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
⊢ (eulerProduct f).IsMultiplicative

Tactic:
have h (s : Finset ι) : (∏ b ∈ s, f b).IsMultiplicative :=
      isMultiplicative_finsetProd f s fun i a ↦ hf i

Goal state after:
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
⊢ (eulerProduct f).IsMultiplicative
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case hb
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
⊢ HasSubst B

Tactic:
· simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

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 : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - ∑ᶠ (i : ℕ), (coeff i) P * if i = 1 then k else 0) = 0

pp: case hf
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
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) P * (coeff (n + 1 + 1)) (B ^ d)

pp: case hg
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
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) P * if d = 1 then k else 0

Tactic:
· simp only [mul_ite, mul_zero]
          nth_rw 2 [finsum_eq_single (a := 1)]
          · simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_zero]
            rw [coeff_subst']
            · rfl
            · simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']
          · simp +contextual

Goal state after:
case hf
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
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) P * (coeff (n + 1 + 1)) (B ^ d)

case hg
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
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) P * if d = 1 then k else 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
let : NontriviallyNormedField 𝕜 := ⟨c, hc⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.succ.hb
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
⊢ HasSubst (B + -(C ⅟((coeff 1) P) * C ((coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2)))

Tactic:
· simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : SMul 𝕜 E
inst✝⁴ : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Tactic:
simp only [tangentConeAt_def, ofPred_subset_ofPred]
  refine fun y hy ↦ hy.mono ?_
  rw [← smul_one_smul (Filter 𝕜')]
  grw [le_top (a := ⊤ • 1)]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤

Tactic:
apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    exact ⟨y - x, interior_mono Submodule.subset_span this⟩

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
simp [derivWithin_zero_of_not_differentiableWithinAt, *]

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

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : ¬DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
simp [derivWithin_zero_of_not_differentiableWithinAt, *]

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 : ¬AccPt x (𝓟 s)
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [accPt_principal_iff_nhdsWithin, not_neBot] at h
  rw [← hasFDerivWithinAt_sdiff_singleton_self, hasFDerivWithinAt_iff_isLittleOTVS, h]
  exact .bot

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 α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ ↑ε * egauge 𝕜 (ball 0 ↑r) 1 ≤ ↑ε * ↑‖c‖₊ / ↑r

Tactic:
mul_div_assoc

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 α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ ↑ε * egauge 𝕜 (ball 0 ↑r) 1 ≤ ↑ε * (↑‖c‖₊ / ↑r)
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
x₀ : E
s : Set E
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ HasFDerivWithinAt f 0 s x₀

Tactic:
hasFDerivWithinAt_iff_isLittleO,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ (fun x' ↦ f x' - f x₀ - 0 (x' - x₀)) =o[𝓝[s] x₀] fun x' ↦ x' - x₀
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case h₁
𝕜 : 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
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ ≤ ∑' (x : { s // s.card = n }), ‖p (k + n)‖₊

Tactic:
apply p.nnnorm_changeOriginSeries_le_tsum

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

Goal state before:
pp: case h.inl
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑0 ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑0 ^ n ≤ C / ↑0

Tactic:
cases n

Goal state after:
case h.inl.zero
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
hr : r = 0
⊢ ‖p (0 + 1)‖ * ↑0 ^ 0 ≤ ‖p 1‖ ∨ ‖p (0 + 1)‖ * ↑0 ^ 0 ≤ C / ↑0

case h.inl.succ
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
hr : r = 0
n✝ : ℕ
⊢ ‖p (n✝ + 1 + 1)‖ * ↑0 ^ (n✝ + 1) ≤ ‖p 1‖ ∨ ‖p (n✝ + 1 + 1)‖ * ↑0 ^ (n✝ + 1) ≤ C / ↑0
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case e'_5
𝕜 : 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
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
x✝ : ℕ
⊢ ((p x✝) fun x ↦ y) = 0

Tactic:
rw [hp, zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ HasFiniteFPowerSeriesOnBall f p x 0 r

Tactic:
refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
  · rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
    exact le_top
  · intro y hy
    rw [hf (x + y)]
    · convert! hasSum_zero
      rw [hp, zero_apply]
    · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]

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 : ℕ → 𝕜
n : ℕ
⊢ ((c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x ↦ 0) = Pi.single 0 (c 0 • 1) n

Tactic:
cases n

Goal state after:
case zero
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
⊢ ((c 0 • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 E) fun x ↦ 0) = Pi.single 0 (c 0 • 1) 0

case succ
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n✝ : ℕ
⊢ ((c (n✝ + 1) • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) E) fun x ↦ 0) = Pi.single 0 (c 0 • 1) (n✝ + 1)
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 : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : ↑r' < (ofScalars E c).radius
this : 1 < r' * r
⊢ ¬Summable fun n ↦ ‖ofScalars E c n‖ * ↑r' ^ n

Tactic:
apply not_summable_of_ratio_test_tendsto_gt_one this

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : ↑r' < (ofScalars E c).radius
this : 1 < r' * r
⊢ Tendsto (fun n ↦ ‖‖ofScalars E c (n + 1)‖ * ↑r' ^ (n + 1)‖ / ‖‖ofScalars E c n‖ * ↑r' ^ n‖) atTop (𝓝 ↑(r' * r))
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case pos
𝕜 : 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)
r' : ℝ≥0
hrz : r' = 0
⊢ Summable fun n ↦ ‖ofScalars E c n‖ * ↑r' ^ n

Tactic:
apply Summable.comp_nat_add (k := 1)
    simp [hrz]

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 : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * ↑r ^ n / ↑r ^ (n + 1) ≤ ‖c (n + 1)‖ / ‖c n‖

pp: case hb
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ↑r ^ (n + 1)

pp: case hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖

Tactic:
mul_div_assoc

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * (↑r ^ n / ↑r ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖

case hb
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ↑r ^ (n + 1)

case hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < p.radius

Tactic:
refine lt_of_lt_of_le ?_ this

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < ↑‖z‖₊
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i j : ℕ
hi : i < b.length
hj : j < b.blocksFun ⟨i, hi⟩
⊢ a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j

Tactic:
induction j with

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
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ (p.prod q).radius = min p.radius q.radius

Tactic:
by
  apply le_antisymm
  · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [le_min_iff]
    have := (p.prod q).isLittleO_one_of_lt_radius hr
    constructor
    all_goals
      apply FormalMultilinearSeries.le_radius_of_isBigO
      refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
      rw [norm_mul, norm_norm, norm_mul, norm_norm]
      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    · apply le_max_left
    · apply le_max_right
  · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [lt_min_iff] at hr
    have := ((p.isLittleO_one_of_lt_radius hr.1).add
      (q.isLittleO_one_of_lt_radius hr.2)).isBigO
    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
    rw [norm_mul, norm_norm, ← add_mul, norm_mul]
    refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
    rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
    apply Real.le_norm_self

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
k : ℕ
hk : k ∈ ofFn fun j ↦ (i.snd j).length
j : Fin i.fst.length
⊢ 0 < (i.snd j).length

Tactic:
exact Composition.length_pos_of_pos _ (Composition.blocks_pos' _ _ _)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
⊢ Function.LeftInverse
    (fun i ↦
      ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
        { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
    fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩

Tactic:
rintro ⟨a, b⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
⊢ (fun i ↦
        ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
          { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
      ((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩) ⟨a, b⟩) =
    ⟨a, b⟩
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
this : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ

Tactic:
simpa [sub_eq_zero, not_imp_not] using (A.trans this.isBigO_symm).eq_zero_imp

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

Goal state before:
pp: case inr
𝕜 : 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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : ↑c ≠ 0
A : f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c) = c • f'
⊢ HasFDerivWithinAt (fun x ↦ f (↑c • x)) (↑c • f') s x ↔
    HasFDerivWithinAt f f' (↑c • s) ((ContinuousLinearEquiv.smulLeft c) x)

Tactic:
← ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff,

Goal state after:
case inr
𝕜 : 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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : ↑c ≠ 0
A : f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c) = c • f'
⊢ HasFDerivWithinAt (fun x ↦ f (↑c • x)) (↑c • f') s x ↔
    HasFDerivWithinAt (f ∘ ⇑(ContinuousLinearEquiv.smulLeft c)) (f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c))
      (⇑(ContinuousLinearEquiv.smulLeft c) ⁻¹' (↑c • s)) x