Theorem: Prod.mk.arg_fstsnd.revDerivProjUpdate_rule (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
⊢ (revDerivProjUpdate K (Yi ⊕ Zi) fun x => (g x, f x)) = fun x =>
    let ydg := revDerivProjUpdate K Yi g x;
    let zdf := revDerivProjUpdate K Zi f x;
    ((ydg.1, zdf.1), fun i dyz dx =>
      match i, dyz with
      | Sum.inl j, dyz => ydg.2 j dyz dx
      | Sum.inr j, dyz => zdf.2 j dyz dx)
Tactic:
unfold revDerivProjUpdate
State after:
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDerivProj K (Yi ⊕ Zi) (fun x => (g x, f x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydg :=
      let ydf' := revDerivProj K Yi g x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let zdf :=
      let ydf' := revDerivProj K Zi f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    ((ydg.1, zdf.1), fun i dyz dx =>
      match i, dyz with
      | Sum.inl j, dyz => ydg.2 j dyz dx
      | Sum.inr j, dyz => zdf.2 j dyz dx)

State before:
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDerivProj K (Yi ⊕ Zi) (fun x => (g x, f x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydg :=
      let ydf' := revDerivProj K Yi g x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let zdf :=
      let ydf' := revDerivProj K Zi f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    ((ydg.1, zdf.1), fun i dyz dx =>
      match i, dyz with
      | Sum.inl j, dyz => ydg.2 j dyz dx
      | Sum.inr j, dyz => zdf.2 j dyz dx)
Tactic:
funext x
State after:
case h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
⊢ (let ydf' := revDerivProj K (Yi ⊕ Zi) (fun x => (g x, f x)) x;
    (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    let ydg :=
      let ydf' := revDerivProj K Yi g x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let zdf :=
      let ydf' := revDerivProj K Zi f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    ((ydg.1, zdf.1), fun i dyz dx =>
      match i, dyz with
      | Sum.inl j, dyz => ydg.2 j dyz dx
      | Sum.inr j, dyz => zdf.2 j dyz dx)

State before:
case h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
⊢ (let ydf' := revDerivProj K (Yi ⊕ Zi) (fun x => (g x, f x)) x;
    (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    let ydg :=
      let ydf' := revDerivProj K Yi g x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let zdf :=
      let ydf' := revDerivProj K Zi f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    ((ydg.1, zdf.1), fun i dyz dx =>
      match i, dyz with
      | Sum.inl j, dyz => ydg.2 j dyz dx
      | Sum.inr j, dyz => zdf.2 j dyz dx)
Tactic:
fun_trans
State after:
case h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
⊢ (fun i de dx =>
      dx +
        match i, de with
        | Sum.inl j, dyz => (revDerivProj K Yi (fun x => g x) x).2 j dyz
        | Sum.inr j, dyz => (revDerivProj K Zi (fun x => f x) x).2 j dyz) =
    fun i dyz dx =>
    match i, dyz with
    | Sum.inl j, dyz => dx + (revDerivProj K Yi g x).2 j dyz
    | Sum.inr j, dyz => dx + (revDerivProj K Zi f x).2 j dyz

State before:
case h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
⊢ (fun i de dx =>
      dx +
        match i, de with
        | Sum.inl j, dyz => (revDerivProj K Yi (fun x => g x) x).2 j dyz
        | Sum.inr j, dyz => (revDerivProj K Zi (fun x => f x) x).2 j dyz) =
    fun i dyz dx =>
    match i, dyz with
    | Sum.inl j, dyz => dx + (revDerivProj K Yi g x).2 j dyz
    | Sum.inr j, dyz => dx + (revDerivProj K Zi f x).2 j dyz
Tactic:
funext i de dx
State after:
case h.h.h.h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
i : Yi ⊕ Zi
de : Sum.rec YI ZI i
dx : X
⊢ (dx +
      match i, de with
      | Sum.inl j, dyz => (revDerivProj K Yi (fun x => g x) x).2 j dyz
      | Sum.inr j, dyz => (revDerivProj K Zi (fun x => f x) x).2 j dyz) =
    match i, de with
    | Sum.inl j, dyz => dx + (revDerivProj K Yi g x).2 j dyz
    | Sum.inr j, dyz => dx + (revDerivProj K Zi f x).2 j dyz

State before:
case h.h.h.h
K : Type
inst✝²⁷ : RCLike K
X : Type
inst✝²⁶ : SemiInnerProductSpace K X
Y : Type
inst✝²⁵ : SemiInnerProductSpace K Y
Z : Type
inst✝²⁴ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
g : X → Y'
f : X → Z'
hg : HasAdjDiff K g
hf : HasAdjDiff K f
x : X
i : Yi ⊕ Zi
de : Sum.rec YI ZI i
dx : X
⊢ (dx +
      match i, de with
      | Sum.inl j, dyz => (revDerivProj K Yi (fun x => g x) x).2 j dyz
      | Sum.inr j, dyz => (revDerivProj K Zi (fun x => f x) x).2 j dyz) =
    match i, de with
    | Sum.inl j, dyz => dx + (revDerivProj K Yi g x).2 j dyz
    | Sum.inr j, dyz => dx + (revDerivProj K Zi f x).2 j dyz
Tactic:
induction i <;> simp
State after:
no goals