Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at (SciLean/Core/FunctionTransformations/FDeriv.lean)

State before:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
⊢ fderiv R (fun x => f x / g x) x =
    let k := f x;
    let k' := g x;
    fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2
Tactic:
have h : ∀ (f : R → K) x, fderiv R f x 1 = deriv f x := by simp[deriv]
State after:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ fderiv R (fun x => f x / g x) x =
    let k := f x;
    let k' := g x;
    fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2

State before:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ fderiv R (fun x => f x / g x) x =
    let k := f x;
    let k' := g x;
    fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2
Tactic:
ext
State after:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ (fderiv R (fun x => f x / g x) x) 1 =
    (let k := f x;
      let k' := g x;
      fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2)
      1

State before:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ (fderiv R (fun x => f x / g x) x) 1 =
    (let k := f x;
      let k' := g x;
      fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2)
      1
Tactic:
simp[h]
State after:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ deriv (fun x => f x / g x) x = (deriv f x * g x - f x * deriv g x) / g x ^ 2

State before:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ deriv (fun x => f x / g x) x = (deriv f x * g x - f x * deriv g x) / g x ^ 2
Tactic:
apply deriv_div hf hg hx
State after:
no goals

State before:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
⊢ ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
Tactic:
simp[deriv]
State after:
no goals