Theorem: SciLean.revDeriv2.pi_rule (SciLean/Core/FunctionTransformations/RevDeriv2.lean)

State before:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
⊢ (revDeriv2 K fun x y i => f x y i) = fun x y =>
    let xdf :=
      revDeriv2Proj K I
        (fun x x_1 =>
          match (motive := X × Y → (i : I) → EI i) x with
          | (x, y) => f x y)
        (x, y) ();
    (fun i => (xdf i).1, fun df dx' => fold (IndexType.univ I) (fun dxy i => ((xdf i).2 (df i) dxy).1) (dx', 0))
Tactic:
unfold revDeriv2Proj revDeriv2
State after:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
⊢ (fun w x =>
      ((fun x y i => f x y i) w x, fun dy =>
        match (motive := X × Y → X → X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match (motive := X × Y → (i : I) → EI i) x with
                | (w, x) => (fun x y i => f x y i) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun x y =>
    let xdf := fun i =>
      let ydf :=
        ((fun x x_1 =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (x, y) => f x y)
            (x, y) (),
          fun dy =>
          match (motive := (X × Y) × Unit → X × Y → (X × Y) × Unit)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match (motive := (X × Y) × Unit → (i : I) → EI i) x with
                  | (w, x) =>
                    (fun x x_1 =>
                        match (motive := X × Y → (i : I) → EI i) x with
                        | (x, y) => f x y)
                      w x)
                ((x, y), ()))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (fun i => (xdf i).1, fun df dx' => fold (IndexType.univ I) (fun dxy i => ((xdf i).2 (df i) dxy).1) (dx', 0))

State before:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
⊢ (fun w x =>
      ((fun x y i => f x y i) w x, fun dy =>
        match (motive := X × Y → X → X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match (motive := X × Y → (i : I) → EI i) x with
                | (w, x) => (fun x y i => f x y i) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun x y =>
    let xdf := fun i =>
      let ydf :=
        ((fun x x_1 =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (x, y) => f x y)
            (x, y) (),
          fun dy =>
          match (motive := (X × Y) × Unit → X × Y → (X × Y) × Unit)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match (motive := (X × Y) × Unit → (i : I) → EI i) x with
                  | (w, x) =>
                    (fun x x_1 =>
                        match (motive := X × Y → (i : I) → EI i) x with
                        | (x, y) => f x y)
                      w x)
                ((x, y), ()))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (fun i => (xdf i).1, fun df dx' => fold (IndexType.univ I) (fun dxy i => ((xdf i).2 (df i) dxy).1) (dx', 0))
Tactic:
funext x y
State after:
case h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
⊢ ((fun x y i => f x y i) x y, fun dy =>
      match (motive := X × Y → X → X × Y)
        semiAdjoint K
          (cderiv K
            (fun x =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (w, x) => (fun x y i => f x y i) w x)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    let xdf := fun i =>
      let ydf :=
        ((fun x x_1 =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (x, y) => f x y)
            (x, y) (),
          fun dy =>
          match (motive := (X × Y) × Unit → X × Y → (X × Y) × Unit)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match (motive := (X × Y) × Unit → (i : I) → EI i) x with
                  | (w, x) =>
                    (fun x x_1 =>
                        match (motive := X × Y → (i : I) → EI i) x with
                        | (x, y) => f x y)
                      w x)
                ((x, y), ()))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (fun i => (xdf i).1, fun df dx' => fold (IndexType.univ I) (fun dxy i => ((xdf i).2 (df i) dxy).1) (dx', 0))

State before:
case h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
⊢ ((fun x y i => f x y i) x y, fun dy =>
      match (motive := X × Y → X → X × Y)
        semiAdjoint K
          (cderiv K
            (fun x =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (w, x) => (fun x y i => f x y i) w x)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    let xdf := fun i =>
      let ydf :=
        ((fun x x_1 =>
              match (motive := X × Y → (i : I) → EI i) x with
              | (x, y) => f x y)
            (x, y) (),
          fun dy =>
          match (motive := (X × Y) × Unit → X × Y → (X × Y) × Unit)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match (motive := (X × Y) × Unit → (i : I) → EI i) x with
                  | (w, x) =>
                    (fun x x_1 =>
                        match (motive := X × Y → (i : I) → EI i) x with
                        | (x, y) => f x y)
                      w x)
                ((x, y), ()))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (fun i => (xdf i).1, fun df dx' => fold (IndexType.univ I) (fun dxy i => ((xdf i).2 (df i) dxy).1) (dx', 0))
Tactic:
simp
State after:
case h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
⊢ (fun dy dw' =>
      (dw' + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).1,
        (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).2)) =
    fun df dx' =>
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (df i))).1) (dx', 0)

State before:
case h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
⊢ (fun dy dw' =>
      (dw' + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).1,
        (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).2)) =
    fun df dx' =>
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (df i))).1) (dx', 0)
Tactic:
funext dw dx
State after:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).1,
      (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)

State before:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).1,
      (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Tactic:
conv =>
  lhs
  rw[cderiv.pi_rule (hf:=by fun_prop)]
  fun_trans
State after:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).1,
      ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)

State before:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).1,
      ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Tactic:
sorry_proof
State after:
no goals

State before:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ ∀ (i : I), CDifferentiable K fun x => f x.1 x.2 i
Tactic:
fun_prop
State after:
no goals