internlm/Lean-Github huggingface dataset:
Theorem: SciLean.proj_basis
Proof state before:
ι : Type u_2
K : Type u_1
X : Type u_3
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ℼ i ⅇ j = if i = j then 1 else 0
Tactic:
simp only [←inner_dualBasis_proj, inner_basis_dualBasis, eq_comm]
Proof state after:
no goals
Theorem: SciLean.proj_zero
Proof state before:
ι : Type u_2
K : Type u_1
X : Type u_3
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i : ι
⊢ ℼ i 0 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.dualProj_dualBasis
Proof state before:
ι : Type u_2
K : Type u_1
X : Type u_3
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ℼ' i ⅇ' j = if i = j then 1 else 0
Tactic:
simp only [←inner_basis_dualProj, inner_dualBasis_basis, eq_comm]
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.id_rule
Proof state before:
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.2744
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.2879
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.3014
inst✝² : Fintype ι
E : ι → Type ?u.3022
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
⊢ (fwdFDeriv K fun x => x) = fun x dx => (x, dx)
Tactic:
unfold fwdFDeriv
Proof state after:
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.2744
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.2879
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.3014
inst✝² : Fintype ι
E : ι → Type ?u.3022
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
⊢ (fun x dx => ((fun x => x) x, (fderiv K (fun x => x) x) dx)) = fun x dx => (x, dx)
Theorem: SciLean.FwdFDeriv.id_rule
Proof state before:
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.2744
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.2879
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.3014
inst✝² : Fintype ι
E : ι → Type ?u.3022
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
⊢ (fun x dx => ((fun x => x) x, (fderiv K (fun x => x) x) dx)) = fun x dx => (x, dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.const_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.4683
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.4818
inst✝² : Fintype ι
E : ι → Type ?u.4826
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
y : Y
⊢ (fwdFDeriv K fun x => y) = fun x dx => (y, 0)
Tactic:
unfold fwdFDeriv
Proof state after:
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.4683
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.4818
inst✝² : Fintype ι
E : ι → Type ?u.4826
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
y : Y
⊢ (fun x dx => ((fun x => y) x, (fderiv K (fun x => y) x) dx)) = fun x dx => (y, 0)
Theorem: SciLean.FwdFDeriv.const_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.4683
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.4818
inst✝² : Fintype ι
E : ι → Type ?u.4826
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
y : Y
⊢ (fun x dx => ((fun x => y) x, (fderiv K (fun x => y) x) dx)) = fun x dx => (y, 0)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.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.8427
inst✝² : Fintype ι
E : ι → Type ?u.8435
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : Y → Z
g : X → Y
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ fwdFDeriv K (fun x => f (g x)) x = fun dx =>
    let ydy := fwdFDeriv K g x dx;
    let zdz := fwdFDeriv K f ydy.1 ydy.2;
    zdz
Tactic:
unfold fwdFDeriv
Proof state after:
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.8427
inst✝² : Fintype ι
E : ι → Type ?u.8435
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : Y → Z
g : X → Y
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ (fun dx => ((fun x => f (g x)) x, (fderiv K (fun x => f (g x)) x) dx)) = fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := (f ydy.1, (fderiv K f ydy.1) ydy.2);
    zdz
Theorem: SciLean.FwdFDeriv.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.8427
inst✝² : Fintype ι
E : ι → Type ?u.8435
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : Y → Z
g : X → Y
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ (fun dx => ((fun x => f (g x)) x, (fderiv K (fun x => f (g x)) x) dx)) = fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := (f ydy.1, (fderiv K f ydy.1) ydy.2);
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.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.18770
inst✝² : Fintype ι
E : ι → Type ?u.18778
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y → Z
g : X → Y
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
⊢ fwdFDeriv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    fun dx =>
    let ydy := fwdFDeriv K g x dx;
    let zdz := fwdFDeriv K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2);
    zdz
Tactic:
unfold fwdFDeriv
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.18770
inst✝² : Fintype ι
E : ι → Type ?u.18778
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y → Z
g : X → Y
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
⊢ (fun dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        (fderiv K
            (fun x =>
              let y := g x;
              f x y)
            x)
          dx)) =
    fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), (fderiv K (fun xy => f xy.1 xy.2) (x, ydy.1)) (dx, ydy.2));
    zdz
