Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at (SciLean/Core/FunctionTransformations/CDeriv.lean)

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
⊢ 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:
simp_rw [← SemiInnerProductSpace.inner_norm2]
State after:
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
⊢ cderiv R (fun x => ⟪f x, f x⟫_R) x = fun dx => 2 * ⟪cderiv R f x dx, f x⟫_R

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
⊢ cderiv R (fun x => ⟪f x, f x⟫_R) x = fun dx => 2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
fun_trans
State after:
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

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
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

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]
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

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
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

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
State after:
no goals