internlm/Lean-Github huggingface dataset:
Theorem: SciLean.fderiv.comp_rule_at
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ ContinuousLinearMap.comp (fderiv K f (g x)) (fderiv K g x) =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K f y) dy;
      dz
Tactic:
ext dx
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
dx : X
⊢ (ContinuousLinearMap.comp (fderiv K f (g x)) (fderiv K g x)) dx =
    (let y := g x;
      fun dx =>L[K]
        let dy := (fderiv K g x) dx;
        let dz := (fderiv K f y) dy;
        dz)
      dx
Theorem: SciLean.fderiv.comp_rule_at
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
dx : X
⊢ (ContinuousLinearMap.comp (fderiv K f (g x)) (fderiv K g x)) dx =
    (let y := g x;
      fun dx =>L[K]
        let dy := (fderiv K g x) dx;
        let dz := (fderiv K f y) dy;
        dz)
      dx
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.fderiv.comp_rule_at
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ (fun x => f (g x)) = f ∘ g
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
⊢ fderiv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
      dz
Tactic:
have h : (fun x => f x (g x)) = (fun xy : X×Y => f xy.1 xy.2) ∘ (fun x => (x, g x)) := by rfl
Proof state after:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
⊢ fderiv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
      dz
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
⊢ fderiv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
      dz
Tactic:
conv =>
  lhs
  rw[h]
  rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)]
  rw[DifferentiableAt.fderiv_prod (by simp) hg]
Proof state after:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
⊢ ContinuousLinearMap.comp (fderiv K (fun xy => f xy.1 xy.2) (x, g x))
      (ContinuousLinearMap.prod (fderiv K (fun x => x) x) (fderiv K g x)) =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
      dz
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
⊢ ContinuousLinearMap.comp (fderiv K (fun xy => f xy.1 xy.2) (x, g x))
      (ContinuousLinearMap.prod (fderiv K (fun x => x) x) (fderiv K g x)) =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
      dz
Tactic:
ext dx
Proof state after:
case h
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
dx : X
⊢ (ContinuousLinearMap.comp (fderiv K (fun xy => f xy.1 xy.2) (x, g x))
        (ContinuousLinearMap.prod (fderiv K (fun x => x) x) (fderiv K g x)))
      dx =
    (let y := g x;
      fun dx =>L[K]
        let dy := (fderiv K g x) dx;
        let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
        dz)
      dx
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
case h
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
dx : X
⊢ (ContinuousLinearMap.comp (fderiv K (fun xy => f xy.1 xy.2) (x, g x))
        (ContinuousLinearMap.prod (fderiv K (fun x => x) x) (fderiv K g x)))
      dx =
    (let y := g x;
      fun dx =>L[K]
        let dy := (fderiv K g x) dx;
        let dz := (fderiv K (fun xy => f xy.1 xy.2) (x, y)) (dx, dy);
        dz)
      dx
Tactic:
simp[ContinuousLinearMap.comp]
Proof state after:
no goals
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
⊢ (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.fderiv.let_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_3
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.56458
inst✝² : Fintype ι
E : ι → Type ?u.56466
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
h : (fun x => f x (g x)) = (fun xy => f xy.1 xy.2) ∘ fun x => (x, g x)
⊢ DifferentiableAt K (fun x => x) x
Tactic:
simp
Proof state after:
no goals
Theorem: Prod.mk.arg_fstsnd.fderiv_rule_at
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_4
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.97516
inst✝² : Fintype ι
E : ι → Type ?u.97524
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x : X
g : X → Y
hg : DifferentiableAt K g x
f : X → Z
hf : DifferentiableAt K f x
⊢ fderiv K (fun x => (g x, f x)) x = fun dx =>L[K] ((fderiv K g x) dx, (fderiv K f x) dx)
Tactic:
apply DifferentiableAt.fderiv_prod hg hf
Proof state after:
no goals
Theorem: Prod.fst.arg_self.fderiv_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_2
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.105610
inst✝² : Fintype ι
E : ι → Type ?u.105618
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ fderiv K (fun x => (f x).1) x = fun dx =>L[K] ((fderiv K f x) dx).1
Tactic:
apply fderiv.fst hf
Proof state after:
no goals
Theorem: Prod.snd.arg_self.fderiv_rule_at
Proof state before:
K : Type u_4
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_2
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.113465
inst✝² : Fintype ι
E : ι → Type ?u.113473
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ fderiv K (fun x => (f x).2) x = fun dx =>L[K] ((fderiv K f x) dx).2
Tactic:
apply fderiv.snd hf
Proof state after:
no goals
Theorem: Neg.neg.arg_a0.fderiv_rule
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.133916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.134051
inst✝² : Fintype ι
E : ι → Type ?u.134059
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y
⊢ (fderiv K fun x => -f x) = fun x => fun dx =>L[K] -(fderiv K f x) dx
Tactic:
funext x
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.133916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.134051
inst✝² : Fintype ι
E : ι → Type ?u.134059
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y
x : X
⊢ fderiv K (fun x => -f x) x = fun dx =>L[K] -(fderiv K f x) dx
Theorem: Neg.neg.arg_a0.fderiv_rule
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.133916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.134051
inst✝² : Fintype ι
E : ι → Type ?u.134059
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y
x : X
⊢ fderiv K (fun x => -f x) x = fun dx =>L[K] -(fderiv K f x) dx
Tactic:
apply fderiv_neg
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.fderiv_rule_at
Proof state before:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
⊢ fderiv K (fun x => f x * g x) x =
    let fx := f x;
    let gx := g x;
    fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx
Tactic:
ext dx
Proof state after:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
dx : X
⊢ (fderiv K (fun x => f x * g x) x) dx =
    (let fx := f x;
      let gx := g x;
      fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx)
      dx
Theorem: HMul.hMul.arg_a0a1.fderiv_rule_at
Proof state before:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
dx : X
⊢ (fderiv K (fun x => f x * g x) x) dx =
    (let fx := f x;
      let gx := g x;
      fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx)
      dx
Tactic:
simp[fderiv_mul hf hg, mul_comm]
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at
Proof 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]
Proof 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
Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at
Proof 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
Proof 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
Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at
Proof 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]
Proof 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
Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at
Proof 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
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.fderiv_rule_at
Proof 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]
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.arg_y.IsSmoothLinearMap_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.6147
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.6158
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.6169
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6196
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
⊢ IsSmoothLinearMap K fun y => semiAdjoint K f y
Tactic:
constructor
Proof state after:
case left
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.6147
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.6158
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.6169
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6196
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
⊢ IsLinearMap K fun y => semiAdjoint K f y

case right
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.6147
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.6158
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.6169
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6196
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
⊢ CDifferentiable K fun y => semiAdjoint K f y