Theorem: SciLean.FwdFDeriv.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.18770
inst✝² : Fintype ι
E : ι → Type ?u.18778
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y → Z
g : X → Y
hf : DifferentiableAt K (fun xy => f xy.1 xy.2) (x, g x)
hg : DifferentiableAt K g x
⊢ (fun dx =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        (fderiv K
            (fun x =>
              let y := g x;
              f x y)
            x)
          dx)) =
    fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := ((fun xy => f xy.1 xy.2) (x, ydy.1), (fderiv K (fun xy => f xy.1 xy.2) (x, ydy.1)) (dx, ydy.2));
    zdz
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.apply_rule
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.29864
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.30006
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.30141
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
i : ι
⊢ (fwdFDeriv K fun x => x i) = fun x dx => (x i, dx i)
Tactic:
unfold fwdFDeriv
Proof state after:
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.29864
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.30006
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.30141
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
i : ι
⊢ (fun x dx => ((fun x => x i) x, (fderiv K (fun x => x i) x) dx)) = fun x dx => (x i, dx i)
Theorem: SciLean.FwdFDeriv.apply_rule
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.29864
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.30006
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.30141
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
i : ι
⊢ (fun x dx => ((fun x => x i) x, (fderiv K (fun x => x i) x) dx)) = fun x dx => (x i, dx i)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.pi_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.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x
⊢ fwdFDeriv K (fun x i => f x i) x = fun dx => (fun i => f x i, fun i => (fwdFDeriv K (fun x => f x i) x dx).2)
Tactic:
unfold fwdFDeriv
Proof state after:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x
⊢ (fun dx => ((fun x i => f x i) x, (fderiv K (fun x i => f x i) x) dx)) = fun dx =>
    (fun i => f x i, fun i => ((fun x => f x i) x, (fderiv K (fun x => f x i) x) dx).2)
Theorem: SciLean.FwdFDeriv.pi_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.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x
⊢ (fun dx => ((fun x i => f x i) x, (fderiv K (fun x i => f x i) x) dx)) = fun dx =>
    (fun i => f x i, fun i => ((fun x => f x i) x, (fderiv K (fun x => f x i) x) dx).2)
Tactic:
fun_trans
Proof state after:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x
⊢ (fun dx => (fun i => f x i, (fderiv K (fun x i => f x i) x) dx)) = fun dx =>
    (fun i => f x i, fun i => (fderiv K (fun x => f x i) x) dx)
Theorem: SciLean.FwdFDeriv.pi_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.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x
⊢ (fun dx => (fun i => f x i, (fderiv K (fun x i => f x i) x) dx)) = fun dx =>
    (fun i => f x i, fun i => (fderiv K (fun x => f x i) x) dx)
Tactic:
funext x
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (fun i => f x✝ i, (fderiv K (fun x i => f x i) x✝) x) = (fun i => f x✝ i, fun i => (fderiv K (fun x => f x i) x✝) x)
Theorem: SciLean.FwdFDeriv.pi_rule_at
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (fun i => f x✝ i, (fderiv K (fun x i => f x i) x✝) x) = (fun i => f x✝ i, fun i => (fderiv K (fun x => f x i) x✝) x)
Tactic:
simp
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (fderiv K (fun x i => f x i) x✝) x = fun i => (fderiv K (fun x => f x i) x✝) x
Theorem: SciLean.FwdFDeriv.pi_rule_at
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (fderiv K (fun x i => f x i) x✝) x = fun i => (fderiv K (fun x => f x i) x✝) x
Tactic:
rw[fderiv_pi (h:=by fun_prop)]
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (ContinuousLinearMap.pi fun i => fderiv K (fun x => f x i) x✝) x = fun i => (fderiv K (fun x => f x i) x✝) x
Theorem: SciLean.FwdFDeriv.pi_rule_at
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ (ContinuousLinearMap.pi fun i => fderiv K (fun x => f x i) x✝) x = fun i => (fderiv K (fun x => f x i) x✝) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.pi_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.32781
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.32916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_4
inst✝² : Fintype ι
E : ι → Type u_1
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x✝ : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
x : X
⊢ ∀ (i : ι), DifferentiableAt K (fun x => f x i) x✝
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.Prod.mk.arg_fstsnd.fwdFDeriv_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.45937
inst✝² : Fintype ι
E : ι → Type ?u.45945
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
g : X → Y
hg : DifferentiableAt K g x
f : X → Z
hf : DifferentiableAt K f x
⊢ fwdFDeriv K (fun x => (g x, f x)) x = fun dx =>
    let ydy := fwdFDeriv K g x dx;
    let zdz := fwdFDeriv K f x dx;
    ((ydy.1, zdz.1), ydy.2, zdz.2)
Tactic:
unfold fwdFDeriv
Proof state after:
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.45937
inst✝² : Fintype ι
E : ι → Type ?u.45945
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
g : X → Y
hg : DifferentiableAt K g x
f : X → Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (g x, f x)) x, (fderiv K (fun x => (g x, f x)) x) dx)) = fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := (f x, (fderiv K f x) dx);
    ((ydy.1, zdz.1), ydy.2, zdz.2)
Theorem: SciLean.FwdFDeriv.Prod.mk.arg_fstsnd.fwdFDeriv_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.45937
inst✝² : Fintype ι
E : ι → Type ?u.45945
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
g : X → Y
hg : DifferentiableAt K g x
f : X → Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (g x, f x)) x, (fderiv K (fun x => (g x, f x)) x) dx)) = fun dx =>
    let ydy := (g x, (fderiv K g x) dx);
    let zdz := (f x, (fderiv K f x) dx);
    ((ydy.1, zdz.1), ydy.2, zdz.2)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.Prod.fst.arg_self.fwdFDeriv_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.54766
inst✝² : Fintype ι
E : ι → Type ?u.54774
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ fwdFDeriv K (fun x => (f x).1) x = fun dx =>
    let yzdyz := fwdFDeriv K f x dx;
    (yzdyz.1.1, yzdyz.2.1)
Tactic:
unfold fwdFDeriv
Proof state after:
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.54766
inst✝² : Fintype ι
E : ι → Type ?u.54774
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (f x).1) x, (fderiv K (fun x => (f x).1) x) dx)) = fun dx =>
    let yzdyz := (f x, (fderiv K f x) dx);
    (yzdyz.1.1, yzdyz.2.1)
Theorem: SciLean.FwdFDeriv.Prod.fst.arg_self.fwdFDeriv_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.54766
inst✝² : Fintype ι
E : ι → Type ?u.54774
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (f x).1) x, (fderiv K (fun x => (f x).1) x) dx)) = fun dx =>
    let yzdyz := (f x, (fderiv K f x) dx);
    (yzdyz.1.1, yzdyz.2.1)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.FwdFDeriv.Prod.snd.arg_self.fwdFDeriv_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.60967
inst✝² : Fintype ι
E : ι → Type ?u.60975
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ fwdFDeriv K (fun x => (f x).2) x = fun dx =>
    let yzdyz := fwdFDeriv K f x dx;
    (yzdyz.1.2, yzdyz.2.2)
Tactic:
unfold fwdFDeriv
Proof state after:
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.60967
inst✝² : Fintype ι
E : ι → Type ?u.60975
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (f x).2) x, (fderiv K (fun x => (f x).2) x) dx)) = fun dx =>
    let yzdyz := (f x, (fderiv K f x) dx);
    (yzdyz.1.2, yzdyz.2.2)
Theorem: SciLean.FwdFDeriv.Prod.snd.arg_self.fwdFDeriv_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.60967
inst✝² : Fintype ι
E : ι → Type ?u.60975
inst✝¹ : (j : ι) → NormedAddCommGroup (E j)
inst✝ : (j : ι) → NormedSpace K (E j)
x : X
f : X → Y × Z
hf : DifferentiableAt K f x
⊢ (fun dx => ((fun x => (f x).2) x, (fderiv K (fun x => (f x).2) x) dx)) = fun dx =>
    let yzdyz := (f x, (fderiv K f x) dx);
    (yzdyz.1.2, yzdyz.2.2)
Tactic:
fun_trans
Proof state after:
no goals