internlm/Lean-Github huggingface dataset:
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
⊢ ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
Tactic:
induction n generalizing m with
| zero =>
  rw [orderedIteratedFPiDeriv_zero_eq_comp]
  simp at hn
  exact (LinearIsometryEquiv.contDiff _).comp (hf.of_le hn)
| succ n ih =>
  rw [orderedIteratedFPiDeriv_succ_eq_comp_left]
  refine ContDiff.comp ?_ ?_
  . exact LinearIsometryEquiv.contDiff _  have hn' : n < N  . simp at hn
    rw [← add_assoc] at hn
    refine lt_of_lt_of_le ?_ hn
    rw [← ENat.add_one_le_iff (ENat.coe_ne_top n)]
    rw [add_assoc]
    exact le_add_self
  conv =>
    arg 3; intro x
    rw [fpideriv_eq_fderiv_comp_single (hf.differentiable_orderedIteratedFPiDeriv hn' _)]
  refine ContDiff.clm_comp ?_ contDiff_const
  specialize @ih (m + 1) ?_
  . rw [add_assoc]
    rw [add_comm 1]
    exact hn
  exact ContDiff.fderiv_right ih (le_refl _)
Proof state after:
no goals
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
m : ℕ∞
hn : m + ↑Nat.zero ≤ N
js : Fin Nat.zero → ι
⊢ ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
Tactic:
rw [orderedIteratedFPiDeriv_zero_eq_comp]
Proof state after:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
m : ℕ∞
hn : m + ↑Nat.zero ≤ N
js : Fin Nat.zero → ι
⊢ ContDiff 𝕜 m (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
m : ℕ∞
hn : m + ↑Nat.zero ≤ N
js : Fin Nat.zero → ι
⊢ ContDiff 𝕜 m (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
Tactic:
simp at hn
Proof state after:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
m : ℕ∞
js : Fin Nat.zero → ι
hn : m ≤ N
⊢ ContDiff 𝕜 m (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
m : ℕ∞
js : Fin Nat.zero → ι
hn : m ≤ N
⊢ ContDiff 𝕜 m (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
Tactic:
exact (LinearIsometryEquiv.contDiff _).comp (hf.of_le hn)
Proof state after:
no goals
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
Tactic:
rw [orderedIteratedFPiDeriv_succ_eq_comp_left]
Proof state after:
case succ
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun i => M (js i)) F) ∘
      fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun i => M (js i)) F) ∘
      fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Tactic:
refine ContDiff.comp ?_ ?_
Proof state after:
case succ.refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun i => M (js i)) F)

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun i => M (js i)) F)

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Tactic:
. exact LinearIsometryEquiv.contDiff _
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Tactic:
have hn' : n < N
Proof state after:
case hn'
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ↑n < N

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case hn'
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
⊢ ↑n < N

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Tactic:
. simp at hn
  rw [← add_assoc] at hn
  refine lt_of_lt_of_le ?_ hn
  rw [← ENat.add_one_le_iff (ENat.coe_ne_top n)]
  rw [add_assoc]
  exact le_add_self
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m (fpideriv 𝕜 (js 0) (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f))
Tactic:
conv =>
  arg 3; intro x
  rw [fpideriv_eq_fderiv_comp_single (hf.differentiable_orderedIteratedFPiDeriv hn' _)]
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m fun x =>
    ContinuousLinearMap.comp (fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x)
      (ContinuousLinearMap.single (js 0))
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m fun x =>
    ContinuousLinearMap.comp (fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x)
      (ContinuousLinearMap.single (js 0))
Tactic:
refine ContDiff.clm_comp ?_ contDiff_const
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Tactic:
specialize @ih (m + 1) ?_
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ m + 1 + ↑n ≤ N

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
ih : ∀ {js : Fin n → ι}, ContDiff 𝕜 (m + 1) (orderedIteratedFPiDeriv 𝕜 js f)
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
ih : ∀ {m : ℕ∞}, m + ↑n ≤ N → ∀ {js : Fin n → ι}, ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
⊢ m + 1 + ↑n ≤ N

case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
ih : ∀ {js : Fin n → ι}, ContDiff 𝕜 (m + 1) (orderedIteratedFPiDeriv 𝕜 js f)
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Tactic:
. rw [add_assoc]
  rw [add_comm 1]
  exact hn
Proof state after:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
ih : ∀ {js : Fin n → ι}, ContDiff 𝕜 (m + 1) (orderedIteratedFPiDeriv 𝕜 js f)
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Theorem: ContDiff.orderedIteratedFPiDeriv_right
Proof state before:
case succ.refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
N : ℕ∞
hf : ContDiff 𝕜 N f
n : ℕ
m : ℕ∞
hn : m + ↑(Nat.succ n) ≤ N
js : Fin (Nat.succ n) → ι
hn' : ↑n < N
ih : ∀ {js : Fin n → ι}, ContDiff 𝕜 (m + 1) (orderedIteratedFPiDeriv 𝕜 js f)
⊢ ContDiff 𝕜 m fun x => fderiv 𝕜 (orderedIteratedFPiDeriv 𝕜 (Fin.tail js) f) x
Tactic:
exact ContDiff.fderiv_right ih (le_refl _)
Proof state after:
no goals