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

Goal state before:
pp: case e'_10
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1)) = fun x ↦ (p' x 0).curry0

Tactic:
ext x y
          change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y
          rw [init_snoc]

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

Goal state before:
pp: case e'_11
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x✝ s] x✝
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x✝
v✝ : Set E
hv : v✝ ∈ 𝓝[insert x✝ u] x✝
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v✝
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v✝
x : E
k : ℕ
v : Fin k → E
y : E
⊢ ((p' x k) (init (snoc v y))) (snoc v y (last k)) = ((p' x k) v) y

Tactic:
snoc_last,

Goal state after:
case e'_11
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x✝ s] x✝
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x✝
v✝ : Set E
hv : v✝ ∈ 𝓝[insert x✝ u] x✝
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v✝
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v✝
x : E
k : ℕ
v : Fin k → E
y : E
⊢ ((p' x k) (init (snoc v y))) y = ((p' x k) v) y
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
    ∃ u ∈ 𝓝[insert x (insert ?m.343 s)] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

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 : ℕ∞ω
hn : n ≠ ∞
⊢ E

Tactic:
insert_eq_of_mem (mem_insert _ _)

Goal state after:
case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
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,
    0 ∈ range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m)

pp: case refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
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
⊢ ∃ m,
    i.succ ∈
      range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m)

Tactic:
· simp only [mem_range]
      exact ⟨0, ⟨0, by simp⟩, by simp⟩

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
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
⊢ ∃ m,
    i.succ ∈
      range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn]

Goal state after:
case mpr
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ ↑n.factorial ≠ 0

Tactic:
norm_cast

Goal state after:
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ ¬n.factorial = 0
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}
⊢ StrictMono fun m ↦
    have this := ⋯;
    (c.emb (Fin.cast this m.succ) ⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩).pred ⋯

Tactic:
intro i

Goal state after:
𝕜 : 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)
⊢ ∀ ⦃b : Fin (c.length - 1)⦄,
    i < b →
      (fun m ↦
            have this := ⋯;
            (c.emb (Fin.cast this m.succ) ⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩).pred ⋯)
          i <
        (fun m ↦
            have this := ⋯;
            (c.emb (Fin.cast this m.succ) ⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩).pred ⋯)
          b
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)

Tactic:
intro i

Goal state after:
case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)
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 j : Fin c.length
hij : i < j
⊢ (fun m ↦
        if h : m = c.index 0 then
          (c.emb m (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb m (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m - 1, ⋯⟩)).pred ⋯)
      i <
    (fun m ↦
        if h : m = c.index 0 then
          (c.emb m (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb m (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m - 1, ⋯⟩)).pred ⋯)
      j

Tactic:
simp only [Fin.lt_def]

Goal state after:
𝕜 : 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 j : Fin c.length
hij : i < j
⊢ ↑(if h : i = c.index 0 then
        (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩.succ)).pred ⋯
      else (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩)).pred ⋯) <
    ↑(if h : j = c.index 0 then
        (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩.succ)).pred ⋯
      else (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩)).pred ⋯)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_3.inl
𝕜 : 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}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ ↑(c.emb (c.index 0) 0) < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
← lt_def

Goal state after:
case e'_3.inl
𝕜 : 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}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 < c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_4.inl
𝕜 : 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
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ ↑(c.emb (c.index 0) 0) < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
← lt_def

Goal state after:
case e'_4.inl
𝕜 : 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
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 < c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inr
𝕜 : 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
hi : i ≠ c.index 0
⊢ ∃ m y, (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

Tactic:
have A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i := by
        simp [hi]

Goal state after:
case inr
𝕜 : 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
hi : i ≠ c.index 0
A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i
⊢ ∃ m y, (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.emb
𝕜 : 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
⊢ ∀ (a : Fin (c.length - 1 + 1)) (a' : Fin c.length),
    a ≍ a' →
      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 ⋯) a ≍
        c.emb a'

Tactic:
intro i

Goal state after:
case pos.emb
𝕜 : 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)
⊢ ∀ (a' : Fin c.length),
    i ≍ a' →
      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 ≍
        c.emb a'
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg.emb
𝕜 : 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ ∀ (a : Fin c.length),
    (if h_1 : a = c.index 0 then
        (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
      else
        succ ∘
          (fun j ↦
              if h : a = c.index 0 then (c.emb a (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb a (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯) ≍
      c.emb a

Tactic:
intro i

Goal state after:
case neg.emb
𝕜 : 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
⊢ (if h_1 : i = c.index 0 then
      (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
    else
      succ ∘
        (fun j ↦ if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
          Fin.cast ⋯) ≍
    c.emb i
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ (expSeries 𝕂 𝔸).radius = ∞

Tactic:
apply expSeries_eq_ofScalars 𝕂 𝔸 ▸
    ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n ↦ ‖(↑n.succ !)⁻¹‖ / ‖(↑n !)⁻¹‖) atTop (𝓝 0)

𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
n : ℕ
⊢ (↑n !)⁻¹ ≠ 0
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
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
v : Fin n → E
⊢ ‖f (c.applyOrderedFinpartition p v)‖ ≤ ‖f‖ * ((∏ i, ‖p i‖) * ∏ i, ‖v i‖)

Tactic:
← c.prod_sigma_eq_prod,

Goal state after:
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
v : Fin n → E
⊢ ‖f (c.applyOrderedFinpartition p v)‖ ≤ ‖f‖ * ((∏ i, ‖p i‖) * ∏ m, ∏ r, ‖v (c.emb m r)‖)
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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
⊢ (q.compAlongOrderedFinpartition p (c.extend none)).curryLeft =
    ((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i ↦ p (c.partSize i)) ∘SL
      (q (c.length + 1)).curryLeft ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p 1)

Tactic:
by
  ext e v
  simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendLeft,
    ContinuousMultilinearMap.curryLeft_apply,
    FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
    ContinuousLinearMap.comp_apply, continuousMultilinearCurryFin1_apply,
    Matrix.zero_empty, ContinuousLinearMap.flipMultilinear_apply_apply,
    compAlongOrderedFinpartitionL_apply, compAlongOrderFinpartition_apply]
  congr
  ext j
  exact Fin.cases rfl (fun i ↦ rfl) j

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: ⊢ AnalyticOnNhd ℂ cexp univ

Tactic:
rw [Complex.exp_eq_exp_ℂ]

Goal state after:
⊢ AnalyticOnNhd ℂ NormedSpace.exp univ
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
rw [(by aesop : (∑ j ∈ u, f j) = (fun x ↦ ∑ j ∈ u, f j x))]
  induction u using Finset.cons_induction with
  | empty => simp
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n) f
c : 𝕜
⊢ (iteratedDeriv n fun x ↦ f (c * x)) = fun x ↦ c ^ n • iteratedDeriv n f (c * x)

Tactic:
funext x
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_comp_const_smul (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr h)
      c (Set.mapsTo_univ _ _)

Goal state after: