internlm/Lean-Github huggingface dataset:
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update (fun x => f x) (↑i) 1 ↑j
Tactic:
simp only [← Function.comp_apply (g := Subtype.val) (x := j)]
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = (Function.update (fun x => f x) (↑i) 1 ∘ Subtype.val) j
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = (Function.update (fun x => f x) (↑i) 1 ∘ Subtype.val) j
Tactic:
rw [Function.update_comp_eq_of_injective _ Subtype.val_injective]
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update ((fun x => f x) ∘ Subtype.val) i 1 j
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update ((fun x => f x) ∘ Subtype.val) i 1 j
Tactic:
rfl
Proof state after:
no goals
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
Tactic:
induction i generalizing x with
| zero => ext; simp
| succ i IH =>
  ext m
  rw [iteratedFDerivWithin_succ_apply_left, fderivWithin_congr (fun _ ↦ IH) (IH hx)]
  rw [fderivWithin_const_apply _ (hs x hx)]
  rfl
Proof state after:
no goals
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case zero
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 Nat.zero (fun x => 0) s x = 0
Tactic:
ext
Proof state after:
case zero.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
x✝ : Fin Nat.zero → E
⊢ (iteratedFDerivWithin 𝕜 Nat.zero (fun x => 0) s x) x✝ = 0 x✝
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case zero.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
x✝ : Fin Nat.zero → E
⊢ (iteratedFDerivWithin 𝕜 Nat.zero (fun x => 0) s x) x✝ = 0 x✝
Tactic:
simp
Proof state after:
no goals
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case succ
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (Nat.succ i) (fun x => 0) s x = 0
Tactic:
ext m
Proof state after:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ (iteratedFDerivWithin 𝕜 (Nat.succ i) (fun x => 0) s x) m = 0 m
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ (iteratedFDerivWithin 𝕜 (Nat.succ i) (fun x => 0) s x) m = 0 m
Tactic:
rw [iteratedFDerivWithin_succ_apply_left, fderivWithin_congr (fun _ ↦ IH) (IH hx)]
Proof state after:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ ((fderivWithin 𝕜 (fun x => 0) s x) (m 0)) (Fin.tail m) = 0 m
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ ((fderivWithin 𝕜 (fun x => 0) s x) (m 0)) (Fin.tail m) = 0 m
Tactic:
rw [fderivWithin_const_apply _ (hs x hx)]
Proof state after:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ (0 (m 0)) (Fin.tail m) = 0 m
Theorem: iteratedFDerivWithin_zero_fun
Proof state before:
case succ.H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
x : E
hx : x ∈ s
m : Fin (Nat.succ i) → E
⊢ (0 (m 0)) (Fin.tail m) = 0 m
Tactic:
rfl
Proof state after:
no goals
Theorem: iteratedFDerivWithin_succ_const
Proof state before:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s x = 0
Tactic:
ext m
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s x) m = 0 m
Theorem: iteratedFDerivWithin_succ_const
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s x) m = 0 m
Tactic:
rw [iteratedFDerivWithin_succ_apply_right hs hx]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 (fun x => c) s y) s x) (Fin.init m)) (m (Fin.last n)) = 0 m
Theorem: iteratedFDerivWithin_succ_const
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 (fun x => c) s y) s x) (Fin.init m)) (m (Fin.last n)) = 0 m
Tactic:
rw [iteratedFDerivWithin_congr (fun y hy ↦ fderivWithin_const_apply c (hs y hy)) hx]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => 0) s x) (Fin.init m)) (m (Fin.last n)) = 0 m
Theorem: iteratedFDerivWithin_succ_const
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => 0) s x) (Fin.init m)) (m (Fin.last n)) = 0 m
Tactic:
rw [iteratedFDerivWithin_zero_fun hs hx]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (0 (Fin.init m)) (m (Fin.last n)) = 0 m
Theorem: iteratedFDerivWithin_succ_const
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (0 (Fin.init m)) (m (Fin.last n)) = 0 m
Tactic:
simp [ContinuousMultilinearMap.zero_apply (R := 𝕜)]
Proof state after:
no goals
Theorem: iteratedFDerivWithin_const_of_ne
Proof state before:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : n ≠ 0
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n (fun x => c) s x = 0
Tactic:
cases n with
| zero => contradiction
| succ n => exact iteratedFDerivWithin_succ_const _ _ hs hx
Proof state after:
no goals
Theorem: iteratedFDerivWithin_const_of_ne
Proof state before:
case zero
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : Nat.zero ≠ 0
⊢ iteratedFDerivWithin 𝕜 Nat.zero (fun x => c) s x = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: iteratedFDerivWithin_const_of_ne
Proof state before:
case succ
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c✝ : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
c : F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : Nat.succ n ≠ 0
⊢ iteratedFDerivWithin 𝕜 (Nat.succ n) (fun x => c) s x = 0
Tactic:
exact iteratedFDerivWithin_succ_const _ _ hs hx
Proof state after:
no goals
Theorem: iteratedFDerivWithin_sum_apply
Proof state before:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
induction u using Finset.induction with
| empty => ext; simp [hs, hx]
| @insert a u ha IH =>
  simp only [Finset.mem_insert] at h
  simp only [Finset.mem_insert, forall_eq_or_imp] at h
  simp only [Finset.sum_insert ha]
  rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffOn.sum h.2) hs hx, IH h.2]
Proof state after:
no goals
Theorem: iteratedFDerivWithin_sum_apply
Proof state before:
case empty
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x = ∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
ext
Proof state after:
case empty.H
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝¹ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x) x✝ = (∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝
Theorem: iteratedFDerivWithin_sum_apply
Proof state before:
case empty.H
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝¹ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x) x✝ = (∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝
Tactic:
simp [hs, hx]
Proof state after:
no goals