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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial d) a) = ⊤

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial d) a) = ↑((weight w) d)

Tactic:
· rw [h, weightedOrder_eq_top_iff, map_zero]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial d) a) = ↑((weight w) d)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
inst✝¹ : Semiring R✝
w✝ : σ✝ → ℕ
f✝ g✝ : MvPowerSeries σ✝ R✝
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g

Tactic:
exact ⟨le_rfl, le_of_lt H₁⟩

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a : ℕ∞
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)

Tactic:
by
      rcases eq_zero_or_pos a with rfl | ha
      · simp [ContinuousAt, nhds_prod_eq]
      · simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']
        refine tendsto_nhds_top_mono continuousAt_snd ?_
        filter_upwards [continuousAt_fst (lt_mem_nhds ha)] with (x, y) (hx : 0 < x)
        exact le_mul_of_one_le_left' (Order.one_le_iff_pos.2 hx)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
⊢ (fun d ↦ if (weight w) d = p then (coeff d) (f + g) else 0) =
    (fun d ↦ if (weight w) d = p then (coeff d) f else 0) + fun d ↦ if (weight w) d = p then (coeff d) g else 0

Tactic:
by
    ext d
    simp only [map_add, coeff_apply]
    split_ifs with h
    · rfl
    · rw [add_zero]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = (coeff d) 0

Tactic:
rw [coeff_zero]
    apply coeff_eq_zero_of_lt_weightedOrder w
    rw [hd]
    exact hf

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

Goal state before:
pp: case refine_2.refine_1
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
⊢ {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)} ∈ 𝓝 0

pp: case refine_2.refine_2
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ x ∈ {x | (valuation K v).restrict x < ↑γ}

Tactic:
· rw [Valued.mem_nhds_zero]
        exact ⟨Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv γ, subset_rfl⟩

Goal state after:
case refine_2.refine_2
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ x ∈ {x | (valuation K v).restrict x < ↑γ}
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : Tendsto m f (𝓝 0)
⊢ Tendsto (a • m) f (𝓝 0)

Tactic:
rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢
  intro I hI
  filter_upwards [ha I hI] with i ai_mem
  exact I.smul_mem _ ai_mem

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

Goal state before:
pp: case succ
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n a : ℕ
ih : (trunc n) (↑((trunc n) f) ^ a) = (trunc n) (f ^ a)
⊢ (trunc n) (↑((trunc n) f) ^ (a + 1)) = (trunc n) (f ^ (a + 1))

Tactic:
| succ a ih =>

Goal state after:
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:
by
  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
s : σ
⊢ (substAlgHom ha) (X s) = a s

Tactic:
rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]

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
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬(coeff i) f = 0
j : σ
hj : j ∈ i.support
⊢ (⨅ i, weightedOrder (fun x ↦ 1) (a i)) * ↑(i j) ≤ (fun i c ↦ ↑c * weightedOrder (fun x ↦ 1) (a i)) j (i j)

Tactic:
simp [mul_comm, mul_le_mul_right (iInf_le_iff.mpr fun _ a ↦ a j)]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
m : ℕ
hm : m ∈ Set.Ici (k * (n + 1))
n' : ℕ
hn' : n' ≤ n
⊢ ↑n' < (f ^ m).order

Tactic:
obtain ⟨m, rfl⟩ := le_iff_exists_add.mp (Set.mem_Ici.mp hm)

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < (f ^ (k * (n + 1) + m)).order
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Goal state after:
case inl
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
⊢ ‖term f s 0‖ ≤ ‖↑C / ↑0 ^ (s + (1 - ↑x))‖

case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: 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, i = k * a

Tactic:
← dvd_def

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
⊢ ¬k ∣ i
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
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff n) ((X ^ k) ^ d) = (algebraMap R S) ((coeff (n / k)) f)

