internlm/Lean-Github huggingface dataset:
Theorem: SciLean.forwardEuler.isOdeStepper
Proof state before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), (x + Δt • f t x)) = f t x
Tactic:
autodiff
Proof state after:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
⊢ ∀ (t : R) (x : X),
    let y := f t x;
    (Filter.limit (nhds 0) fun Δt' => y) = f t x
Theorem: SciLean.forwardEuler.isOdeStepper
Proof state before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
⊢ ∀ (t : R) (x : X),
    let y := f t x;
    (Filter.limit (nhds 0) fun Δt' => y) = f t x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.mk_eval
Proof state before:
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.4149
inst✝⁵ : Vec K Z
W : Type ?u.4160
inst✝⁴ : Vec K W
ι : Type ?u.4171
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.4198
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : IsSmoothLinearMap K f
⊢ { toFun := f, is_smooth_linear_map := hf } x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.eta_reduce
Proof state before:
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.4502
inst✝⁵ : Vec K Z
W : Type ?u.4513
inst✝⁴ : Vec K W
ι : Type ?u.4524
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.4551
inst✝ : (i : ι) → Vec K (E i)
f : X ⊸[K] Y
⊢ { toFun := f.toFun, is_smooth_linear_map := ⋯ } = f
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.mk'_eval
Proof state before:
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.5367
inst✝⁵ : Vec K Z
W : Type ?u.5378
inst✝⁴ : Vec K W
ι : Type ?u.5389
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.5416
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : IsSmoothLinearMap K f
⊢ (mk' K f hf) x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.add_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.18833
inst✝⁵ : Vec K Z
W : Type ?u.18844
inst✝⁴ : Vec K W
ι : Type ?u.18855
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18882
inst✝ : (i : ι) → Vec K (E i)
f g : X ⊸[K] Y
x : X
r : K
⊢ (f + g) x = f x + g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.sub_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.20452
inst✝⁵ : Vec K Z
W : Type ?u.20463
inst✝⁴ : Vec K W
ι : Type ?u.20474
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.20501
inst✝ : (i : ι) → Vec K (E i)
f g : X ⊸[K] Y
x : X
r : K
⊢ (f - g) x = f x - g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.neg_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.21535
inst✝⁵ : Vec K Z
W : Type ?u.21546
inst✝⁴ : Vec K W
ι : Type ?u.21557
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.21584
inst✝ : (i : ι) → Vec K (E i)
f g : X ⊸[K] Y
x : X
r : K
⊢ (-f) x = -f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.smul_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.22179
inst✝⁵ : Vec K Z
W : Type ?u.22190
inst✝⁴ : Vec K W
ι : Type ?u.22201
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.22228
inst✝ : (i : ι) → Vec K (E i)
f g : X ⊸[K] Y
x : X
r : K
⊢ (r • f) x = r • f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.zero_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.24103
inst✝⁵ : Vec K Z
W : Type ?u.24114
inst✝⁴ : Vec K W
ι : Type ?u.24125
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24152
inst✝ : (i : ι) → Vec K (E i)
f g : X ⊸[K] Y
x : X
r : K
⊢ 0 x = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.apply_zero
Proof state before:
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.25089
inst✝⁵ : Vec K Z
W : Type ?u.25100
inst✝⁴ : Vec K W
ι : Type ?u.25111
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.25138
inst✝ : (i : ι) → Vec K (E i)
f✝ g : X ⊸[K] Y
x : X
r : K
f : X ⊸[K] Y
⊢ f 0 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.fintype_sum_apply
Proof state before:
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : Vec K X
Y : Type u_4
inst✝⁷ : Vec K Y
Z : Type ?u.27875
inst✝⁶ : Vec K Z
W : Type ?u.27886
inst✝⁵ : Vec K W
ι : Type ?u.27897
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.27924
inst✝¹ : (i : ι) → Vec K (E i)
I : Type u_1
inst✝ : Fintype I
f : I → X ⊸[K] Y
x : X
⊢ (∑ i : I, f i) x = ∑ i : I, (f i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SmoothLinearMap.indextype_sum_apply
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : Vec K X
Y : Type (max u_2 u_3)
inst✝⁷ : Vec K Y
Z : Type ?u.30189
inst✝⁶ : Vec K Z
W : Type ?u.30200
inst✝⁵ : Vec K W
ι : Type ?u.30211
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.30238
inst✝¹ : (i : ι) → Vec K (E i)
I : Type u_1
inst✝ : IndexType I
f : I → X ⊸[K] Y
x : X
⊢ ( ∑ i, f i) x = ∑ i, (f i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.mk'_eval
Proof state before:
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.6141
inst✝⁵ : Vec K Z
W : Type ?u.6152
inst✝⁴ : Vec K W
ι : Type ?u.6163
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6190
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
x : X
f : X → Y
hf : ContCDiff K n f
⊢ { toFun := f, is_cont_cdiff_map := hf } x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.eta_reduce
Proof state before:
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.6513
inst✝⁵ : Vec K Z
W : Type ?u.6524
inst✝⁴ : Vec K W
ι : Type ?u.6535
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6562
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿[K,n] Y
⊢ { toFun := f.toFun, is_cont_cdiff_map := ⋯ } = f
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap_eta
Proof state before:
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.12567
inst✝⁵ : Vec K Z
W : Type ?u.12578
inst✝⁴ : Vec K W
ι : Type ?u.12589
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.12616
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿[K,n] Y
⊢ (fun x ⟿[K,n] f x) = f
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.add_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.19513
inst✝⁵ : Vec K Z
W : Type ?u.19524
inst✝⁴ : Vec K W
ι : Type ?u.19535
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.19562
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿[K,n] Y
x : X
r : K
⊢ (f + g) x = f x + g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.sub_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.21147
inst✝⁵ : Vec K Z
W : Type ?u.21158
inst✝⁴ : Vec K W
ι : Type ?u.21169
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.21196
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿[K,n] Y
x : X
r : K
⊢ (f - g) x = f x - g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.neg_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.22245
inst✝⁵ : Vec K Z
W : Type ?u.22256
inst✝⁴ : Vec K W
ι : Type ?u.22267
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.22294
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿[K,n] Y
x : X
r : K
⊢ (-f) x = -f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.smul_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.22902
inst✝⁵ : Vec K Z
W : Type ?u.22913
inst✝⁴ : Vec K W
ι : Type ?u.22924
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.22951
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿[K,n] Y
x : X
r : K
⊢ (r • f) x = r • f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap.zero_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.24839
inst✝⁵ : Vec K Z
W : Type ?u.24850
inst✝⁴ : Vec K W
ι : Type ?u.24861
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24888
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿[K,n] Y
x : X
r : K
⊢ 0 x = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap_eval_CDifferentiable
Proof state before:
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.44416
inst✝⁵ : Vec K Z
W : Type ?u.44427
inst✝⁴ : Vec K W
ι : Type ?u.44438
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.44465
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
h : 0 < n
⊢ CDifferentiable K fun fx => fx.1 fx.2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap_eval_CDifferentiable'
Proof state before:
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.44862
inst✝⁵ : Vec K Z
W : Type ?u.44873
inst✝⁴ : Vec K W
ι : Type ?u.44884
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.44911
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
⊢ CDifferentiable K fun fx => fx.1 fx.2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap_apply_CDifferentiable
Proof state before:
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.45251
inst✝⁵ : Vec K Z
W : Type u_4
inst✝⁴ : Vec K W
ι : Type ?u.45273
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.45300
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → X ⟿[K,⊤] Y
g : W → X
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun w => (f w) (g w)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMap_apply_CDifferentiableAt
Proof state before:
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.45662
inst✝⁵ : Vec K Z
W : Type u_4
inst✝⁴ : Vec K W
ι : Type ?u.45684
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.45711
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → X ⟿[K,⊤] Y
g : W → X
w : W
hf : CDifferentiableAt K f w
hg : CDifferentiableAt K g w
⊢ CDifferentiableAt K (fun w => (f w) (g w)) w
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.id_rule
Proof state before:
K : Type u_2
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type ?u.538
inst✝⁶ : Vec K Y
Z : Type ?u.549
inst✝⁵ : Vec K Z
W : Type ?u.560
inst✝⁴ : Vec K W
ι : Type ?u.571
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.598
inst✝ : (i : ι) → Vec K (E i)
⊢ (fwdDeriv K fun x => x) = fun x dx => (x, dx)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_2
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type ?u.538
inst✝⁶ : Vec K Y
Z : Type ?u.549
inst✝⁵ : Vec K Z
W : Type ?u.560
inst✝⁴ : Vec K W
ι : Type ?u.571
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.598
inst✝ : (i : ι) → Vec K (E i)
⊢ (fun x dx => ((fun x => x) x, cderiv K (fun x => x) x dx)) = fun x dx => (x, dx)
Theorem: SciLean.fwdDeriv.id_rule
Proof state before:
K : Type u_2
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type ?u.538
inst✝⁶ : Vec K Y
Z : Type ?u.549
inst✝⁵ : Vec K Z
W : Type ?u.560
inst✝⁴ : Vec K W
ι : Type ?u.571
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.598
inst✝ : (i : ι) → Vec K (E i)
⊢ (fun x dx => ((fun x => x) x, cderiv K (fun x => x) x dx)) = fun x dx => (x, dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.const_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.879
inst✝⁵ : Vec K Z
W : Type ?u.890
inst✝⁴ : Vec K W
ι : Type ?u.901
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.928
inst✝ : (i : ι) → Vec K (E i)
y : Y
⊢ (fwdDeriv K fun x => y) = fun x dx => (y, 0)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.879
inst✝⁵ : Vec K Z
W : Type ?u.890
inst✝⁴ : Vec K W
ι : Type ?u.901
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.928
inst✝ : (i : ι) → Vec K (E i)
y : Y
⊢ (fun x dx => ((fun x => y) x, cderiv K (fun x => y) x dx)) = fun x dx => (y, 0)
Theorem: SciLean.fwdDeriv.const_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.879
inst✝⁵ : Vec K Z
W : Type ?u.890
inst✝⁴ : Vec K W
ι : Type ?u.901
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.928
inst✝ : (i : ι) → Vec K (E i)
y : Y
⊢ (fun x dx => ((fun x => y) x, cderiv K (fun x => y) x dx)) = fun x dx => (y, 0)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.comp_rule_at
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.2446
inst✝⁴ : Vec K W
ι : Type ?u.2457
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2484
inst✝ : (i : ι) → Vec K (E i)
x : X
f : Y → Z
g : X → Y
hf : CDifferentiableAt K f (g x)
hg : CDifferentiableAt K g x
⊢ fwdDeriv K (fun x => f (g x)) x = fun dx =>
    let ydy := fwdDeriv K g x dx;
    let zdz := fwdDeriv K f ydy.1 ydy.2;
    zdz
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.2446
inst✝⁴ : Vec K W
ι : Type ?u.2457
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2484
inst✝ : (i : ι) → Vec K (E i)
x : X
f : Y → Z
g : X → Y
hf : CDifferentiableAt K f (g x)
hg : CDifferentiableAt K g x
⊢ (fun dx => ((fun x => f (g x)) x, cderiv K (fun x => f (g x)) x dx)) = fun dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := (f ydy.1, cderiv K f ydy.1 ydy.2);
    zdz
Theorem: SciLean.fwdDeriv.comp_rule_at
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.2446
inst✝⁴ : Vec K W
ι : Type ?u.2457
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2484
inst✝ : (i : ι) → Vec K (E i)
x : X
f : Y → Z
g : X → Y
hf : CDifferentiableAt K f (g x)
hg : CDifferentiableAt K g x
⊢ (fun dx => ((fun x => f (g x)) x, cderiv K (fun x => f (g x)) x dx)) = fun dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := (f ydy.1, cderiv K f ydy.1 ydy.2);
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.comp_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.5271
inst✝⁴ : Vec K W
ι : Type ?u.5282
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.5309
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fwdDeriv K fun x => f (g x)) = fun x dx =>
    let ydy := fwdDeriv K g x dx;
    let zdz := fwdDeriv K f ydy.1 ydy.2;
    zdz
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.5271
inst✝⁴ : Vec K W
ι : Type ?u.5282
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.5309
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fun x dx => ((fun x => f (g x)) x, cderiv K (fun x => f (g x)) x dx)) = fun x dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := (f ydy.1, cderiv K f ydy.1 ydy.2);
    zdz
Theorem: SciLean.fwdDeriv.comp_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.5271
inst✝⁴ : Vec K W
ι : Type ?u.5282
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.5309
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fun x dx => ((fun x => f (g x)) x, cderiv K (fun x => f (g x)) x dx)) = fun x dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := (f ydy.1, cderiv K f ydy.1 ydy.2);
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.let_rule_at
Proof state before:
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
W : Type ?u.8253
inst✝⁴ : Vec K W
ι : Type ?u.8264
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.8291
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y → Z
g : X → Y
hf : CDifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : CDifferentiableAt K g x
⊢ fwdDeriv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    fun dx =>
    let ydy := fwdDeriv K g x dx;
    let zdz := fwdDeriv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2);
    zdz
Tactic:
unfold fwdDeriv
Proof state after:
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
W : Type ?u.8253
inst✝⁴ : Vec K W
ι : Type ?u.8264
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.8291
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y → Z
g : X → Y
hf : CDifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : CDifferentiableAt K g x
⊢ (fun dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        cderiv K
          (fun x =>
            let y := g x;
            f x y)
          x dx)) =
    fun dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), cderiv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2));
    zdz
Theorem: SciLean.fwdDeriv.let_rule_at
Proof state before:
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
W : Type ?u.8253
inst✝⁴ : Vec K W
ι : Type ?u.8264
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.8291
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y → Z
g : X → Y
hf : CDifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : CDifferentiableAt K g x
⊢ (fun dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        cderiv K
          (fun x =>
            let y := g x;
            f x y)
          x dx)) =
    fun dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), cderiv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2));
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.let_rule
Proof state before:
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
W : Type ?u.13431
inst✝⁴ : Vec K W
ι : Type ?u.13442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13469
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
g : X → Y
hf : CDifferentiable K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
⊢ (fwdDeriv K fun x =>
      let y := g x;
      f x y) =
    fun x dx =>
    let ydy := fwdDeriv K g x dx;
    let zdz := fwdDeriv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2);
    zdz
Tactic:
unfold fwdDeriv
Proof state after:
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
W : Type ?u.13431
inst✝⁴ : Vec K W
ι : Type ?u.13442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13469
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
g : X → Y
hf : CDifferentiable K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
⊢ (fun x dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        cderiv K
          (fun x =>
            let y := g x;
            f x y)
          x dx)) =
    fun x dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), cderiv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2));
    zdz
Theorem: SciLean.fwdDeriv.let_rule
Proof state before:
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
W : Type ?u.13431
inst✝⁴ : Vec K W
ι : Type ?u.13442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13469
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
g : X → Y
hf : CDifferentiable K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
⊢ (fun x dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        cderiv K
          (fun x =>
            let y := g x;
            f x y)
          x dx)) =
    fun x dx =>
    let ydy := (g x, cderiv K g x dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), cderiv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2));
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.apply_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type ?u.17506
inst✝⁷ : Vec K X
Y : Type ?u.17519
inst✝⁶ : Vec K Y
Z : Type ?u.17530
inst✝⁵ : Vec K Z
W : Type ?u.17541
inst✝⁴ : Vec K W
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_2
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ (fwdDeriv K fun x => x i) = fun x dx => (x i, dx i)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_3
inst✝⁸ : RCLike K
X : Type ?u.17506
inst✝⁷ : Vec K X
Y : Type ?u.17519
inst✝⁶ : Vec K Y
Z : Type ?u.17530
inst✝⁵ : Vec K Z
W : Type ?u.17541
inst✝⁴ : Vec K W
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_2
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ (fun x dx => ((fun x => x i) x, cderiv K (fun x => x i) x dx)) = fun x dx => (x i, dx i)
Theorem: SciLean.fwdDeriv.apply_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type ?u.17506
inst✝⁷ : Vec K X
Y : Type ?u.17519
inst✝⁶ : Vec K Y
Z : Type ?u.17530
inst✝⁵ : Vec K Z
W : Type ?u.17541
inst✝⁴ : Vec K W
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_2
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ (fun x dx => ((fun x => x i) x, cderiv K (fun x => x i) x dx)) = fun x dx => (x i, dx i)
Tactic:
fun_trans
Proof state after:
no goals