mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
]

Goal state after:
𝕜 : 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
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
]

Goal state after:
𝕜 : 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
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) = ↑j

Tactic:
]

Goal state after:
case inl.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) = ↑j
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mp
𝕜 : 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 : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
]

Goal state after:
case mp
𝕜 : 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 : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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 : ℕ
⊢ ((∀ (m : ℕ),
        ↑m ≤ ↑n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x) ↔
    (∀ m ≤ n, Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ m < n, Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x

Tactic:
]

Goal state after:
𝕜 : 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 : ℕ
⊢ ((∀ (m : ℕ),
        ↑m ≤ ↑n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x) ↔
    (∀ m ≤ n, Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ m < n, Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)

Tactic:
]

Goal state after:
𝕜 : 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
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (fderiv 𝕜 f)

Tactic:
]

Goal state after:
𝕜 : 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
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (fderiv 𝕜 f)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb.inl.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
a : Fin c.length
⊢ c.partSize a = update (c.extendMiddle a).partSize a ((c.extendMiddle a).partSize a - 1) a

Tactic:
]

Goal state after:
case emb.inl.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
a : Fin c.length
⊢ c.partSize a = update (c.extendMiddle a).partSize a ((c.extendMiddle a).partSize a - 1) a
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb.inr.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.partSize a = update (c.extendMiddle i).partSize i ((c.extendMiddle i).partSize i - 1) a

Tactic:
]

Goal state after:
case emb.inr.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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.partSize a = update (c.extendMiddle i).partSize i ((c.extendMiddle i).partSize i - 1) a
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : IsEmpty (Algebra ℚ 𝔸)
x : 𝔸
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x = (expSeries 𝕂 𝔸).sum x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ exp x = (expSeries 𝕂 𝔸).sum x

Tactic:
rw [exp, dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩, ← @expSeries_sum_eq_rat (𝕂 := 𝕂)]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
⊢ (expSeries 𝕂 𝔸).sum = fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
⊢ (expSeries 𝕂 𝔸).sum = fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) = fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
⊢ ⟨c.eraseLeft h, none⟩.fst.extend ⟨c.eraseLeft h, none⟩.snd = c

Tactic:
]

Goal state after:
case pos
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
⊢ ⟨c.eraseLeft h, none⟩.fst.extend ⟨c.eraseLeft h, none⟩.snd = c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum 0 else 1) = 1

Tactic:
]

Goal state after:
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum 0 else 1) = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (MulOpposite.op x) = MulOpposite.op ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x)

Tactic:
]

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (MulOpposite.op x) = MulOpposite.op ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝¹⁰ : Ring 𝔸
inst✝⁹ : TopologicalSpace 𝔸
inst✝⁸ : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst✝⁷ : Monoid R
inst✝⁶ : SMul ℚ R
inst✝⁵ : MulAction R 𝔸
inst✝⁴ : Algebra ℚ 𝔸
inst✝³ : IsScalarTower ℚ R 𝔸
inst✝² : SetLike S 𝔸
inst✝¹ : SubsemiringClass S 𝔸
inst✝ : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst✝⁹] ↑s
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x ∈ s

Tactic:
]

Goal state after:
𝔸 : Type u_2
inst✝¹⁰ : Ring 𝔸
inst✝⁹ : TopologicalSpace 𝔸
inst✝⁸ : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst✝⁷ : Monoid R
inst✝⁶ : SMul ℚ R
inst✝⁵ : MulAction R 𝔸
inst✝⁴ : Algebra ℚ 𝔸
inst✝³ : IsScalarTower ℚ R 𝔸
inst✝² : SetLike S 𝔸
inst✝¹ : SubsemiringClass S 𝔸
inst✝ : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst✝⁹] ↑s
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x ∈ s
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)

Tactic:
]

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • x ^ n = (↑n !)⁻¹ • x ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝³ : DivisionRing 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝔸
⊢ (expSeries ℚ 𝔸).sum = fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !

Tactic:
]

Goal state after:
𝔸 : Type u_2
inst✝³ : DivisionRing 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝔸
⊢ (expSeries ℚ 𝔸).sum = fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable fun n ↦ ‖(↑n !)⁻¹ • x ^ n‖

Tactic:
change Summable (norm ∘ _)

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (↑n !)⁻¹ • x ^ n)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x)

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x) (exp x)

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x) (exp x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 0
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 exp x

Tactic:
]

Goal state after:
case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 0
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 exp x
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
⊢ ⟨c.eraseMiddle h, some (c.index 0)⟩.fst.extend ⟨c.eraseMiddle h, some (c.index 0)⟩.snd = c

Tactic:
]

Goal state after:
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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
⊢ ⟨c.eraseMiddle h, some (c.index 0)⟩.fst.extend ⟨c.eraseMiddle h, some (c.index 0)⟩.snd = c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ edist x 0 < (expSeries 𝕂 𝔸).radius

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ edist x 0 < (expSeries 𝕂 𝔸).radius
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hnx : -x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ f ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ f ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable fun n ↦ ‖x ^ n / ↑n !‖

Tactic:
change Summable (norm ∘ _)

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ x ^ n / ↑n !)