internlm/Lean-Github huggingface dataset:
Theorem: SciLean.ContCDiff.comp_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_2
inst✝³ : Vec K Y
Z : Type u_3
inst✝² : Vec K Z
ι : Type ?u.5109
inst✝¹ : IndexType ι
E : ι → Type ?u.5118
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : ContCDiff K n f
hg : ContCDiff K n g
⊢ ContCDiff K n fun x => f (g x)
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_2
inst✝³ : Vec K Y
Z : Type u_3
inst✝² : Vec K Z
ι : Type ?u.5109
inst✝¹ : IndexType ι
E : ι → Type ?u.5118
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : ContCDiff K n f
hg : ContCDiff K n g
x : X
⊢ ContCDiffAt K n (fun x => f (g x)) x
Theorem: SciLean.ContCDiff.comp_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_2
inst✝³ : Vec K Y
Z : Type u_3
inst✝² : Vec K Z
ι : Type ?u.5109
inst✝¹ : IndexType ι
E : ι → Type ?u.5118
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : ContCDiff K n f
hg : ContCDiff K n g
x : X
⊢ ContCDiffAt K n (fun x => f (g x)) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.ContCDiff.apply_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type ?u.5644
inst✝⁴ : Vec K X
Y : Type ?u.5657
inst✝³ : Vec K Y
Z : Type ?u.5668
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ ContCDiff K n fun x => x i
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type ?u.5644
inst✝⁴ : Vec K X
Y : Type ?u.5657
inst✝³ : Vec K Y
Z : Type ?u.5668
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
x : (i : ι) → E i
⊢ ContCDiffAt K n (fun x => x i) x
Theorem: SciLean.ContCDiff.apply_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type ?u.5644
inst✝⁴ : Vec K X
Y : Type ?u.5657
inst✝³ : Vec K Y
Z : Type ?u.5668
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
x : (i : ι) → E i
⊢ ContCDiffAt K n (fun x => x i) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.ContCDiff.pi_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.6437
inst✝³ : Vec K Y
Z : Type ?u.6448
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
⊢ ContCDiff K n fun x i => f x i
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.6437
inst✝³ : Vec K Y
Z : Type ?u.6448
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ContCDiffAt K n (fun x i => f x i) x
Theorem: SciLean.ContCDiff.pi_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.6437
inst✝³ : Vec K Y
Z : Type ?u.6448
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ContCDiffAt K n (fun x i => f x i) x
Tactic:
apply ContCDiffAt.pi_rule
Proof state after:
case hf
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.6437
inst✝³ : Vec K Y
Z : Type ?u.6448
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ∀ (i : ι), ContCDiffAt K n (fun x => f x i) x
Theorem: SciLean.ContCDiff.pi_rule
Proof state before:
case hf
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.6437
inst✝³ : Vec K Y
Z : Type ?u.6448
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ∀ (i : ι), ContCDiffAt K n (fun x => f x i) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.CDifferentaibleAt.ContCDiffAt_rule'
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.7762
inst✝² : Vec K Z
ι : Type ?u.7773
inst✝¹ : IndexType ι
E : ι → Type ?u.7782
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : ContCDiffAt K ⊤ f x
⊢ CDifferentiableAt K f x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.CDifferentaibleAt.ContCDiffAt_rule'
Proof state before:
case funProp.discharger
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.7762
inst✝² : Vec K Z
ι : Type ?u.7773
inst✝¹ : IndexType ι
E : ι → Type ?u.7782
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : ContCDiffAt K ⊤ f x
⊢ 0 < ⊤
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.CDifferentaible.ContCDiff_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8394
inst✝² : Vec K Z
ι : Type ?u.8405
inst✝¹ : IndexType ι
E : ι → Type ?u.8414
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K n f
h : 0 < n
⊢ CDifferentiable K f
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8394
inst✝² : Vec K Z
ι : Type ?u.8405
inst✝¹ : IndexType ι
E : ι → Type ?u.8414
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K n f
h : 0 < n
x : X
⊢ CDifferentiableAt K f x
Theorem: SciLean.CDifferentaible.ContCDiff_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8394
inst✝² : Vec K Z
ι : Type ?u.8405
inst✝¹ : IndexType ι
E : ι → Type ?u.8414
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K n f
h : 0 < n
x : X
⊢ CDifferentiableAt K f x
Tactic:
fun_prop (disch:=assumption)
Proof state after:
no goals
Theorem: SciLean.CDifferentaible.ContCDiff_rule
Proof state before:
case funProp.discharger
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8394
inst✝² : Vec K Z
ι : Type ?u.8405
inst✝¹ : IndexType ι
E : ι → Type ?u.8414
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K n f
h : 0 < n
x : X
⊢ 0 < n
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.CDifferentaible.ContCDiff_rule'
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8931
inst✝² : Vec K Z
ι : Type ?u.8942
inst✝¹ : IndexType ι
E : ι → Type ?u.8951
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K ⊤ f
⊢ CDifferentiable K f
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8931
inst✝² : Vec K Z
ι : Type ?u.8942
inst✝¹ : IndexType ι
E : ι → Type ?u.8951
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K ⊤ f
x : X
⊢ CDifferentiableAt K f x
Theorem: SciLean.CDifferentaible.ContCDiff_rule'
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8931
inst✝² : Vec K Z
ι : Type ?u.8942
inst✝¹ : IndexType ι
E : ι → Type ?u.8951
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K ⊤ f
x : X
⊢ CDifferentiableAt K f x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.9994
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.10002
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.10015
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.10026
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.10037
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.10046
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.10103
inst✝¹ : IndexType ι
E : ι → Type ?u.10112
inst✝ : (i : ι) → Vec K (E i)
x : X
g : X → Y
hg : ContCDiffAt K n g x
f : X → Z
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => (g x, f x)) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.ContCDiff_rule
Proof state before:
K✝ : Type ?u.10348
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.10356
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.10369
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.10380
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.10391
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.10400
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.10457
inst✝¹ : IndexType ι
E : ι → Type ?u.10466
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : ContCDiff K n g
f : X → Z
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => (g x, f x)
Tactic:
intro x
Proof state after:
K✝ : Type ?u.10348
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.10356
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.10369
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.10380
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.10391
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.10400
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.10457
inst✝¹ : IndexType ι
E : ι → Type ?u.10466
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : ContCDiff K n g
f : X → Z
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => (g x, f x)) x
Theorem: SciLean.Prod.mk.arg_fstsnd.ContCDiff_rule
Proof state before:
K✝ : Type ?u.10348
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.10356
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.10369
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.10380
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.10391
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.10400
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.10457
inst✝¹ : IndexType ι
E : ι → Type ?u.10466
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : ContCDiff K n g
f : X → Z
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => (g x, f x)) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.11095
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.11103
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11116
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11127
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11138
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11147
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.11204
inst✝¹ : IndexType ι
E : ι → Type ?u.11213
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => (f x).1) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.ContCDiff_rule
Proof state before:
K✝ : Type ?u.11392
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.11400
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11413
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11424
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11435
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11444
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.11501
inst✝¹ : IndexType ι
E : ι → Type ?u.11510
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => (f x).1
Tactic:
intro x
Proof state after:
K✝ : Type ?u.11392
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.11400
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11413
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11424
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11435
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11444
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.11501
inst✝¹ : IndexType ι
E : ι → Type ?u.11510
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => (f x).1) x
Theorem: SciLean.Prod.fst.arg_self.ContCDiff_rule
Proof state before:
K✝ : Type ?u.11392
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.11400
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11413
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11424
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11435
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11444
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.11501
inst✝¹ : IndexType ι
E : ι → Type ?u.11510
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => (f x).1) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.11947
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.11955
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11968
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11979
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11990
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11999
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.12056
inst✝¹ : IndexType ι
E : ι → Type ?u.12065
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => (f x).2) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.ContCDiff_rule
Proof state before:
K✝ : Type ?u.12244
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.12252
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.12265
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.12276
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.12287
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.12296
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.12353
inst✝¹ : IndexType ι
E : ι → Type ?u.12362
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => (f x).2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.12535
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.12543
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.12556
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.12567
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.12578
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.12587
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.12633
inst✝² : Vec K Z
ι : Type ?u.12644
inst✝¹ : IndexType ι
E : ι → Type ?u.12653
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => -f x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.ContCDiff_rule
Proof state before:
K✝ : Type ?u.13026
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.13034
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.13047
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.13058
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.13069
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.13078
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.13124
inst✝² : Vec K Z
ι : Type ?u.13135
inst✝¹ : IndexType ι
E : ι → Type ?u.13144
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => -f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.13511
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.13519
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.13532
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.13543
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.13554
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.13563
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.13609
inst✝² : Vec K Z
ι : Type ?u.13620
inst✝¹ : IndexType ι
E : ι → Type ?u.13629
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : ContCDiffAt K n f x
hg : ContCDiffAt K n g x
⊢ ContCDiffAt K n (fun x => f x + g x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.ContCDiff_rule
Proof state before:
K✝ : Type ?u.14921
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.14929
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.14942
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.14953
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.14964
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.14973
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.15019
inst✝² : Vec K Z
ι : Type ?u.15030
inst✝¹ : IndexType ι
E : ι → Type ?u.15039
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : ContCDiff K n f
hg : ContCDiff K n g
⊢ ContCDiff K n fun x => f x + g x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.16325
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.16333
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.16346
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.16357
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.16368
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.16377
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.16423
inst✝² : Vec K Z
ι : Type ?u.16434
inst✝¹ : IndexType ι
E : ι → Type ?u.16443
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : ContCDiffAt K n f x
hg : ContCDiffAt K n g x
⊢ ContCDiffAt K n (fun x => f x - g x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.ContCDiff_rule
Proof state before:
K✝ : Type ?u.17199
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.17207
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.17220
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.17231
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.17242
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.17251
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.17297
inst✝² : Vec K Z
ι : Type ?u.17308
inst✝¹ : IndexType ι
E : ι → Type ?u.17317
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : ContCDiff K n f
hg : ContCDiff K n g
⊢ ContCDiff K n fun x => f x - g x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiffAt_rule_nat
Proof state before:
K✝ : Type ?u.20796
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.20804
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.20817
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.20828
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.20839
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.20848
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.20894
inst✝² : Vec K Z
ι : Type ?u.20905
inst✝¹ : IndexType ι
E : ι → Type ?u.20914
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
x : X
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => c • f x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiffAt_rule_int
Proof state before:
K✝ : Type ?u.21551
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.21559
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.21572
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.21583
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.21594
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.21603
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.21649
inst✝² : Vec K Z
ι : Type ?u.21660
inst✝¹ : IndexType ι
E : ι → Type ?u.21669
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
x : X
hf : ContCDiffAt K n f x
⊢ ContCDiffAt K n (fun x => c • f x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiff_rule_n
Proof state before:
K✝ : Type ?u.24285
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.24293
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.24306
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.24317
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.24328
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.24337
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.24383
inst✝² : Vec K Z
ι : Type ?u.24394
inst✝¹ : IndexType ι
E : ι → Type ?u.24403
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => c • f x
Tactic:
intro x
Proof state after:
K✝ : Type ?u.24285
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.24293
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.24306
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.24317
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.24328
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.24337
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.24383
inst✝² : Vec K Z
ι : Type ?u.24394
inst✝¹ : IndexType ι
E : ι → Type ?u.24403
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => c • f x) x
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiff_rule_n
Proof state before:
K✝ : Type ?u.24285
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.24293
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.24306
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.24317
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.24328
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.24337
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.24383
inst✝² : Vec K Z
ι : Type ?u.24394
inst✝¹ : IndexType ι
E : ι → Type ?u.24403
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => c • f x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiff_rule_int
Proof state before:
K✝ : Type ?u.25276
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.25284
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.25297
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.25308
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.25319
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.25328
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.25374
inst✝² : Vec K Z
ι : Type ?u.25385
inst✝¹ : IndexType ι
E : ι → Type ?u.25394
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
hf : ContCDiff K n f
⊢ ContCDiff K n fun x => c • f x
Tactic:
intro x
Proof state after:
K✝ : Type ?u.25276
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.25284
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.25297
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.25308
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.25319
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.25328
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.25374
inst✝² : Vec K Z
ι : Type ?u.25385
inst✝¹ : IndexType ι
E : ι → Type ?u.25394
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => c • f x) x
Theorem: SciLean.HSMul.hSMul.arg_a1.ContCDiff_rule_int
Proof state before:
K✝ : Type ?u.25276
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.25284
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.25297
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.25308
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.25319
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.25328
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.25374
inst✝² : Vec K Z
ι : Type ?u.25385
inst✝¹ : IndexType ι
E : ι → Type ?u.25394
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
hf : ContCDiff K n f
x : X
⊢ ContCDiffAt K n (fun x => c • f x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IndexType.sum.arg_f.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.32221
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.32229
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.32242
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.32253
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.32264
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.32273
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.32319
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.32339
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
x : X
hf : ∀ (i : ι), ContCDiffAt K n (fun x => f x i) x
⊢ ContCDiffAt K n (fun x =>  ∑ i, f x i) x
Tactic:
sorry_proof
Proof state after:
no goals