internlm/Lean-Github huggingface dataset:
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ
Tactic:
have : HasAdjDiff R φ := sorry_proof
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ
Tactic:
simp [diracRevDeriv,revDeriv, parDistribRevDeriv, postComp]
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x_1:=w;dx), φ (x x_1)) dz) =
    fun dr ⊸[R] semiAdjoint R (∂ x w) (semiAdjoint R (∂ ⇑φ (x w)) dr)
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x_1:=w;dx), φ (x x_1)) dz) =
    fun dr ⊸[R] semiAdjoint R (∂ x w) (semiAdjoint R (∂ ⇑φ (x w)) dr)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule
Proof state before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
⊢ (parDistribRevDeriv fun w => f w + g w) = fun w =>
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
Tactic:
funext w
Proof state after:
case h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
⊢ parDistribRevDeriv (fun w => f w + g w) w =
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
⊢ parDistribRevDeriv (fun w => f w + g w) w =
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
Tactic:
ext φ
Proof state after:
case h.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).1 =
    ((let ydf := parDistribRevDeriv f w;
        let ydg := parDistribRevDeriv g w;
        ydf + ydg)
        φ).1

case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule
Proof state before:
case h.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).1 =
    ((let ydf := parDistribRevDeriv f w;
        let ydg := parDistribRevDeriv g w;
        ydf + ydg)
        φ).1

case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Tactic:
simp[parDistribRevDeriv]
Proof state after:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule
Proof state before:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Tactic:
simp[parDistribRevDeriv]
Proof state after:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ semiAdjoint R (fun dx => ∂ (x:=w;dx), ((f x) φ + (g x) φ)) x✝ =
    semiAdjoint R (fun dx => ∂ (x:=w;dx), (f x) φ) x✝ + semiAdjoint R (fun dx => ∂ (x:=w;dx), (g x) φ) x✝
Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule
Proof state before:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ semiAdjoint R (fun dx => ∂ (x:=w;dx), ((f x) φ + (g x) φ)) x✝ =
    semiAdjoint R (fun dx => ∂ (x:=w;dx), (f x) φ) x✝ + semiAdjoint R (fun dx => ∂ (x:=w;dx), (g x) φ) x✝
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiableM.pure_rule
Proof state before:
ι : Sort ?u.2726
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
⊢ CDifferentiableM K fun x => pure x
Tactic:
apply CDifferentiableM_pure
Proof state after:
case hf
ι : Sort ?u.2726
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
⊢ CDifferentiable K fun x => x
Theorem: SciLean.CDifferentiableM.pure_rule
Proof state before:
case hf
ι : Sort ?u.2726
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
⊢ CDifferentiable K fun x => x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
⊢ CDifferentiableM K fun x => y
Tactic:
have h : (fun _ : X => y)
         =
         fun _ : X => pure () >>= fun _ => y := by simp
Proof state after:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => y
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => y
Tactic:
rw[h]
Proof state after:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => do
    pure ()
    y
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => do
    pure ()
    y
Tactic:
apply CDifferentiableM_bind
Proof state after:
case hf
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => y

case hg
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => pure ()
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
case hf
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => y

case hg
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => pure ()
Tactic:
apply hy
Proof state after:
case hg
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => pure ()
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
case hg
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiableM K fun x => pure ()
Tactic:
apply CDifferentiableM_pure
Proof state after:
case hg.hf
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiable K fun x => ()
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
case hg.hf
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ CDifferentiable K fun x => ()
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.CDifferentiableM.const_rule
Proof state before:
ι : Sort ?u.3179
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
y : m Y
hy : CDifferentiableValM K y
⊢ (fun x => y) = fun x => do
    pure ()
    y
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.CDifferentiableM.comp_rule
Proof state before:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ CDifferentiableM K fun x => f (g x)
Tactic:
rw[show ((fun x => f (g x))
         =
         fun x => pure (g x) >>= f) by simp]
Proof state after:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ CDifferentiableM K fun x => pure (g x) >>= f
Theorem: SciLean.CDifferentiableM.comp_rule
Proof state before:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ CDifferentiableM K fun x => pure (g x) >>= f
Tactic:
apply CDifferentiableM_bind _ _ hf
Proof state after:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ CDifferentiableM K fun x => pure (g x)
Theorem: SciLean.CDifferentiableM.comp_rule
Proof state before:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ CDifferentiableM K fun x => pure (g x)
Tactic:
apply CDifferentiableM_pure g hg
Proof state after:
no goals
Theorem: SciLean.CDifferentiableM.comp_rule
Proof state before:
ι : Sort ?u.5269
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : Y → m Z
g : X → Y
hf : CDifferentiableM K f
hg : CDifferentiable K g
⊢ (fun x => f (g x)) = fun x => pure (g x) >>= f
Tactic:
simp
Proof state after:
no goals