Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule (SciLean/Core/FunctionTransformations/FwdDeriv.lean)

State before:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
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
⊢ (fwdDeriv R fun x => ‖f x‖₂[R]) = fun x dx =>
    let ydy := fwdDeriv R f x dx;
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
unfold fwdDeriv
State after:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
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
⊢ (fun x dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)

State before:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
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
⊢ (fun x dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
fun_trans (disch:=assumption)
State after:
no goals

State before:
case funProp.discharger
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
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 dx : X
⊢ ∀ (x : X), f x ≠ 0
Tactic:
assumption
State after:
no goals