mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
c : α → 𝕜
⊢ (fun x ↦ c x • f x) =o[𝕜; l] fun x ↦ c x • g x

Tactic:
simp only [isLittleOTVS_iff] at *

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h : ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (c x • f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (c x • g x)
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
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * (‖u‖ ^ n * (↑r ^ n / ‖u‖ ^ n)) = ‖p n‖ * ↑r ^ n

Tactic:
mul_div_cancel₀

Goal state after:
𝕜 : 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
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * ↑r ^ n = ‖p n‖ * ↑r ^ n

case hb
𝕜 : 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
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖u‖ ^ n ≠ 0
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case h.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 + 1)‖ * ↑r ^ n ≤ C
m : ℕ
⊢ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ ‖p 0‖ ∨ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ C * ↑r

Tactic:
right

Goal state after:
case h.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 + 1)‖ * ↑r ^ n ≤ C
m : ℕ
⊢ ‖p (m + 1)‖ * ↑r ^ (m + 1) ≤ C * ↑r
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
hsf : Summable f
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ s, (p n) (s.piecewise (fun x_1 ↦ x) fun x ↦ y))

Tactic:
← changeOriginSeriesTerm_changeOriginIndexEquiv_symm

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
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩)
    (∑ x_1,
      ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst
            (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯)
          fun x_2 ↦ x)
        fun x ↦ y)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun i ↦ Ei i.castSucc) (Ei (last n) →L[𝕜] G) :=
  { toFun := fun m ↦ (f.curryRight m).mkContinuous (‖f‖ * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }
m : (i : Fin n) → Ei i.castSucc
⊢ ‖f' m‖ ≤ ‖f‖ * ∏ i, ‖m i‖

Tactic:
simp only [f', MultilinearMap.coe_mk]

Goal state after:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun i ↦ Ei i.castSucc) (Ei (last n) →L[𝕜] G) :=
  { toFun := fun m ↦ (f.curryRight m).mkContinuous (‖f‖ * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }
m : (i : Fin n) → Ei i.castSucc
⊢ ‖(f.curryRight m).mkContinuous (‖f‖ * ∏ i, ‖m i‖) ⋯‖ ≤ ‖f‖ * ∏ i, ‖m i‖
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case h.inr
𝕜 : 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 : 0 < r
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r

Tactic:
right

Goal state after:
case h.inr
𝕜 : 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 : 0 < r
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r
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
m n : ℕ
h : HasFiniteFPowerSeriesAt f p x n
hmn : n ≤ m
⊢ HasFiniteFPowerSeriesAt f p x m

Tactic:
rcases h with ⟨r, hr⟩
  exact ⟨r, hr.of_le hmn⟩

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
inst✝ : Nontrivial E
⊢ Function.Injective (ofScalars E)

Tactic:
by
  intro _ _ h
  ext n
  simpa [ofScalars] using congrArg (fun p ↦ p n fun _ ↦ (1 : E)) h

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 : ℕ → 𝕜
f : E →L[𝕜] E
⊢ (ofScalars E c).compContinuousLinearMap (-f) = (ofScalars E fun k ↦ (-1) ^ k * c k).compContinuousLinearMap f

Tactic:
conv => lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
  rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]

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
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
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ s, (p n) (s.piecewise (fun x_1 ↦ x) fun x ↦ y))

Tactic:
← changeOriginSeriesTerm_changeOriginIndexEquiv_symm

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
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩)
    (∑ x_1,
      ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst
            (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯)
          fun x_2 ↦ x)
        fun x ↦ y)
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ ‖f‖ * ∏ i, ‖p (c.blocksFun i)‖ * ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖ =
    (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖

Tactic:
Finset.prod_mul_distrib,

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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ ‖f‖ * ((∏ x, ‖p (c.blocksFun x)‖) * ∏ x, ∏ j, ‖(v ∘ ⇑(c.embedding x)) j‖) =
    (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < n
⊢ id 𝕜 E x n = 0

Tactic:
match n with
    | 0 => contradiction
    | 1 => contradiction
    | n + 2 => rfl

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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ ↑rp < p.radius
hrq : rq < 1 ∧ ↑rq < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
⊢ ∃ r > 0, Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst

Tactic:
have r0_pos : 0 < r0 := inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1))

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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ ↑rp < p.radius
hrq : rq < 1 ∧ ↑rq < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
⊢ ∃ r > 0, Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ∃ j, ∃ (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = ⟨n, c⟩

Tactic:
refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩

Goal state after:
case refine_1
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨c.length, c.blocksFun⟩ ∈ compPartialSumSource m M N

case refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ compChangeOfVariables m M N ⟨c.length, c.blocksFun⟩ ?refine_1 = ⟨n, c⟩
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : 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
⊢ ↑‖z‖₊ ≤ p.radius

Tactic:
simp only [dist_zero_right] at h

Goal state after:
𝕜 : 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
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ ↑‖z‖₊ ≤ p.radius
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp.refine_1
𝕜 : 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
⊢ y ∈ insert x s ∩ eball x r → f y = (fun y ↦ p.sum (y - x)) y

Tactic:
⟨ys,yb⟩

Goal state after:
case mp.refine_1
𝕜 : 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∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : y ∈ eball x r
⊢ f y = (fun y ↦ p.sum (y - x)) y
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n : ℕ
⊢ ‖alternatingGeometricSeries 𝕜 A n‖ = 1

Tactic:
simp [alternatingGeometricSeries]

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

Goal state before:
pp: case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

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

Goal state before:
pp: case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : E [⋀^ι]→L[𝕜] SeparationQuotient F
⊢ ∃ a, (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap a = f

Tactic:
use (SeparationQuotient.outCLM _ _).compContinuousAlternatingMap f

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : E [⋀^ι]→L[𝕜] SeparationQuotient F
⊢ (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap
      ((SeparationQuotient.outCLM 𝕜 F).compContinuousAlternatingMap f) =
    f
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : TopologicalSpace F
inst✝⁷ : IsTopologicalAddGroup F
G : Type u_5
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜 G
inst✝⁴ : TopologicalSpace G
inst✝³ : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst✝² : AddCommGroup E'
inst✝¹ : Module 𝕜 E'
inst✝ : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (compContinuousLinearMapₗ f).toFun

Tactic:
rw [isEmbedding_toContinuousMultilinearMap.continuous_iff]
    exact (map_continuous <| ContinuousMultilinearMap.compContinuousLinearMapL fun _ ↦ f).comp
      continuous_toContinuousMultilinearMap

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m ≤ N
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
apply (H m).cont m (by simp)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑(n + 1) → ContinuousOn (fun x ↦ p x m) s

Tactic:
intro m (hm : (m : ℕ∞ω) ≤ n.succ)

Goal state after:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
m : ℕ
hm : ↑m ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x m) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s

Tactic:
rw [hasFTaylorSeriesUpToOn_top_iff hN]

Goal state after:
case refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
      ∀ (n : ℕ),
        HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E}, ↑m ≤ n → x ∈ s → p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : ↑(m + 1) ≤ n
hx : x ∈ s
⊢ p x (m + 1) = iteratedFDerivWithin 𝕜 (m + 1) f s x

Tactic:
have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
    have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
    rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
    exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm

Goal state after: