mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : Finite ι
val✝ : Fintype ι
⊢ Continuous ((toContinuousMultilinearMapCLM 𝕜).comp ∘ compContinuousLinearMapCLM)

Tactic:
change Continuous <|
    (toContinuousMultilinearMapCLM 𝕜 : (F [⋀^ι]→L[𝕜] G) →L[𝕜] _).precomp _ ∘
      ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜
        (fun _ : ι ↦ E) (fun _ ↦ F) G ∘
      (fun f _ ↦ f)

Goal state after:
𝕜 : 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✝ : Finite ι
val✝ : Fintype ι
⊢ Continuous
    (⇑(ContinuousLinearMap.precomp (ContinuousMultilinearMap 𝕜 (fun x ↦ E) G) (toContinuousMultilinearMapCLM 𝕜)) ∘
      ⇑(ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 (fun x ↦ E) (fun x ↦ F) G) ∘ fun f x ↦
        f)
Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM

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

Tactic:
have := Fintype.ofFinite ι
  simp [fderivWithin_continuousMultilinear_apply_const hxs hc]

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 t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ iteratedFDerivWithin 𝕜 0 f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 0 f t

Tactic:
exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy

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
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
⊢ HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x

Tactic:
rw [← hasFDerivWithinAt_univ]

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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) univ x
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
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDeriv 𝕜 (n + 1) f x) m =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y ↦ fderiv 𝕜 f y) x) m

Tactic:
iteratedFDeriv_succ_apply_right,

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
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (init m)) (m (last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y ↦ fderiv 𝕜 f y) x) m
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
x : E
m : Fin 1 → E
⊢ (iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)

Tactic:
iteratedFDeriv_succ_apply_right,

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
x : E
m : Fin 1 → E
⊢ ((iteratedFDeriv 𝕜 0 (fun y ↦ fderiv 𝕜 f y) x) (init m)) (m (last 0)) = (fderiv 𝕜 f x) (m 0)
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
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s

Tactic:
by
  induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_analyticOnNhd h
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
    convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
    case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
    simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ deriv (fun y ↦ c • f y) x = c • deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_fun_const_smul_field]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasStrictFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

Tactic:
by
  convert! (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt
  exact (fderiv_inverse x).symm

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun x ↦ f (x + a)) x = deriv f (x + a)

Tactic:
simpa [add_comm] using deriv_comp_const_add f a x

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

Goal state before:
pp: case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (Inv.inv ∘ fun x ↦ x ^ (-m)) ((↑(-m) * x ^ (-m - 1)) • -((x ^ (-m)) ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
simp only [Function.comp_def, zpow_neg, inv_inv, smul_eq_mul] at this

Goal state after:
case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * x ^ (-m - 1) * x ^ (m + m)

Tactic:
mul_assoc,

Goal state after:
case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * (x ^ (-m - 1) * x ^ (m + m))
Module: Mathlib.Analysis.Calculus.ContDiff.RCLike

Goal state before:
pp: 𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
⊢ LocallyLipschitz f

Tactic:
intro x
  rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩
  use K, t

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.fst 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
simp [Function.comp_def]

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

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.snd 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
simp [Function.comp_def]

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 : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
← contDiffWithinAt_insert,

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 : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (insert ?m.52 (s \ {y})) x ↔ ContDiffWithinAt 𝕜 n f s x

𝕜 : 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 : ℕ∞ω
y : E
⊢ E
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr.refine_2.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 ≠ ∞
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
⊢ HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1))
    (fun x ↦ ((p' x).unshift (f x)).shift) (v ∩ u)

Tactic:
· convert! (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1
        · 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]
        · ext x k v y
          change p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y))
            (@snoc k (fun _ : Fin k.succ => E) v y (last k)) = p' x k v y
          rw [snoc_last, init_snoc]

Goal state after:
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) →
    ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
← contDiffWithinAt_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) →
    ContDiffWithinAt 𝕜 (n + 1) f (insert ?m.343 s) x

𝕜 : 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
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case succ.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✝ c : OrderedFinpartition n
j i : Fin c.length
a✝¹ :
  (i.castSucc < j.castSucc →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.castSucc) →
    i.castSucc < j.succ →
      (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          i.castSucc <
        (fun m ↦
            cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
              ⟨cons 1 c.partSize m - 1, ⋯⟩)
          j.succ
a✝ :
  i.succ < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i.succ <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i.succ < j.succ
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i.succ <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      j.succ

Tactic:
simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]
        exact c.parts_strictMono (by simpa using hij)

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

Goal state before:
pp: case 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✝ c : OrderedFinpartition n
m : Fin c.length
⊢ ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'

Tactic:
intro a' b' h'

Goal state after:
case 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✝ c : OrderedFinpartition n
m : Fin c.length
a' b' : Fin (c.partSize m + 1)
h' : a' < b'
⊢ cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
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
⊢ Fin n

Tactic:
refine Fin.pred (c.emb (Fin.cast this (succ i)) j) ?_

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)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this : c.length - 1 + 1 = c.length
⊢ c.emb (Fin.cast this i.succ) j ≠ 0
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inl
𝕜 : 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
⊢ ContDiffWithinAt 𝕜 (↑m) f s x

Tactic:
apply ContDiffWithinAt.of_le _ (show (m : ℕ∞ω) ≤ m + 1 from le_self_add)

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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑m + 1) f s x
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
f : E → F
x : E
n : ℕ
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x) →
    ∃ u ∈ 𝓝 x,
      (↑n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x

Tactic:
· rintro ⟨f', ⟨u, H, h_fderiv⟩, h_cont_diff⟩
    refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.contDiffWithinAt⟩
    exact (h_fderiv x hxu).hasFDerivWithinAt

Goal state after:
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
f : E → F
n : ℕ∞ω
⊢ ContDiff 𝕜 ω f → ContDiffOn 𝕜 ω f univ

Tactic:
rintro ⟨p, hp, h'p⟩ x _

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p : ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x ↦ p x i) univ
x : E
a✝ : x ∈ univ
⊢ ContDiffWithinAt 𝕜 ω f univ 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
x : E
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ∃ u ∈ 𝓝 x, ContinuousOn f' u) ↔
    ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Tactic:
exists_mem_and_iff antitone_bforall antitone_continuousOn,

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
x : E
⊢ (∃ f', ∃ u ∈ 𝓝 x, (∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContinuousOn f' u) ↔
    ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
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
⊢ ∃ m,
    x ∈
      range fun j ↦ if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯

Tactic:
by
    simp only [mem_range]
    obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
      ⟨c.index (succ x), c.invEmbedding (succ x), by simp⟩
    rcases eq_or_ne i (c.index 0) with rfl | hi
    · refine ⟨c.index 0, ?_⟩
      have j_ne : j ≠ 0 := by
        rintro rfl
        simp only [c.emb_zero] at hij
        exact (Fin.succ_ne_zero _).symm hij
      have je_ne' : (j : ℕ) ≠ 0 := by simpa
      simp only [↓reduceDIte]
      have A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
        Nat.sub_add_cancel (c.partSize_pos _)
      have B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
        c.partSize (c.index 0) - 1 := by simp
      refine ⟨Fin.cast B.symm (pred (Fin.cast A.symm j) ?_), ?_⟩
      · simpa using j_ne
      · have : x = pred (succ x) (succ_ne_zero x) := rfl
        rw [this]
        simp only [pred_inj, ← hij]
        congr 1
        rw [← val_eq_val]
        simp only [val_cast, val_succ, val_pred]
        omega
    · have A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i := by
        simp [hi]
      exact ⟨i, Fin.cast A.symm j, by simp [hi, hij]⟩

Goal state after: