internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivM.const_rule
Proof state before:
case hf
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiff K fun x => ()

case hf
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => y

case hg
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => pure ()
Tactic:
fun_prop
Proof state after:
case hf
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => y

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

case hg
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => pure ()
Tactic:
apply hy
Proof state after:
case hg
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => pure ()
Theorem: SciLean.revDerivM.const_rule
Proof state before:
case hg
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiffM K fun x => pure ()
Tactic:
apply HasAdjDiffM_pure
Proof state after:
case hg.hf
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiff K fun x => ()
Theorem: SciLean.revDerivM.const_rule
Proof state before:
case hg.hf
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
h :
  (fun x => y) = fun x => do
    pure ()
    y
⊢ HasAdjDiff K fun x => ()
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDerivM.const_rule
Proof state before:
ι : Sort ?u.10563
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
y : m Y
hy : HasAdjDiffValM K y
⊢ (fun x => y) = fun x => do
    pure ()
    y
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.revDerivM.comp_rule
Proof state before:
ι : Sort ?u.27735
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → m Z
g : X → Y
hf : HasAdjDiffM K f
hg : HasAdjDiff K g
⊢ (revDerivM K fun x => f (g x)) = fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K f ydg.1
    pure
        (zdf.1, fun dz => do
          let dy ← zdf.2 dz
          pure (ydg.2 dy))
Tactic:
conv =>
  lhs
  rw[show ((fun x => f (g x))
           =
           fun x => pure (g x) >>= f) by simp]
  rw[revDerivM_bind f (fun x => pure (g x))
       hf (HasAdjDiffM_pure _ hg)]
  simp[revDerivM_pure g hg]
Proof state after:
no goals
Theorem: SciLean.revDerivM.comp_rule
Proof state before:
ι : Sort ?u.27735
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → m Z
g : X → Y
hf : HasAdjDiffM K f
hg : HasAdjDiff K g
⊢ (fun x => f (g x)) = fun x => pure (g x) >>= f
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Tactic:
let f' := (fun xy : X×Y => f xy.1 xy.2)
Proof state after:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Tactic:
let g' := (fun x => (x,g x))
Proof state after:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Tactic:
have hg' : HasAdjDiff K g' := by rw[show g' = (fun x => (x,g x)) by rfl]; fun_prop
Proof state after:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
hg' : HasAdjDiff K g'
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
hg' : HasAdjDiff K g'
⊢ (revDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDeriv K g x;
    do
    let zdf ← revDerivM K (fun xy => f xy.1 xy.2) (x, ydg.1)
    pure
        (zdf.1, fun dz => do
          let dxy ← zdf.2 dz
          let dx : X := ydg.2 dxy.2
          pure (dxy.1 + dx))
Tactic:
conv =>
  lhs
  rw[show ((fun x => f x (g x))
           =
           fun x => pure (g' x) >>= f') by simp]
  rw[revDerivM_bind f' (fun x => pure (g' x)) hf (HasAdjDiffM_pure g' hg')]
  simp[revDerivM_pure (K:=K) g' hg']
  fun_trans; simp
Proof state after:
no goals
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ HasAdjDiff K g'
Tactic:
rw[show g' = (fun x => (x,g x)) by rfl]
Proof state after:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ HasAdjDiff K fun x => (x, g x)
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ HasAdjDiff K fun x => (x, g x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ g' = fun x => (x, g x)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDerivM.let_rule
Proof state before:
ι : Sort ?u.38037
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → m Z
g : X → Y
hf : HasAdjDiffM K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
hg' : HasAdjDiff K g'
⊢ (fun x => f x (g x)) = fun x => pure (g' x) >>= f'
Tactic:
simp
Proof state after:
no goals
Theorem: Pure.pure.arg_a0.HasAdjDiffM_rule
Proof state before:
ι : Sort ?u.58553
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
a0 : X → Y
ha0 : HasAdjDiff K a0
⊢ HasAdjDiffM K fun x => pure (a0 x)
Tactic:
apply RevDerivMonad.HasAdjDiffM_pure a0 ha0
Proof state after:
no goals
Theorem: Pure.pure.arg_a0.revDerivM_rule
Proof state before:
ι : Sort ?u.59125
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
a0 : X → Y
ha0 : HasAdjDiff K a0
⊢ (revDerivM K fun x => pure (a0 x)) = fun x =>
    let ydf := revDeriv K a0 x;
    pure (ydf.1, fun dy => pure (ydf.2 dy))
Tactic:
apply RevDerivMonad.revDerivM_pure a0 ha0
Proof state after:
no goals
Theorem: Pure.pure.HasAdjDiffValM_rule
Proof state before:
ι : Sort ?u.59891
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiffValM K (pure x)
Tactic:
unfold HasAdjDiffValM
Proof state after:
ι : Sort ?u.59891
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiffM K fun x_1 => pure x
Theorem: Pure.pure.HasAdjDiffValM_rule
Proof state before:
ι : Sort ?u.59891
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiffM K fun x_1 => pure x
Tactic:
apply RevDerivMonad.HasAdjDiffM_pure
Proof state after:
case hf
ι : Sort ?u.59891
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiff K fun x_1 => x
Theorem: Pure.pure.HasAdjDiffValM_rule
Proof state before:
case hf
ι : Sort ?u.59891
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiff K fun x_1 => x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Pure.pure.arg.revDerivValM_rule
Proof state before:
ι : Sort ?u.60401
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ revDerivValM K (pure x) = pure (x, fun dy => pure 0)
Tactic:
unfold revDerivValM
Proof state after:
ι : Sort ?u.60401
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ revDerivM K (fun x_1 => pure x) () = pure (x, fun dy => pure 0)
Theorem: Pure.pure.arg.revDerivValM_rule
Proof state before:
ι : Sort ?u.60401
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ revDerivM K (fun x_1 => pure x) () = pure (x, fun dy => pure 0)
Tactic:
rw[RevDerivMonad.revDerivM_pure]
Proof state after:
ι : Sort ?u.60401
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ (fun x_1 =>
        let ydf := revDeriv K (fun x_2 => x) x_1;
        pure (ydf.1, fun dy => pure (ydf.2 dy)))
      () =
    pure (x, fun dy => pure 0)

case hf
ι : Sort ?u.60401
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
⊢ HasAdjDiff K fun x_1 => x