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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat, ψ.order.toNat).1) φ * (coeff (φ.order.toNat, ψ.order.toNat).2) ψ ≠ 0

Tactic:
exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasEval X

Tactic:
rw [hasEval_iff]
  exact MvPowerSeries.HasEval.X

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)

Tactic:
intro f g hfg

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a b : ℝ
h1 : #↑((fun x ↦ x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))⁻¹

Tactic:
inv_Ioo_0_left h,

Goal state after:
a b : ℝ
h1 : #↑((fun x ↦ x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioi (b - a)⁻¹)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case inl
x y : ℝ
h : y ≤ x
heq : y = x
⊢ (Icc x y).Countable

pp: case inr
x y : ℝ
h : y ≤ x
hlt : y < x
⊢ (Icc x y).Countable

Tactic:
· simp [heq]

Goal state after:
case inr
x y : ℝ
h : y ≤ x
hlt : y < x
⊢ (Icc x y).Countable
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
simp [hn, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: 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

Tactic:
have := h.le_tsum n fun _ _ ↦ norm_nonneg _

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‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
· by_cases h : ∃ a, q ^ a = n
      · obtain ⟨a, rfl⟩ := h
        simp [(Nat.pow_right_injective hq).extend_apply]
      · simp [h]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n
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)

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:
· rw [coeff_subst' (.X_pow hk), finsum_eq_single _ (n / k), ← pow_mul, Nat.mul_div_cancel' h,
      coeff_X_pow_self, Algebra.algebraMap_eq_smul_one]
    intro j hj
    rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
    contrapose hj
    rw [hj, Nat.mul_div_cancel_left j hk.pos]

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
⊢ (coeff n) (subst (X ^ k) f) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
⊢ φ.order ≤ order (subst f φ)

Tactic:
conv_rhs => rw [order_eq_order]
  exact le_order_subst_left hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x

Tactic:
calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)

Tactic:
rw [le_egauge_iff]
  rintro a ⟨y, hy, hxy⟩
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le
    rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]
    refine egauge_le_of_mem_smul ⟨y, hy, ?_⟩
    simp only [mul_smul, hxy, inv_smul_smul₀ hc]

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

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
n : σ →₀ ℕ
⊢ (coeff n) ((rescale b) ((rescale a) f)) = (coeff n) ((rescale (a * b)) f)

Tactic:
simp [← mul_assoc, mul_pow, mul_comm]

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

Goal state before:
pp: case pos.refine_1
ι : 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
h : ∀ (x : Finset ι), (∏ b ∈ x, f b) 1 = 1
key : ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, 1 = (∏' (b : ι), f b) 1
⊢ (eulerProduct f) 1 = 1

Tactic:
eventually_const,

Goal state after:
case pos.refine_1
ι : 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
h : ∀ (x : Finset ι), (∏ b ∈ x, f b) 1 = 1
key : 1 = (∏' (b : ι), f b) 1
⊢ (eulerProduct f) 1 = 1
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:
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✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ Differentiable 𝕜 f

Tactic:
← differentiableOn_univ,

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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ DifferentiableOn 𝕜 f univ
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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst✝³] (s i)
hs' : ⋃ i, s i = univ
⊢ Differentiable 𝕜 f

Tactic:
← differentiableOn_univ,

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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst✝³] (s i)
hs' : ⋃ i, s i = univ
⊢ DifferentiableOn 𝕜 f univ
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
hf : DifferentiableAt 𝕜 f (R z)
⊢ DifferentiableAt 𝕜 (⇑L ∘ f ∘ ⇑R) z

Tactic:
simpa using (hf.hasFDerivAt.comp_semilinear L R).differentiableAt

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
this : ↑(‖f x‖₊ / ε) ≤ ↑‖g x‖₊
⊢ ‖f x‖ / ↑ε ≤ ‖g x‖

Tactic:
exact_mod_cast this

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
⊢ f =o[𝕜; l] g ↔ f =o[l] g

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩
  have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
  simp only [isLittleO_iff, nhds_basis_ball.isLittleOTVS_iff nhds_basis_ball]
  refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩
  · rcases h ε hε with ⟨δ, hδ₀, hδ⟩
    lift ε to ℝ≥0 using hε.le; lift δ to ℝ≥0 using hδ₀.le; norm_cast at hε hδ₀
    filter_upwards [hδ (δ / ‖c‖₊) (div_pos hδ₀ hc₀).ne'] with x hx
    suffices (‖f x‖₊ / ε : ℝ≥0∞) ≤ ‖g x‖₊ by
      rw [← ENNReal.coe_div hε.ne'] at this
      rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
      exact_mod_cast this
    calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
  · filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
    lift ε to ℝ≥0 using hε.le
    calc
      egauge 𝕜 (ball 0 ε) (f x) ≤ ‖c‖₊ * ‖f x‖₊ / ε :=
        egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hε)
      _ ≤ ‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ‖g x‖₊) / ε := by gcongr; exact_mod_cast hx
      _ = (‖c‖₊ / ‖c‖₊) * (ε / ε) * δ * ‖g x‖₊ := by
        simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]; ring
      _ ≤ 1 * 1 * δ * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = δ * ‖g x‖₊ := by simp
      _ ≤ δ * egauge 𝕜 (ball 0 1) (g x) := by gcongr; apply le_egauge_ball_one

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun n ↦ ‖p.changeOrigin x n‖₊ * r ^ n

Tactic:
refine NNReal.summable_of_le this ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun b ↦ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (b + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ b
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case h'y
𝕜 : 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
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert (x + y) (insert x s)
⊢ x + (y + z) ∈ insert x s

Tactic:
insert_eq_of_mem hy

Goal state after:
case h'y
𝕜 : 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
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert x s
⊢ x + (y + z) ∈ insert x s
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
x✝ : Fin m → E
⊢ (g.compContinuousMultilinearMap 0) x✝ = 0 x✝

Tactic:
exact map_zero g

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Tactic:
let f (s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) : F :=
    p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) fun _ ↦ y

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
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
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
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
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ Metric.eball x r
⊢ HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f y)

Tactic:
by
  have : y - x ∈ Metric.eball 0 r := by simpa [edist_eq_enorm_sub] using hy
  simpa only [add_sub_cancel] using hf.hasSum this

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}
r' : ℝ≥0∞ := ⋯
this : HasFPowerSeriesWithinOnBall f p s x r'
⊢ EqOn g f (s ∩ Metric.eball x r')

Tactic:
intro z

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 ε
this : HasFPowerSeriesWithinOnBall f p s x r'
z : E
⊢ z ∈ s ∩ Metric.eball x r' → g z = f z
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 * (‖c n‖ * ↑r ^ n) ≤ ‖c (n + 1)‖ * ↑r ^ (n + 1)

Tactic:
mul_comm ‖c n‖,

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 * ‖c n‖) ≤ ‖c (n + 1)‖ * ↑r ^ (n + 1)
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = 0
⊢ (ofScalars E c).radius = r⁻¹

pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ∞
⊢ (ofScalars E c).radius = r⁻¹

pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
⊢ (ofScalars E c).radius = r⁻¹

Tactic:
· simp_rw [hr, inv_zero] at hc' ⊢
    by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 0)
    · apply ofScalars_radius_eq_top_of_tendsto E c h ?_
      refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp hc'
      filter_upwards [h]
      simp
    · apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero
      simp only [eventually_atTop, not_exists, not_forall, not_not] at h ⊢
      obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)
      obtain ⟨zi, hzi, z⟩ := h ti
      refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
      nontriviality E
      simp only [ofScalars_eq_zero] at a ⊢
      contrapose! hti
      exact ⟨n, hzi.trans hmn, ENNReal.div_eq_top.mpr (by simp [a, hti])⟩

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ∞
⊢ (ofScalars E c).radius = r⁻¹

case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
⊢ (ofScalars E c).radius = r⁻¹
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)))
⊢ Tendsto (fun z ↦ p.partialSum z.1 z.2) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))

Tactic:
suffices Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y)
    (atTop ×ˢ 𝓝 y) (𝓝 0) by simpa using A.add this

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)))
⊢ Tendsto (fun z ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y) (atTop ×ˢ 𝓝 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
⊢ ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4

Tactic:
by
    have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
      apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)
    exact ((tendsto_order.1 this).2 _ (by linarith)).exists

Goal state after: