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
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)

Tactic:
hgx

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)

Tactic:
filter_upwards [hWf ε hε, hWg ε hε] with x hfx hgx

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)

Tactic:
hgx

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
⊢ HasDerivAtFilter f₁ f' L

Tactic:
hL.hasDerivAtFilter_iff rfl

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
⊢ HasDerivAtFilter f f' L
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: case refine_2
𝕜 : 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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (fun n ↦ ‖c n‖) l atTop
⊢ Tendsto (fun n ↦ c n • (c n)⁻¹ • v) l (𝓝 v)

Tactic:
refine tendsto_nhds_of_eventually_eq ?_
    refine (eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_
    simp [hy]

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

Goal state before:
pp: case refine_1
𝕜 : 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 : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ C + ε

pp: case refine_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
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, ‖f' x‖ ≤ (C + ε) * ‖x‖

Tactic:
· exact add_nonneg hC₀ ε0.le

Goal state after:
case refine_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
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, ‖f' x‖ ≤ (C + ε) * ‖x‖
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
h' : p k = 0
⊢ p k = 0

Tactic:
exact h'

Goal state after:
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
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ g =o[𝕜; l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)
⊢ g =o[𝕜; l] f
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 y : E
n : ℕ
t : Finset (Fin n)
⊢ let s := changeOriginIndexEquiv.symm ⟨n, t⟩;
  (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y) =
    (p n) (t.piecewise (fun x_1 ↦ x) fun x ↦ y)

Tactic:
by
  have : ∀ (m) (hm : n = m), p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) =
      p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) := by
    rintro m rfl
    simp +unfoldPartialApp [Finset.piecewise]
  simp_rw [changeOriginSeriesTerm_apply, eq_comm]; apply this

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 : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ∃ x, ¬(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = 0 x

Tactic:
use fun _ ↦ 1

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ¬((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x ↦ 1) = 0 fun x ↦ 1
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
⊢ ‖c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖

Tactic:
norm_smul

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
⊢ ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖
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‖ * ↑r' ^ n

pp: case neg
𝕜 : 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‖ * ↑r' ^ n

Tactic:
· apply Summable.comp_nat_add (k := 1)
    simp [hrz]

Goal state after:
case neg
𝕜 : 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‖ * ↑r' ^ n
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case mp
𝕜 : 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∞
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesOnBall f p x r

Tactic:
refine ⟨h.r_le, h.r_pos, fun {y} m ↦ h.hasSum (by simp) m⟩

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
x : E
hf : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
rcases hf with ⟨r, hr⟩
  filter_upwards [Metric.eball_mem_nhds (0 : E) hr.r_pos] with y hy
  exact hr.tendsto_partialSum hy

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 : 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
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)] fun y ↦
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
set L : E × E → ℝ := fun y =>
    C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))

Goal state after:
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 : 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))
⊢ (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)] fun y ↦
    ‖y - (x, x)‖ * ‖y.1 - y.2‖
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 < 0
⊢ id 𝕜 E x 0 = 0

Tactic:
contradiction

Goal state after:
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 < 1
⊢ id 𝕜 E x 1 = 0

Tactic:
contradiction

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

Goal state before:
pp: case e_f.e_p
𝕜 : 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
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
k : ℕ
x✝ : Fin k → F
⊢ (if k < n + 2 then p.removeZero.rightInv i x k else 0) x✝ = (if k < n + 2 then p.rightInv i x k else 0) x✝

Tactic:
by_cases hk : k < n + 2 <;> simp [hk, IH]

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

Goal state before:
pp: case h'y
𝕜 : 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := ⋯
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
⊢ f x + (f (x + y) - f x) ∈ insert (f x) t

Tactic:
simpa using! fy_mem.1

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

Tactic:
rw [← analyticWithinAt_univ] at hg hf ⊢
  apply hg.comp hf (by simp)

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

Goal state before:
pp: n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b.blocks = b'.blocks

Tactic:
exact h'

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

Goal state before:
pp: case pos
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : (Function.mulSupport f).Finite
⊢ AnalyticAt 𝕜 (∏ᶠ (n : α), f n) c

Tactic:
simp_all [finprod_eq_prod _ hf, Finset.analyticAt_prod]

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

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
x : E
c : F
⊢ fderiv 𝕜 (fun y ↦ c - f y) x = -fderiv 𝕜 f x

Tactic:
simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]

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

Goal state before:
pp: case neg
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (iso x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = fderivWithin 𝕜 f s (iso x) ∘SL ↑iso

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a ↦ dist a a

Tactic:
exact Completion.continuous_dist continuous_id continuous_id

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case pos
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑x, ↑y) ∈ t

Tactic:
exact Or.inl h

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

Goal state before:
pp: case zero_eq
𝕜 : 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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ ∀ x ∈ s, ((p x).shift 0).curry0 = (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)

pp: case fderivWithin
𝕜 : 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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ ∀ (m : ℕ), ↑m < ↑n → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ (p x).shift m) ((p x).shift m.succ).curryLeft s x

pp: case 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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ ∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (fun x ↦ (p x).shift m) s

Tactic:
· intro x _
    rfl

Goal state after:
case fderivWithin
𝕜 : 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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ ∀ (m : ℕ), ↑m < ↑n → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ (p x).shift m) ((p x).shift m.succ).curryLeft s x

case 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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
⊢ ∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (fun x ↦ (p x).shift m) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case refine_2
𝕜 : 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 :
  (∀ 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
⊢ HasFTaylorSeriesUpToOn N f p s

Tactic:
· apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun n ↦ ?_)
    rw [hasFTaylorSeriesUpToOn_succ_nat_iff_right]
    exact ⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩

Goal state after: