mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : 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 | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} = {p | ε ≤ dist p.1 p.2} ∪ t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x)) s x ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableOn 𝕜 (fun x ↦ Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s

Tactic:
by

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

Goal state before:
pp: case neg
α : 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:
have Z := hε h
          simp only [Set.mem_ofPred_eq] at Z
          exact Or.inr Z

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

Goal state before:
pp: α : 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 < ε
⊢ ε ≤ dist x y ∨ (x, y) ∈ t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (Differentiable 𝕜 fun x ↦ Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
x y : Completion E
⊢ dist x y = ‖-x + y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedAddCommGroup E
x : E
⊢ ‖↑x‖₊ = ‖x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedAddCommGroup E
x : E
⊢ ‖↑x‖ₑ = ‖x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : Completion A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : NormedField A
inst✝ : CompletableTopField A
x y : Completion A
⊢ Continuous fun x ↦ ‖x.1 * x.2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : NormedField A
inst✝ : CompletableTopField A
x y : Completion A
⊢ Continuous fun x ↦ ‖x.1‖ * ‖x.2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : NormedField A
inst✝ : CompletableTopField A
x y : Completion A
⊢ ∀ (a b : A), ‖↑a * ↑b‖ = ‖↑a‖ * ‖↑b‖

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ |dist a b| < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
⊢ Continuous fun x ↦ dist (c • x.1) (c • x.2)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
⊢ Continuous fun x ↦ dist c 0 * dist x.1 x.2

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
x₁ x₂ : Completion α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
⊢ Continuous fun a ↦ dist (c₁ • a) (c₂ • a)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
⊢ Continuous fun a ↦ dist c₁ c₂ * dist a 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
x : Completion α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x ↦ dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x ↦ ↑K * dist x.1 x.2

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f ↑a) (Completion.extension f ↑b) ≤ ↑K * dist ↑a ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x ↦ dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α → β
h : Isometry f
x y : Completion α
x✝¹ x✝ : α
⊢ dist (Completion.extension f ↑x✝¹) (Completion.extension f ↑x✝) = dist ↑x✝¹ ↑x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : Ring α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
inst✝³ : Ring β
inst✝² : PseudoMetricSpace β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
h : Isometry ⇑f
⊢ Continuous fun x ↦ dist x.1 x.2

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : Ring α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
inst✝³ : Ring β
inst✝² : PseudoMetricSpace β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
h : Isometry ⇑f
x y : Completion α
⊢ dist (h.mapRingHom x) (h.mapRingHom y) = dist x y

Tactic:
by

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

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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun y ↦ c y ∘SL d y) ((compL 𝕜 F G H) (c x) ∘SL d' + (compL 𝕜 F G H).flip (d x) ∘SL c') s x

Tactic:
by

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

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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun y ↦ c y ∘SL d y) ((compL 𝕜 F G H) (c x) ∘SL d' + (compL 𝕜 F G H).flip (d x) ∘SL c') x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hu : HasFDerivWithinAt u u' s x
⊢ HasFDerivWithinAt (fun y ↦ (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivAt c c' x
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun y ↦ (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : (i : ι) → NormedAddCommGroup (M i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (M i)
H : Type u_7
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst✝ : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
m : E
⊢ (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : (i : ι) → NormedAddCommGroup (M i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (M i)
H : Type u_7
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst✝ : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
⊢ (fderiv 𝕜 (fun y ↦ (c y) u) x) m = ((fderiv 𝕜 c x) m) u

Tactic:
by

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

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
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst✝ : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
⊢ (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Tactic:
by

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

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
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst✝ : Finite ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
m : E
⊢ (fderiv 𝕜 (fun y ↦ (c y) u) x) m = ((fderiv 𝕜 c x) m) u

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
x : E
hx : x ∈ s
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p ∅

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ HasFTaylorSeriesUpToOn n f₁ p s

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x ↦ p x m) (fun x ↦ q x m) s
x : E
hx : x ∈ s
⊢ (q x 0).curry0 = f x

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x ↦ p x m) (fun x ↦ q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ q x m) (q x m.succ).curryLeft s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ ContinuousOn f s

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ ↑m < ↑(m.succ + k)

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ ↑m ≤ ↑(m + k)

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 : ℕ
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
⊢ HasFTaylorSeriesUpToOn N f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧ ∀ (m : ℕ), ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y m) (p x m.succ).curryLeft s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 : ℕ
⊢ HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔
    HasFTaylorSeriesUpToOn (↑n) f p s ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
⊢ ↑m.succ < ↑n.succ

Tactic:
by

Goal state after: