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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a b : σ → MvPowerSeries τ S
ha : HasSubst a
hb : HasSubst b
this : UniformSpace S := ⊥
⊢ HasSubst (a + b)

Tactic:
hasSubst_iff_hasEval_of_discreteTopology

Goal state after:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a b : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
hb : HasEval b
ha : HasEval a
⊢ HasEval (a + b)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
b a : σ → MvPowerSeries τ S
ha : HasSubst a
this : UniformSpace S := ⊥
⊢ HasSubst (b * a)

Tactic:
hasSubst_iff_hasEval_of_discreteTopology

Goal state after:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
b a : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
ha : HasEval a
⊢ HasEval (b * a)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ 0
⊢ x = 0

Tactic:
Set.mem_zero

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x = 0
⊢ x = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case e_a.e_a
σ : 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1 =
    (∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1

Tactic:
rw [← Finset.prod_mul_distrib]

Goal state after:
case e_a.e_a
σ : 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1 =
    ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ x.1 x_1 * a x_1 ^ x.2 x_1
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)
⊢ Invertible ((coeff 1) P.substInv)

Tactic:
simpa using invertibleInvOf

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

Goal state before:
pp: R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ (aeval ⋯) (∑' (i : ℕ), x i) = ∑' (i : ℕ), (aeval ⋯) (x i)

Tactic:
hx.map_tsum _

Goal state after:
R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ ∑' (i : ℕ), (aeval ⋯) (x i) = ∑' (i : ℕ), (aeval ⋯) (x i)

R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Continuous ⇑(aeval ⋯)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff e) (subst (X₀ + X₁) f) = ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

Tactic:
PowerSeries.subst,

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff e) (MvPowerSeries.subst (fun x ↦ X₀ + X₁) f) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s t : Set E
x : E
inst✝ : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ Tendsto (fun x_1 ↦ x + x_1) (𝓝 0) (𝓝 x)

Tactic:
exact (continuous_const_add x).tendsto' 0 x (add_zero _)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Semiring 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
s : Set E
x : E
inst✝ : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ y ∈ 0

Tactic:
have H₁ : Tendsto (x + d ·) l (𝓝 x) := by
    simpa using tendsto_const_nhds.add hd₀

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Semiring 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
s : Set E
x : E
inst✝ : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
H₁ : Tendsto (fun x_1 ↦ x + d x_1) l (𝓝 x)
⊢ y ∈ 0
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
hs : (interior s).Nonempty
hx : x ∈ closure[inst✝²] s
⊢ Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤

Tactic:
rcases hs with ⟨y, hy⟩
  suffices y - x ∈ interior (tangentConeAt ℝ s x) by
    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
  rw [mem_interior_iff_mem_nhds]
  replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
  apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
  rintro _ ⟨z, zs, rfl⟩
  refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
  exact conv.openSegment_closure_interior_subset_interior hx zs

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
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
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)

Tactic:
have hsf : Summable f := by
    refine .of_nnnorm_bounded (p.changeOriginSeries_summable_aux₁ h) ?_
    rintro ⟨k, l, s, hs⟩
    dsimp only [Subtype.coe_mk]
    exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
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
hsf : Summable f
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
⊢ p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius

Tactic:
obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u
  · simp
  rw [ENNReal.div_le_iff (by simpa using h_zero) (by simp)]
  refine le_of_forall_nnreal_lt fun r hr ↦ ?_
  rw [← ENNReal.div_le_iff (by simpa using h_zero) (by simp), enorm_eq_nnnorm, ← coe_div h_zero.ne']
  obtain ⟨C, hC_pos, hC⟩ := p.norm_mul_pow_le_of_lt_radius hr
  refine le_radius_of_bound _ C fun n ↦ ?_
  calc
    ‖p.compContinuousLinearMap u n‖ * ↑(r / ‖u‖₊) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n := by
      gcongr
      exact nnnorm_compContinuousLinearMap_le p u n
    _ = ‖p n‖ * r ^ n := by
      simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
      rw [mul_div_cancel₀]
      rw [← NNReal.coe_pos] at h_zero
      positivity
    _ ≤ C := hC n

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
m : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ (f (Fin.cons m x 0)) x = (f m) x

Tactic:
cons_zero

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
m : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ (f m) x = (f m) x
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 ∈ insert x s ∩ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using! h.2

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
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 ∈ insert x s ∩ Metric.eball x r
this : ↑‖y - x‖₊ < r
⊢ AnalyticWithinAt 𝕜 f s y
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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : r' = 0
⊢ ↑r' ≤ (ofScalars E c).radius

Tactic:
simp [hrz]

Goal state after:
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 + 1)‖ * ↑r' ^ (n + 1)

Tactic:
simp [hrz]

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

Goal state before:
pp: case inr
𝕜 : 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 y : E
hy : x ≠ y
h : HasFPowerSeriesWithinAt f p s x
⊢ s ∈ 𝓝[s] x

Tactic:
exact self_mem_nhdsWithin

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:
by
  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
  have finsupp : f.support.Finite := by
    apply Set.Finite.subset (s := changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n})
    · apply Set.Finite.preimage (Equiv.injective _).injOn
      simp_rw [← {m | m < n}.iUnion_of_singleton_coe, preimage_iUnion, ← range_sigmaMk]
      exact finite_iUnion fun _ ↦ finite_range _
    · refine fun s ↦ Not.imp_symm fun hs ↦ ?_
      simp only [preimage_ofPred_eq, changeOriginIndexEquiv_apply_fst, mem_ofPred, not_lt] at hs
      dsimp only [f]
      rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, _root_.zero_apply, _root_.zero_apply]
  have hfkl k l : HasSum (f ⟨k, l, ·⟩) (changeOriginSeries p k l (fun _ ↦ x) fun _ ↦ y) := by
    simp_rw [changeOriginSeries, sum_apply]; apply hasSum_fintype
  have hfk k : HasSum (f ⟨k, ·⟩) (changeOrigin p x k fun _ ↦ y) := by
    have (m) (hm : m ∉ Finset.range n) : changeOriginSeries p k m (fun _ ↦ x) = 0 := by
      rw [Finset.mem_range, not_lt] at hm
      rw [changeOriginSeries_finite_of_finite _ hn _ (le_add_of_le_right hm), _root_.zero_apply]
    rw [changeOrigin, FormalMultilinearSeries.sum,
      ContinuousMultilinearMap.tsum_eval (summable_of_ne_finset_zero this)]
    refine (summable_of_ne_finset_zero (s := Finset.range n) fun m hm ↦ ?_).hasSum.sigma_of_hasSum
      (hfkl k) (summable_of_hasFiniteSupport <| finsupp.preimage sigma_mk_injective.injOn)
    rw [this m hm, _root_.zero_apply]
  have hf : HasSum f ((p.changeOrigin x).sum y) :=
    ((p.changeOrigin x).hasSum_of_finite (fun _ ↦ changeOrigin_finite_of_finite p hn) _)
      |>.sigma_of_hasSum hfk (summable_of_hasFiniteSupport finsupp)
  refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)
  refine (p.hasSum_of_finite hn (x + y)).sigma_of_hasSum (fun n ↦ ?_)
    (changeOriginIndexEquiv.symm.summable_iff.2 hf.summable)
  rw [← Pi.add_def, (p n).map_add_univ (fun _ ↦ x) fun _ ↦ y]
  simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm]
  exact hasSum_fintype fun c ↦ f (changeOriginIndexEquiv.symm ⟨n, c⟩)

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
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
⊢ (ofScalars E c).radius = r⁻¹

Tactic:
rcases ENNReal.trichotomy r with (hr | hr | hr)
  · 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])⟩
  · simp_rw [hr, inv_top] at hc' ⊢
    apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)
    refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))
    filter_upwards [hc'.eventually_ne top_ne_zero] with n hn
    apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm
    simp_all
  · have hr' := toReal_ne_zero.mp hr.ne.symm
    have hr'' := toNNReal_ne_zero.mpr hr' -- this result could go in ENNReal
    convert! ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
    · simp [ENNReal.coe_inv hr'', ENNReal.coe_toNNReal (toReal_ne_zero.mp hr.ne.symm).2]
    · simp_rw [ENNReal.coe_toNNReal_eq_toReal]
      refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'
      filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]
      simp

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

Goal state before:
pp: case inr.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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

Tactic:
change
      ∀ b : Composition n, b ∈ Finset.univ → b ≠ Composition.single n n_pos →
        compAlongComposition (id 𝕜 F (p 0 v0)) p b = 0
      intro b _ hb
      have A : 1 < b.length := by
        have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
        have : 0 < b.length := Composition.length_pos_of_pos b n_pos
        lia
      ext v
      rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A, _root_.zero_apply,
        _root_.zero_apply]

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

Goal state before:
pp: case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m
this : ∀ i < m.1, i < n.1
⊢ a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n

Tactic:
have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2

Goal state after:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m
this✝ : ∀ i < m.1, i < n.1
this : ∀ i < m.2, i < n.2
⊢ a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr.a
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
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 : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ x + y ∈ insert x s ∩ eball x r

Tactic:
· refine ⟨ys, ?_⟩
      simpa only [mem_eball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt

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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
rw [← hy] at hg

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g y
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
rw [← hy] at hg

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
rw [← hy] at hg

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 (g ∘ f) x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ (a.blocks.splitWrtComposition b)[↑i].length = b.blocksFun i

Tactic:
rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]

Goal state after: