awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m + (↑0 : ℕ∞ω) ≤ n
⊢ m ≤ n

Tactic:
simp only [CharP.cast_eq_zero, add_zero] at hmn

Premises used: CharP.cast_eq_zero, add_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 0 f s) s x₀

Tactic:
(hf.of_le hmn).continuousLinearMap_comp
      ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.continuousLinearMap_comp, iteratedFDerivWithin, ContinuousMultilinearMap.constOfIsEmpty, ContinuousMultilinearMap.uncurry0
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 0 f s) s x₀

Tactic:
exact (hf.of_le hmn).continuousLinearMap_comp
      ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.continuousLinearMap_comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
i : ℕ
hi :
  ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 i f s) s x₀
m : ℕ∞ω
hmn : m + (↑(i + 1) : ℕ∞ω) ≤ n
⊢ m + 1 + (↑i : ℕ∞ω) ≤ n

Tactic:
rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn

Premises used: Nat.cast_succ, add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
i : ℕ
hi :
  ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 i f s) s x₀
m : ℕ∞ω
hmn : m + 1 + (↑i : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 (i + 1) f s) s x₀

Tactic:
((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
      ((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm :
        _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)

Premises used: ContinuousLinearMap.uncurryLeft, le_rfl, ContDiffWithinAt.continuousLinearMap_comp, iteratedFDerivWithin, MultilinearMap.mkContinuous, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
i : ℕ
hi :
  ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 i f s) s x₀
m : ℕ∞ω
hmn : m + 1 + (↑i : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 (i + 1) f s) s x₀

Tactic:
exact ((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
      ((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm :
        _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)

Premises used: le_rfl, ContDiffWithinAt.continuousLinearMap_comp, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + (↑i : ℕ∞ω) ≤ n
hx₀s : x₀ ∈ s
zero :
  ∀ {m : ℕ∞ω} (hmn : m + (↑0 : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 0 f s) s x₀
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ {m : ℕ∞ω} (hmn : m + (↑i : ℕ∞ω) ≤ n),
        ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
          (iteratedFDerivWithin 𝕜 i f s) s x₀)
    {m : ℕ∞ω} (hmn : m + (↑(i + 1) : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 (i + 1) f s) s x₀
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f s) s x₀

Tactic:
induction i generalizing m with
  | zero =>
    simp only [CharP.cast_eq_zero, add_zero] at hmn
    exact (hf.of_le hmn).continuousLinearMap_comp
      ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)
  | succ i hi =>
    rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn
    exact ((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
      ((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm :
        _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)

Premises used: CharP.cast_eq_zero, Nat.cast_succ, ContDiffWithinAt.of_le, add_assoc, ContDiffWithinAt.continuousLinearMap_comp, add_comm, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
simp_rw : ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderiv 𝕜 (f x) (g x)) x₀

Tactic:
simp_rw [← fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀

Tactic:
(ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    hmn (mem_univ x₀) ?_).contDiffAt univ_mem

Premises used: ContDiffWithinAt.contDiffAt, uniqueDiffOn_univ, Set.mem_univ, ContDiffWithinAt.fderivWithin, Filter.univ_mem, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
refine : univ ⊆ g ⁻¹' univ
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀

Tactic:
refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    hmn (mem_univ x₀) ?_).contDiffAt univ_mem

Premises used: ContDiffWithinAt.contDiffAt, uniqueDiffOn_univ, Set.mem_univ, ContDiffWithinAt.fderivWithin, Filter.univ_mem, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
rw rw₁ : Subset.{u_2} (α := Set E) univ univ
⊢ univ ⊆ g ⁻¹' univ

Tactic:
rw [preimage_univ]

Premises used: Set.preimage_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x₀ : E
m : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 (m + 1) (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) m (fun (x : E) ↦ fderiv 𝕜 (f x) (g x)) x₀

Tactic:
ContDiffAt.fderiv hf hg (le_refl _)

Premises used: le_refl, ContDiffAt.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 (F := E →L[𝕜] F) m (fderiv 𝕜 f) x₀

Tactic:
ContDiffAt.fderiv (ContDiffAt.comp (x₀, x₀) hf contDiffAt_snd) contDiffAt_id hmn

Premises used: contDiffAt_snd, Prod.mk, contDiffAt_id, ContDiffAt.fderiv, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 (n + 1) f x₀
⊢ ContDiffAt 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) x₀

Tactic:
ContDiffAt.fderiv (ContDiffAt.comp (x₀, x₀) hf contDiffAt_snd) contDiffAt_id (le_refl (n + 1))

Premises used: contDiffAt_snd, le_refl, Prod.mk, HAdd.hAdd, contDiffAt_id, ContDiffAt.fderiv, ContDiffAt.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffAt 𝕜 n f x₀
hmn : m + (↑i : ℕ∞ω) ≤ n
rw :
  ∀ (hf : ContDiffWithinAt 𝕜 n f univ x₀) (hmn : m + (↑i : ℕ∞ω) ≤ n),
    ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
      (iteratedFDerivWithin 𝕜 i f univ) univ x₀
⊢ ContDiffAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m (iteratedFDeriv 𝕜 i f) x₀

Tactic:
rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffWithinAt 𝕜 n f univ x₀
hmn : m + (↑i : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f univ) univ x₀

Tactic:
hf.iteratedFDerivWithin_right uniqueDiffOn_univ hmn trivial

Premises used: trivial, uniqueDiffOn_univ, ContDiffWithinAt.iteratedFDerivWithin_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffWithinAt 𝕜 n f univ x₀
hmn : m + (↑i : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f univ) univ x₀

Tactic:
exact hf.iteratedFDerivWithin_right uniqueDiffOn_univ hmn trivial

Premises used: trivial, uniqueDiffOn_univ, ContDiffWithinAt.iteratedFDerivWithin_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiff 𝕜 m (uncurry f)
hg : ContDiff 𝕜 n g
hnm : n + 1 ≤ m
⊢ ContDiff 𝕜 (F := F →L[𝕜] G) n fun (x : E) ↦ fderiv 𝕜 (f x) (g x)

Tactic:
contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt hnm

Premises used: Iff.mpr, ContDiffAt.fderiv, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiff 𝕜 (n + 1) (uncurry f)
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 (F := F →L[𝕜] G) n fun (x : E) ↦ fderiv 𝕜 (f x) (g x)

Tactic:
contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt (le_refl (n + 1))

Premises used: Iff.mpr, le_refl, HAdd.hAdd, ContDiffAt.fderiv, OfNat.ofNat, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
m n : ℕ∞ω
hf : ContDiff 𝕜 n f
hmn : m + 1 ≤ n
⊢ ContDiff 𝕜 (F := E →L[𝕜] F) m (fderiv 𝕜 f)

Tactic:
contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.fderiv_right hmn

Premises used: Iff.mpr, ContDiffAt.fderiv_right, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
m n : ℕ∞ω
i : ℕ
hf : ContDiff 𝕜 n f
hmn : m + (↑i : ℕ∞ω) ≤ n
⊢ ContDiff 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m (iteratedFDeriv 𝕜 i f)

Tactic:
contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.iteratedFDeriv_right hmn

Premises used: Iff.mpr, ContDiffAt.iteratedFDeriv_right, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
m : ℕ∞ω
i : ℕ
hf : ContDiff 𝕜 (m + (↑i : ℕ∞ω)) f
⊢ ContDiff 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m (iteratedFDeriv 𝕜 i f)

Tactic:
contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.iteratedFDeriv_right (le_refl _)

Premises used: Iff.mpr, le_refl, ContDiffAt.iteratedFDeriv_right, Nat.cast, HAdd.hAdd, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiff 𝕜 n (uncurry f)
hg :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hn : 1 ≤ n
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ _root_.fderiv 𝕜 (f x) (g x)

Tactic:
(hf.fderiv (contDiff_zero.mpr hg) hn).continuous

Premises used: Iff.mpr, contDiff_zero, ContDiff.continuous, ContDiff.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F → G
g : E → F
hf : ContDiff 𝕜 1 (uncurry f)
hg :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ _root_.fderiv 𝕜 (f x) (g x)

Tactic:
(hf.fderiv (contDiff_zero.mpr hg) (le_refl 1)).continuous

Premises used: Iff.mpr, le_refl, contDiff_zero, ContDiff.continuous, OfNat.ofNat, ContDiff.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F → G
g : E → F
hf : ContDiff 𝕜 2 (uncurry f)
hg : ContDiff 𝕜 1 g
⊢ Differentiable 𝕜 (F := F →L[𝕜] G) fun (x : E) ↦ fderiv 𝕜 (f x) (g x)

Tactic:
ContDiff.differentiable
    (contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt (le_refl 2))
    one_ne_zero

Premises used: Iff.mpr, le_refl, ContDiffAt.fderiv, ContDiff.differentiable, one_ne_zero, OfNat.ofNat, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ∞ω
f : E → F → G
g k : E → F
hf : ContDiff 𝕜 m (uncurry f)
hg : ContDiff 𝕜 n g
hk : ContDiff 𝕜 n k
hnm : n + 1 ≤ m
⊢ ContDiff.{u_1, u_2, u_4} 𝕜 (F := G) n fun (x : E) ↦ (fderiv 𝕜 (f x) (g x) : (a : F) → G) (k x)

Tactic:
(hf.fderiv hg hnm).clm_apply hk

Premises used: ContDiff.clm_apply, ContDiff.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
s : Set E
f : E → F
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderivWithin 𝕜 f s p.1 : (a : E) → F) p.2)
    (SProd.sprod (β := Set E) s univ)

Tactic:
((hf.fderivWithin hs hmn).comp contDiffOn_fst (prod_subset_preimage_fst _ _)).clm_apply
    contDiffOn_snd

Premises used: ContDiffOn.clm_apply, ContDiffOn.comp, contDiffOn_fst, Set.prod_subset_preimage_fst, ContDiffOn.fderivWithin, contDiffOn_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 1 ≤ n
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (p : E × E) ↦ (fderivWithin 𝕜 f s p.1 : (a : E) → F) p.2)
    (SProd.sprod (β := Set E) s univ)

Tactic:
(contDiffOn_fderivWithin_apply (m := 0) hf hs hn).continuousOn

Premises used: setOf, ContDiffOn.continuousOn, contDiffOn_fderivWithin_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiff 𝕜 n f
hmn : m + 1 ≤ n
rw :
  ∀ (hf : ContDiffOn 𝕜 n f univ) (hmn : m + 1 ≤ n),
    ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2) univ
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) m fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2

Tactic:
rw [← contDiffOn_univ] at hf ⊢

Premises used: contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
rw :
  ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderivWithin 𝕜 f univ p.1 : (a : E) → F) p.2)
    (SProd.sprod (α := Set E) (β := Set E) univ univ)
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2) univ

Tactic:
rw [← fderivWithin_univ, ← univ_prod_univ]

Premises used: fderivWithin_univ, Set.univ_prod_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderivWithin 𝕜 f univ p.1 : (a : E) → F) p.2)
    (SProd.sprod (α := Set E) (β := Set E) univ univ)

Tactic:
contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn

Premises used: uniqueDiffOn_univ, contDiffOn_fderivWithin_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderivWithin 𝕜 f univ p.1 : (a : E) → F) p.2)
    (SProd.sprod (α := Set E) (β := Set E) univ univ)

Tactic:
exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn

Premises used: uniqueDiffOn_univ, contDiffOn_fderivWithin_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hn : n ≠ 0
hx : x ∈ s
⊢ HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n

Tactic:
simpa [ENat.one_le_iff_ne_zero_withTop]

Premises used: ENat.one_le_iff_ne_zero_withTop
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : n ≠ 0
⊢ HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n

Tactic:
simpa [ENat.one_le_iff_ne_zero_withTop]

Premises used: ENat.one_le_iff_ne_zero_withTop