Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiffAt_rule (SciLean/Core/FunctionPropositions/HasAdjDiff.lean)

State before:
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂²) x
Tactic:
constructor
State after:
case left
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ CDifferentiableAt R (fun x => ‖f x‖₂²) x

case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂²) x)

State before:
case left
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ CDifferentiableAt R (fun x => ‖f x‖₂²) x

case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂²) x)
Tactic:
fun_prop
State after:
case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂²) x)

State before:
case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂²) x)
Tactic:
fun_trans
State after:
case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R fun dx => 2 * ⟪cderiv R (fun x => f x) x dx, f x⟫_R

State before:
case right
K✝ : Type ?u.83178
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.83184
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.83197
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.83208
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.83219
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.83246
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.83262
inst✝¹¹ : RCLike K
X✝ : Type ?u.83268
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.83281
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.83292
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.83303
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.83314
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.83341
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : HasAdjDiffAt R f x
⊢ HasSemiAdjoint R fun dx => 2 * ⟪cderiv R (fun x => f x) x dx, f x⟫_R
Tactic:
fun_prop
State after:
no goals