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
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
f : α → E
l : Filter α
⊢ f =O[𝕜; l] f

Tactic:
by
  rw [isBigOTVS_iff]
  exact fun U hU ↦ ⟨U, hU, EventuallyLE.rfl⟩

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✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
⊢ f =O[𝕜; l] g

Tactic:
hb.isBigOTVS_iff (basis_sets _)

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
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
⊢ ∀ (i : ι), p i → ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : 𝕜 → F
L : Filter (𝕜 × 𝕜)
inst✝ : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAtFilter f f' L ↔ HasDerivAtFilter f (f' 1) L

Tactic:
simp [HasDerivAtFilter]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
have := hf.isLittleO.add_isBigOWith (f'.isBigOWith_comp _ _) hK
  simp only [sub_add_cancel, IsBigOWith] at this
  rcases exists_nhds_square this with ⟨U, Uo, xU, hU⟩
  exact
    ⟨U, Uo.mem_nhds xU, lipschitzOnWith_iff_norm_sub_le.2 fun x hx y hy => hU (mk_mem_prod hx hy)⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: case zero
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : Fin 0 → E
⊢ (p 0) (⇑0 ∘ v) = (p 0) ![]

Tactic:
congr

Goal state after:
case zero.e_6
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : Fin 0 → E
⊢ ⇑0 ∘ v = ![]
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
h₀ : 0 < ↑r
a✝ : ℝ
ha✝ : a✝ ∈ Ioo (-1) 1
hp✝ : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a✝ ^ x
this :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : ↑a ∈ Ioo 0 1
hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n
⊢ ↑r < ↑r / ↑a

Tactic:
simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2

Goal state after:
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, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

Tactic:
congr

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
⊢ (fun r ↦ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r) = fun r ↦
    ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
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 : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j : Option ι
x : G × ((i : ι) → E i)
⊢ ∀ (y : G × ((i : ι) → E i)),
    ((B (update v j (x + y) none).1) fun i ↦ (update v j (x + y) (some i)).2 i) =
      ((B (update v j x none).1) fun i ↦ (update v j x (some i)).2 i) +
        (B (update v j y none).1) fun i ↦ (update v j y (some i)).2 i

Tactic:
y

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 : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j : Option ι
x y : G × ((i : ι) → E i)
⊢ ((B (update v j (x + y) none).1) fun i ↦ (update v j (x + y) (some i)).2 i) =
    ((B (update v j x none).1) fun i ↦ (update v j x (some i)).2 i) +
      (B (update v j y none).1) fun i ↦ (update v j y (some i)).2 i
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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ ((pf 0) fun x_1 ↦ y - x) = (pf 0) fun x_1 ↦ x - x

Tactic:
congr

Goal state after:
case e_6
𝕜 : 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ (fun x_1 ↦ y - x) = fun x_1 ↦ x - 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
⊢ ‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n

Tactic:
have : y ∈ Metric.eball (0 : E) r := by
    refine mem_eball_zero_iff.2 (lt_trans ?_ h)
    simpa [enorm] using! yr'

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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
⊢ ‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ p.applyComposition (Composition.ones n) = fun v i ↦ (p 1) fun x ↦ v (Fin.castLE ⋯ i)

Tactic:
funext v i

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
⊢ p.applyComposition (Composition.ones n) v i = (p 1) fun x ↦ v (Fin.castLE ⋯ i)
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)‖) * ∏ i, ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖ =
    (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ a, ∏ s, ‖v (c.blocksFinEquiv ⟨a, s⟩)‖

Tactic:
congr

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
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
⊢ y ∈ Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s → ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
⟨hy', ys⟩

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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) ↑r'
ys : y ∈ insert x s ×ˢ insert x s
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
j : ℕ
hj1 : j < (Composition.ones (n + 2)).length
hj2 : j < n + 2
k : ℕ
x✝¹ x✝ : k < 1
⊢ v (Fin.castLE ⋯ ⟨j, hj1⟩) = v ⟨j, hj2⟩

Tactic:
congr

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

Goal state before:
pp: case convert_2
𝕜 : 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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j ↦ (p 1) fun x ↦ v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j ↦ (p 1) fun x ↦ v j
⊢ ∑ a ∈ {x | x.length < n + 2}.toFinset,
      (p.leftInv i x a.length) (p.applyComposition a (⇑↑i.symm ∘ fun j ↦ (p 1) fun x ↦ v j)) =
    ∑ c ∈ {x | x.length < n + 2}.toFinset, (p.leftInv i x c.length) (p.applyComposition c v)

Tactic:
congr

Goal state after:
case convert_2.e_f
𝕜 : 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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j ↦ (p 1) fun x ↦ v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j ↦ (p 1) fun x ↦ v j
⊢ (fun a ↦ (p.leftInv i x a.length) (p.applyComposition a (⇑↑i.symm ∘ fun j ↦ (p 1) fun x ↦ v j))) = fun c ↦
    (p.leftInv i x c.length) (p.applyComposition c v)
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case convert_2.e_f
𝕜 : 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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j ↦ (p 1) fun x ↦ v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j ↦ (p 1) fun x ↦ v j
c : Composition (n + 2)
⊢ (p.leftInv i x c.length) (p.applyComposition c (⇑↑i.symm ∘ fun j ↦ (p 1) fun x ↦ v j)) =
    (p.leftInv i x c.length) (p.applyComposition c v)

Tactic:
congr

Goal state after:
case convert_2.e_f.e_6.e_a
𝕜 : 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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j ↦ (p 1) fun x ↦ v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j ↦ (p 1) fun x ↦ v j
c : Composition (n + 2)
⊢ (⇑↑i.symm ∘ fun j ↦ (p 1) fun x ↦ v j) = v
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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
C : ℝ
hC :
  ∀ (a b : E),
    edist a x < r' →
      edist b x < r' →
        a ∈ insert x s → b ∈ insert x s → ‖f a - f b - (p 1) fun x ↦ a - b‖ ≤ C * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ C,
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s, edist z x < r' → ‖f y - f z - (p 1) fun x ↦ y - z‖ ≤ C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)

Tactic:
exact ⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n : ℕ
v : Fin 0 → F
⊢ ((p 0) fun _i ↦ 0) = (p 0) ![]

Tactic:
congr

Goal state after:
case e_6
𝕜 : 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
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n : ℕ
v : Fin 0 → F
⊢ (fun _i ↦ 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
⊢ ∀ x_1 ∈ (fun x_2 ↦ x + x_2) ⁻¹' insert x s ∩ Metric.eball 0 r,
    ∃ t ∈ 𝓝[(fun x_2 ↦ x + x_2) ⁻¹' insert x s ∩ Metric.eball 0 r] x_1,
      ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u

Tactic:
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
⊢ y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r →
    ∃ t ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
      ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case i_inj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : ⟨k, blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H'
⊢ ⟨k, blocks_fun⟩ = ⟨k, blocks_fun'⟩

Tactic:
congr

Goal state after:
case i_inj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : ⟨k, blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H'
⊢ blocks_fun = blocks_fun'
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
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
y : E
hy : y ∈ Metric.eball x r
⊢ Metric.eball x r ∈ 𝓝 y

Tactic:
exact Metric.isOpen_eball.mem_nhds hy

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

Goal state before:
pp: 𝕜 : 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
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔ ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case 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
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) → ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

case refine_2
𝕜 : 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
s : Set E
x : E
⊢ (∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g 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
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
rw [← analyticWithinAt_univ] at hg hf ⊢

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
x : E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f Set.univ x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) Set.univ x