internlm/Lean-Github huggingface dataset:
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ (fun dx => ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪f x, cderiv R (fun x => f x) x dx⟫_R) = fun dx =>
    2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
funext dx
Proof state after:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪f x, cderiv R (fun x => f x) x dx⟫_R = 2 * ⟪cderiv R f x dx, f x⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪f x, cderiv R (fun x => f x) x dx⟫_R = 2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
conv =>
  lhs; enter[2]
  rw [← SemiInnerProductSpace.conj_sym]
Proof state after:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + (starRingEnd R) ⟪cderiv R (fun x => f x) x dx, f x⟫_R =
    2 * ⟪cderiv R f x dx, f x⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + (starRingEnd R) ⟪cderiv R (fun x => f x) x dx, f x⟫_R =
    2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
simp
Proof state after:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪cderiv R (fun x => f x) x dx, f x⟫_R = 2 * ⟪cderiv R f x dx, f x⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
case h
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
dx : X
⊢ ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪cderiv R (fun x => f x) x dx, f x⟫_R = 2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
ring
Proof state after:
no goals
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule
Proof state before:
K✝ : Type ?u.114372
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.114378
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.114391
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.114402
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.114413
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.114424
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.114451
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.114467
inst✝¹¹ : RCLike K
X✝ : Type ?u.114473
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.114486
inst✝⁹ : Vec K Y✝
Z : Type ?u.114497
inst✝⁸ : Vec K Z
W : Type ?u.114508
inst✝⁷ : Vec K W
ι : Type ?u.114519
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.114546
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ (cderiv R fun x => ‖f x‖₂²) = fun x dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    2 * ⟪dy, y⟫_R
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.114372
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.114378
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.114391
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.114402
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.114413
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.114424
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.114451
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.114467
inst✝¹¹ : RCLike K
X✝ : Type ?u.114473
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.114486
inst✝⁹ : Vec K Y✝
Z : Type ?u.114497
inst✝⁸ : Vec K Z
W : Type ?u.114508
inst✝⁷ : Vec K W
ι : Type ?u.114519
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.114546
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
x : X
⊢ cderiv R (fun x => ‖f x‖₂²) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    2 * ⟪dy, y⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.114372
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.114378
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.114391
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.114402
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.114413
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.114424
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.114451
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.114467
inst✝¹¹ : RCLike K
X✝ : Type ?u.114473
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.114486
inst✝⁹ : Vec K Y✝
Z : Type ?u.114497
inst✝⁸ : Vec K Z
W : Type ?u.114508
inst✝⁷ : Vec K W
ι : Type ?u.114519
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.114546
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
x : X
⊢ cderiv R (fun x => ‖f x‖₂²) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    2 * ⟪dy, y⟫_R
Tactic:
apply SciLean.Norm2.norm2.arg_a0.cderiv_rule_at f x (hf x)
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.cderiv_rule_at
Proof state before:
K✝ : Type ?u.115368
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.115374
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.115387
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.115398
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.115409
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.115420
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.115447
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.115463
inst✝¹¹ : RCLike K
X✝ : Type ?u.115469
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.115482
inst✝⁹ : Vec K Y✝
Z : Type ?u.115493
inst✝⁸ : Vec K Z
W : Type ?u.115504
inst✝⁷ : Vec K W
ι : Type ?u.115515
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.115542
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ cderiv R (fun x => ‖f x‖₂[R]) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    ‖y‖₂[R]⁻¹ * ⟪dy, y⟫_R
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.cderiv_rule
Proof state before:
K✝ : Type ?u.117262
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.117268
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.117281
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.117292
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.117303
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.117314
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.117341
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.117357
inst✝¹¹ : RCLike K
X✝ : Type ?u.117363
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.117376
inst✝⁹ : Vec K Y✝
Z : Type ?u.117387
inst✝⁸ : Vec K Z
W : Type ?u.117398
inst✝⁷ : Vec K W
ι : Type ?u.117409
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.117436
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
⊢ (cderiv R fun x => ‖f x‖₂[R]) = fun x dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    ‖y‖₂[R]⁻¹ * ⟪dy, y⟫_R
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.117262
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.117268
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.117281
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.117292
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.117303
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.117314
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.117341
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.117357
inst✝¹¹ : RCLike K
X✝ : Type ?u.117363
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.117376
inst✝⁹ : Vec K Y✝
Z : Type ?u.117387
inst✝⁸ : Vec K Z
W : Type ?u.117398
inst✝⁷ : Vec K W
ι : Type ?u.117409
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.117436
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ cderiv R (fun x => ‖f x‖₂[R]) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    ‖y‖₂[R]⁻¹ * ⟪dy, y⟫_R
Theorem: SciLean.SciLean.norm₂.arg_x.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.117262
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.117268
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.117281
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.117292
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.117303
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.117314
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.117341
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.117357
inst✝¹¹ : RCLike K
X✝ : Type ?u.117363
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.117376
inst✝⁹ : Vec K Y✝
Z : Type ?u.117387
inst✝⁸ : Vec K Z
W : Type ?u.117398
inst✝⁷ : Vec K W
ι : Type ?u.117409
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.117436
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ cderiv R (fun x => ‖f x‖₂[R]) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    ‖y‖₂[R]⁻¹ * ⟪dy, y⟫_R
Tactic:
rw [SciLean.norm₂.arg_x.cderiv_rule_at f x (hf x) (hx x)]
Proof state after:
no goals
Theorem: SciLean.SciLean.cderiv.arg_dx.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.119278
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119284
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119297
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119308
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119319
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119330
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119357
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119414
inst✝⁴ : Vec K W
ι : Type ?u.119425
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119452
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
dx : X
hf : CDifferentiableAt K f y
hg : CDifferentiableAt K g dx
⊢ CDifferentiableAt K (fun dx' => cderiv K f y (g dx')) dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.cderiv.arg_dx.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun dx' => cderiv K f y (g dx')
Tactic:
intro dx
Proof state after:
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => cderiv K f y (g dx')) dx
Theorem: SciLean.SciLean.cderiv.arg_dx.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => cderiv K f y (g dx')) dx
Tactic:
apply SciLean.cderiv.arg_dx.CDifferentiableAt_rule
Proof state after:
case hf
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K f y

case hg
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => g dx') dx
Theorem: SciLean.SciLean.cderiv.arg_dx.CDifferentiable_rule
Proof state before:
case hf
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K f y

case hg
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => g dx') dx
Tactic:
apply (hf y)
Proof state after:
case hg
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => g dx') dx
Theorem: SciLean.SciLean.cderiv.arg_dx.CDifferentiable_rule
Proof state before:
case hg
K✝ : Type ?u.119671
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.119677
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.119690
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.119701
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.119712
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.119723
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.119750
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.119807
inst✝⁴ : Vec K W
ι : Type ?u.119818
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119845
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ CDifferentiableAt K (fun dx' => g dx') dx
Tactic:
apply (hg dx)
Proof state after:
no goals
Theorem: SciLean.SciLean.cderiv.arg_dx.cderiv_rule_at
Proof state before:
K✝ : Type ?u.120176
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.120182
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.120195
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.120206
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.120217
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.120228
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.120255
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.120312
inst✝⁴ : Vec K W
ι : Type ?u.120323
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.120350
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
dx : X
hf : CDifferentiableAt K f y
hg : CDifferentiableAt K g dx
⊢ cderiv K (fun dx' => cderiv K f y (g dx')) dx = fun ddx =>
    let ddy := cderiv K g dx ddx;
    cderiv K f y ddy
Tactic:
sorry_proof
Proof state after:
no goals