internlm/Lean-Github huggingface dataset:
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiffAt_rule
Proof 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
Proof 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)
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiffAt_rule
Proof 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
Proof 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)
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiffAt_rule
Proof 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
Proof 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
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiffAt_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.85565
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.85571
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.85584
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.85595
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.85606
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.85633
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.85649
inst✝¹¹ : RCLike K
X✝ : Type ?u.85655
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.85668
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.85679
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.85690
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.85701
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.85728
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
f : X → Y
hf : HasAdjDiff R f
⊢ HasAdjDiff R fun x => ‖f x‖₂²
Tactic:
intro x
Proof state after:
K✝ : Type ?u.85565
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.85571
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.85584
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.85595
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.85606
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.85633
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.85649
inst✝¹¹ : RCLike K
X✝ : Type ?u.85655
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.85668
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.85679
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.85690
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.85701
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.85728
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
f : X → Y
hf : HasAdjDiff R f
x : X
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂²) x
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.85565
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.85571
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.85584
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.85595
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.85606
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.85633
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.85649
inst✝¹¹ : RCLike K
X✝ : Type ?u.85655
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.85668
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.85679
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.85690
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.85701
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.85728
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
f : X → Y
hf : HasAdjDiff R f
x : X
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂²) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.86209
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.86215
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.86228
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.86239
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.86250
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.86277
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.86293
inst✝¹¹ : RCLike K
X✝ : Type ?u.86299
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.86312
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.86323
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.86334
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.86345
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.86372
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
hfz : f x ≠ 0
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂[R]) x
Tactic:
constructor
Proof state after:
case left
K✝ : Type ?u.86209
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.86215
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.86228
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.86239
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.86250
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.86277
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.86293
inst✝¹¹ : RCLike K
X✝ : Type ?u.86299
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.86312
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.86323
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.86334
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.86345
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.86372
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
hfz : f x ≠ 0
⊢ CDifferentiableAt R (fun x => ‖f x‖₂[R]) x

case right
K✝ : Type ?u.86209
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.86215
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.86228
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.86239
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.86250
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.86277
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.86293
inst✝¹¹ : RCLike K
X✝ : Type ?u.86299
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.86312
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.86323
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.86334
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.86345
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.86372
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
hfz : f x ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂[R]) x)
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiffAt_rule
Proof state before:
case right
K✝ : Type ?u.86209
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.86215
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.86228
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.86239
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.86250
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.86277
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.86293
inst✝¹¹ : RCLike K
X✝ : Type ?u.86299
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.86312
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.86323
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.86334
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.86345
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.86372
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
hfz : f x ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun x => ‖f x‖₂[R]) x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiffAt_rule
Proof state before:
case funProp.discharger
K✝ : Type ?u.86209
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.86215
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.86228
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.86239
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.86250
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.86277
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.86293
inst✝¹¹ : RCLike K
X✝ : Type ?u.86299
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.86312
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.86323
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.86334
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.86345
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.86372
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
hfz : f x ≠ 0
⊢ f x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.88108
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.88114
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.88127
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.88138
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.88149
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.88176
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.88192
inst✝¹¹ : RCLike K
X✝ : Type ?u.88198
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.88211
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.88222
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.88233
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.88244
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.88271
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
f : X → Y
hf : HasAdjDiff R f
hfz : ∀ (x : X), f x ≠ 0
⊢ HasAdjDiff R fun x => ‖f x‖₂[R]
Tactic:
intro x
Proof state after:
K✝ : Type ?u.88108
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.88114
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.88127
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.88138
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.88149
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.88176
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.88192
inst✝¹¹ : RCLike K
X✝ : Type ?u.88198
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.88211
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.88222
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.88233
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.88244
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.88271
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
f : X → Y
hf : HasAdjDiff R f
hfz : ∀ (x : X), f x ≠ 0
x : X
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂[R]) x
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.88108
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.88114
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.88127
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.88138
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.88149
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.88176
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.88192
inst✝¹¹ : RCLike K
X✝ : Type ?u.88198
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.88211
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.88222
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.88233
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.88244
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.88271
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
f : X → Y
hf : HasAdjDiff R f
hfz : ∀ (x : X), f x ≠ 0
x : X
⊢ HasAdjDiffAt R (fun x => ‖f x‖₂[R]) x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.HasAdjDiff_rule
Proof state before:
case funProp.discharger
K✝ : Type ?u.88108
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.88114
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.88127
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.88138
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.88149
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.88176
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.88192
inst✝¹¹ : RCLike K
X✝ : Type ?u.88198
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.88211
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.88222
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.88233
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.88244
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.88271
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
f : X → Y
hf : HasAdjDiff R f
hfz : ∀ (x : X), f x ≠ 0
x : X
⊢ f x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.SciLean.semiAdjoint.arg_y.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.91165
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91171
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91184
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91195
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91206
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91233
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.91279
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.91290
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.91301
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.91328
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiableAt K a0 w
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) w
Tactic:
fun_prop
Proof state after:
no goals