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

Goal state before:
pp: case inl.succ.zero
𝕜 : 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✝ c : OrderedFinpartition n
m : Fin c.length
b : Fin (c.partSize m)
a✝ : 0 < b.castSucc → cases 0 (succ ∘ c.emb m) 0 < cases 0 (succ ∘ c.emb m) b.castSucc
h' : 0 < b.succ
⊢ cases 0 (succ ∘ c.emb m) 0 < cases 0 (succ ∘ c.emb m) b.succ

Tactic:
simp

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

Goal state before:
pp: case inl.zero
𝕜 : 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✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
a' : Fin (c.partSize i)
⊢ (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) 0

Tactic:
simp

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

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
k : Fin c.length
⊢ 0 < update c.partSize k (c.partSize k + 1) k

Tactic:
simp

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

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
k : Fin c.length
⊢ (if h : k = k then (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast ⋯ else succ ∘ c.emb k ∘ Fin.cast ⋯) ⟨0, ⋯⟩ = 0

Tactic:
simp

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

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
i : Fin n
⊢ update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) = c.partSize (c.index i) + 1

Tactic:
simp

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

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
s : Set E
f : E → F
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)

Tactic:
exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm

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

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
i : Fin n
A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) = c.partSize (c.index i) + 1
⊢ (if h : c.index i = c.index i then (fun i_1 ↦ cases 0 (succ ∘ c.emb (c.index i)) i_1) ∘ Fin.cast ⋯
      else succ ∘ c.emb (c.index i) ∘ Fin.cast ⋯)
      (Fin.cast ⋯ (c.invEmbedding i).succ) =
    i.succ

Tactic:
simp

Goal state after:
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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ↑m = ∞ → n = ω

Tactic:
simp

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

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
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}
i : Fin (c.length - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this✝ : c.length - 1 + 1 = c.length
this : (Disjoint on fun m ↦ range (c.emb m)) (Fin.cast this✝ i.succ) 0
⊢ c.emb (Fin.cast this✝ i.succ) j ∈ (fun m ↦ range (c.emb m)) (Fin.cast this✝ i.succ)

Tactic:
simp

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

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
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
⊢ c.emb (c.index x.succ) (c.invEmbedding x.succ) = x.succ

Tactic:
simp

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

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
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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
⊢ c.partSize i = c.partSize (Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ)

Tactic:
simp

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

Goal state before:
pp: case e_3
𝕜 : 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
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ = i

Tactic:
simp

Goal state after:
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
x : E
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : ↑m + 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1)) f t
A : t =ᶠ[𝓝[≠] x] s
B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t
C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) t x
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
rw [differentiableWithinAt_congr_set' _ A] at C

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
x : E
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : ↑m + 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1)) f t
A : t =ᶠ[𝓝[≠] x] s
B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t
C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) s x
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s 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
s : Set E
f : E → F
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s) ↔
    (∀ m ≤ n, ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simp

Goal state after:
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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ↑m ≠ ∞

Tactic:
simp

Goal state after:
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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ↑m = ω → AnalyticOn 𝕜 f s

Tactic:
simp

Goal state after:
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
⊢ n + 1 ≠ 0

Tactic:
simp

Goal state after:
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this✝ : ContDiffWithinAt 𝕜 (↑m) f' s x
this : s ∩ o ∈ 𝓝[s] x
y : E
hy : y ∈ s ∩ o
⊢ fderivWithin 𝕜 f s y = f' y

Tactic:
have A : fderivWithin 𝕜 f (s ∩ o) y = f' y :=
      ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open y hy)

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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this✝ : ContDiffWithinAt 𝕜 (↑m) f' s x
this : s ∩ o ∈ 𝓝[s] x
y : E
hy : y ∈ s ∩ o
A : fderivWithin 𝕜 f (s ∩ o) y = f' y
⊢ fderivWithin 𝕜 f s y = f' y
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
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderivWithin 𝕜 f s) s

Tactic:
simp

Goal state after:
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderiv 𝕜 f) s

Tactic:
simp

Goal state after:
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
x : E
n : ℕ
⊢ ↑n ≠ ∞

Tactic:
simp

Goal state after:
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
x : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n) f' x
u : Set E
H : u ∈ 𝓝 x
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ↑n = ω → AnalyticOn 𝕜 f u

Tactic:
simp

Goal state after:
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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ ↑n = ∞ → ↑n = ω

Tactic:
simp

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

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
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
⊢ c.emb (c.index x.succ) (c.invEmbedding x.succ) = x.succ

Tactic:
simp

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

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
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)
⊢ update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1

Tactic:
simp

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

Goal state before:
pp: case e'_2
𝕜 : 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
x✝ : E → E →L[𝕜] F
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] x✝ ↔ ContDiff 𝕜 (↑0) x✝

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
h : IsEmpty (Algebra ℚ 𝔸)
this : IsEmpty (Algebra ℚ 𝔸ᵐᵒᵖ)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
simp

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

Goal state before:
pp: case h
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
X✝ : 𝔸
⊢ exp (MulOpposite.unop (MulOpposite.op X✝)) = MulOpposite.unop (exp (MulOpposite.op X✝))

Tactic:
simp

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

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝⁵ : Ring 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h✝ : IsEmpty (Algebra ℚ 𝔸)
⊢ star (exp x) = exp (star x)

Tactic:
simp

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

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
h✝ : IsEmpty (Algebra ℚ 𝔸)
⊢ Commute x (exp y)

Tactic:
simp

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

Goal state before:
pp: case pos.emb.refine_1.succ
𝕜 : 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
i : Fin (c.length - 1)
a✝ :
  i.castSucc ≍ Fin.cast A i.castSucc →
    cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i.castSucc = c.partSize (Fin.cast A i.castSucc)
h' : i.succ ≍ Fin.cast A i.succ
⊢ cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i.succ = c.partSize (Fin.cast A i.succ)

Tactic:
simp

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

Goal state before:
pp: case pos.emb.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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ ∀ (i_1 : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i)),
    cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
        (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i i_1 =
      c.emb (Fin.cast A i) ⟨↑i_1, ⋯⟩

Tactic:
intro j

Goal state after:
case pos.emb.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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i)
⊢ cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
      (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i j =
    c.emb (Fin.cast A i) ⟨↑j, ⋯⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.emb.refine_2.succ
𝕜 : 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
i : Fin (c.length - 1)
a✝ :
  ∀ (h' : i.castSucc ≍ Fin.cast A i.castSucc) (j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i.castSucc)),
    cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
        (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i.castSucc j =
      c.emb (Fin.cast A i.castSucc) ⟨↑j, ⋯⟩
h' : i.succ ≍ Fin.cast A i.succ
j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i.succ)
⊢ cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
      (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i.succ j =
    c.emb (Fin.cast A i.succ) ⟨↑j, ⋯⟩

Tactic:
simp

Goal state after: