mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 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
x✝ : ι → E
⊢ ((SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap
        ((SeparationQuotient.outCLM 𝕜 F).compContinuousAlternatingMap f))
      x✝ =
    f x✝

Tactic:
simp

Goal state after:
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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² + x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ({ toContinuousMultilinearMap := f x✝², map_eq_zero_of_eq' := ⋯ } +
        { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ })
      x✝

Tactic:
simp

Goal state after:
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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² : 𝕜
x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² • x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ }) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
inst✝ : IsEmpty ι
x : F
⊢ (fun f ↦ f 0) (constOfIsEmpty 𝕜 E ι x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F [⋀^ι]→L[𝕜] G
g : E →L[𝕜] F
⊢ ‖f.toContinuousMultilinearMap‖ * ∏ i, ‖g‖ = ‖f‖ * ‖g‖ ^ Fintype.card ι

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ + x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝³;
          { toLinearMap := __LinearMap, cont := ⋯ }) +
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ : 𝕜
x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ • x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((RingHom.id 𝕜) x✝³ •
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ (((f.fderivCompContinuousLinearMap fun x ↦ g) ∘SL ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (E →L[𝕜] F))
        dg)
      v =
    ∑ i, f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
x✝³ : F [⋀^ι]→L[𝕜] G
x✝² x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ ((x✝³.fderivCompContinuousLinearMap x✝²) x✝¹) x✝ = ((0 x✝³ x✝²) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x y : F
x✝ : ι → E
⊢ ((f (x + y)).mkContinuous (C * ‖x + y‖) ⋯) x✝ = ((f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
c : 𝕜
x : F
x✝ : ι → E
⊢ ((f (c • x)).mkContinuous (C * ‖c • x‖) ⋯) x✝ = ((RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
x y : E
x✝ : ι' → F
⊢ ((f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯) x✝ =
    ((f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯ +
        (f (Function.update m i y)).mkContinuous (C * ∏ i_1, ‖Function.update m i y i_1‖) ⋯)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
c : 𝕜
x : E
x✝ : ι' → F
⊢ ((f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯) x✝ =
    (c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯) x✝

Tactic:
simp

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 < ε
x✝ : Completion α × Completion α
⊢ x✝ ∈ {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} ↔ x✝ ∈ {p | ε ≤ dist p.1 p.2} ∪ t

Tactic:
simp

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ x ∈ ∅, (p x 0).curry0 = f x

Tactic:
simp

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

Goal state before:
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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ ∅, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft ∅ x

Tactic:
simp

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

Goal state before:
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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ p x m) ∅

Tactic:
simp

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:
constructor <;> simp

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:
simp

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
⊢ ∞ ≤ ω + 1

Tactic:
simp

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
⊢ ∞ ≤ ∞ + 1

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin (0 + 1) → E
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm
        (↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL fderivWithin 𝕜 f s x))
      m =
    (fderivWithin 𝕜 f s x) (m (last 0))

Tactic:
simp

Goal state after:
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:
| succ m IH =>

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ x ∈ insert x s

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
y : E
hy : y ∈ s
⊢ s ⊆ insert y s

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hy : ↑‖0‖₊ < r
h'y : x + 0 ∈ insert x s
⊢ x = x + 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r

Tactic:
refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries x r

case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ (fun z ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z
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 : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z - a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x - a)

Tactic:
simpa [sub_eq_add_neg] using iteratedFDeriv_comp_add_right' n (-a)

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)

Tactic:
ext b

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a b : 𝕜
⊢ ((iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s b) fun x ↦ 1) =
    ((-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-b)) fun x ↦ 1
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_9
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm =
    ⇑↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• f x ^ (n + 1) =
    ∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i

Tactic:
rw [Finset.sum_range_succ _ (n + 1), Finset.smul_sum]
  simp only [Nat.pred_eq_sub_one, add_tsub_cancel_right, tsub_self, pow_zero, one_smul]
  simp_rw [smul_comm (_ : 𝔸) (_ : 𝔸ᵐᵒᵖ), smul_smul, ← pow_succ']
  congr! 5 with x hx
  simp only [Finset.mem_range, Nat.lt_succ_iff] at hx
  rw [tsub_add_eq_add_tsub hx]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ deriv (fun x ↦ x ^ n) x = ↑n * x ^ (n - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
x✝ : 𝕜
⊢ (∑ i ∈ u, A i) x✝ = ∑ i ∈ u, A i x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r

Tactic:
refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries
    x n r

case refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ Metric.eball x r
⊢ (fun z ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

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

Goal state before:
pp: case inl.refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ fderiv 𝕜 (fun x ↦ 0) y = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

Goal state after: