Theorem: SciLean.revDerivProjUpdate.let_rule (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.179458
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.179469
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.179480
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.179505
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_4
EI : I → Type u_6
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.179669
J : Type ?u.179672
FJ : J → Type ?u.179677
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → E
g : X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (x, y) => f x y
hg : HasAdjDiff K g
⊢ (revDerivProjUpdate K I fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      revDerivProjUpdate K I
        (fun x =>
          match x with
          | (x, y) => f x y)
        (x, ydg'.1);
    (zdf'.1, fun i dei dx =>
      let dxy := zdf'.2 i dei (dx, 0);
      ydg'.2 dxy.2 dxy.1)
Tactic:
unfold revDerivProjUpdate
State after:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.179458
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.179469
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.179480
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.179505
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_4
EI : I → Type u_6
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.179669
J : Type ?u.179672
FJ : J → Type ?u.179677
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → E
g : X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (x, y) => f x y
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' :=
        revDerivProj K I
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      let ydf' :=
        revDerivProj K I
          (fun x =>
            match x with
            | (x, y) => f x y)
          (x, ydg'.1);
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (zdf'.1, fun i dei dx =>
      let dxy := zdf'.2 i dei (dx, 0);
      ydg'.2 dxy.2 dxy.1)

State before:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.179458
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.179469
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.179480
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.179505
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_4
EI : I → Type u_6
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.179669
J : Type ?u.179672
FJ : J → Type ?u.179677
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → E
g : X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (x, y) => f x y
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' :=
        revDerivProj K I
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      let ydf' :=
        revDerivProj K I
          (fun x =>
            match x with
            | (x, y) => f x y)
          (x, ydg'.1);
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (zdf'.1, fun i dei dx =>
      let dxy := zdf'.2 i dei (dx, 0);
      ydg'.2 dxy.2 dxy.1)
Tactic:
simp [revDerivProj.let_rule _ _ _ _ hf hg,add_assoc,add_comm,revDerivUpdate]
State after:
no goals