Tactic:
finsum_eq_single _ (n / k),

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
⊢ (coeff (n / k)) f • (coeff n) ((X ^ k) ^ (n / k)) = (algebraMap R S) ((coeff (n / k)) f)

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
⊢ ∀ (x : ℕ), x ≠ n / k → (coeff x) f • (coeff n) ((X ^ k) ^ x) = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
⊢ egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
by
  refine le_antisymm ?_ (iSup₂_le fun i hi ↦ le_egauge_pi hi _ _)
  refine le_of_forall_gt fun r hr ↦ ?_
  have : ∀ i ∈ I, ∃ c : 𝕜, x i ∈ c • U i ∧ ‖c‖ₑ < r := fun i hi ↦
    egauge_lt_iff.mp <| (le_iSup₂ i hi).trans_lt hr
  choose! c hc hcr using this
  obtain ⟨c₀, hc₀, hc₀I, hc₀r⟩ :
      ∃ c₀ : 𝕜, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r := by
    have hr₀ : 0 < r := hr.bot_lt
    rcases I.eq_empty_or_nonempty with rfl | hIne
    · obtain hι | hbot : IsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀
      · use 0
        simp [@eq_comm _ ∅, hι, hr₀]
      · rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
        exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩
    · obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne
      by_cases! H : c i₀ ≠ 0 ∨ I = univ
      · exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using! hc_max hi, hcr _ hi₀I⟩
      · have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
        have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
        have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
        rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
        refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
        simp [hc0 i hi]
  refine egauge_lt_iff.2 ⟨c₀, ?_, hc₀r⟩
  rw [smul_set_pi₀' hc₀]
  intro i hi
  exact (hU i hi).smul_mono (hc₀I i hi) (hc i hi)

Goal state after:
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 : 𝕜
hc : 1 < ‖c‖
x : E
⊢ egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Tactic:
by
  simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

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

Goal state before:
pp: case mpr
α : 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 : Tendsto f l (𝓝 0)
U : Set E
hU : U ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
c : 𝕜
hc₀ : 0 < ‖c‖
hcε : ‖c‖ < ↑ε
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 (ball 0 1) (1 x)

Tactic:
replace hc₀ : c ≠ 0 := by simpa using! hc₀

Goal state after:
case mpr
α : 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 : Tendsto f l (𝓝 0)
U : Set E
hU : U ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
c : 𝕜
hcε : ‖c‖ < ↑ε
hc₀ : c ≠ 0
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 (ball 0 1) (1 x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case right
α : 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✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (ball 0 ↑r) 1

Tactic:
filter_upwards [h.eventually_mem hU₀] with a ha

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✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ egauge 𝕜 (id U + id U) (f a) ≤ egauge 𝕜 (ball 0 ↑r) 1
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a ∈ Ioo 0 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =o[atTop] fun x ↦ a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n

Tactic:
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at rt

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a ∈ Ioo 0 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =o[atTop] fun x ↦ a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
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
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  rw [← analyticWithinAt_univ]
  exact hf.analyticWithinAt_of_mem (by simpa using h)

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

Goal state before:
pp: case ht
𝕜 : 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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y) = 0

Tactic:
rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, _root_.zero_apply, _root_.zero_apply]

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
let r' := min r ε

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinAt g 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
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)))
this : Tendsto (fun z ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun z ↦ p.partialSum z.1 z.2) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))

Tactic:
by simpa using A.add this

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
⊢ (q.comp p 1) v = (q 1) fun _i ↦ (p 1) v

Tactic:
have : {Composition.ones 1} = (Finset.univ : Finset (Composition 1)) :=
    Finset.eq_univ_of_card _ (by simp [composition_card])
  simp only [FormalMultilinearSeries.comp, compAlongComposition_apply, ← this,
    Finset.sum_singleton]
  refine q.congr (by simp) fun i hi1 hi2 => ?_
  simp only [applyComposition_ones]
  exact p.congr rfl fun j _hj1 hj2 => by congr!

Goal state after:
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 g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
  exact ⟨r, hr.1.add hr.2⟩

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

Goal state before:
pp: m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N i hi).snd.length = i.fst

Tactic:
rcases i with ⟨k, blocks_fun⟩

Goal state after:
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N ⟨k, blocks_fun⟩ hi).snd.length = ⟨k, blocks_fun⟩.fst
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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop
    ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r)

Tactic:
intro u hu y hy
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩
  have : Metric.eball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds Metric.isOpen_eball yr'
  refine ⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩
  · rw [nhdsWithin_inter_of_mem']
    · exact inter_mem_nhdsWithin _ this
    · apply mem_nhdsWithin_of_mem_nhds
      apply Filter.mem_of_superset this (Metric.eball_subset_eball hr'.le)
  · simpa [Metric.eball_coe] using hf.tendstoUniformlyOn hr' u hu

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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
by
  apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem_nhdsWithin
  exact inter_mem_nhdsWithin _ (Metric.eball_mem_nhds x hf.r_pos)

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
x : E
hf : AnalyticAt 𝕜 f x
⊢ ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y

Tactic:
rcases hf with ⟨g, r, hg⟩
  have : Metric.eball x r ∈ 𝓝 x := Metric.eball_mem_nhds _ hg.r_pos
  filter_upwards [this] with y hy
  apply hg.continuousOn.continuousAt
  exact Metric.isOpen_eball.mem_nhds hy

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
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)

Tactic:
by
  rcases eq_zero_or_pos p.radius with h | h
  · simp [h, continuousOn_empty]
  · exact (p.hasFPowerSeriesOnBall h).continuousOn

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

Goal state before:
pp: case base
𝕜 : 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
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
⊢ ∑ k ∈ Ico 1 1, a ^ k * ‖p.rightInv i x k‖ ≤ (I + 1) * a

Tactic:
Ico_eq_empty_of_le (le_refl 1),

Goal state after:
case base
𝕜 : 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
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
⊢ ∑ k ∈ ∅, a ^ k * ‖p.rightInv i x k‖ ≤ (I + 1) * a
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
c : F
e y✝ : E
x✝ : y✝ ∈ Metric.eball 0 ∞
n : ℕ
hn : n ≠ 0
⊢ ((constFormalMultilinearSeries 𝕜 E c n) fun x ↦ y✝) = 0

Tactic:
simp [constFormalMultilinearSeries_apply_of_nonzero hn]

Goal state after: