Theorem: IndexType.sum.arg_f.revDeriv_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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (revDeriv K fun x =>  ∑ i, f x i) = fun x =>
    let ydf := revDeriv K f x;
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)
Tactic:
unfold revDeriv
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ((fun x =>  ∑ i, f x i) x, semiAdjoint K (cderiv K (fun x =>  ∑ i, f x i) x))) = fun x =>
    let ydf := (f x, semiAdjoint K (cderiv K f x));
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)

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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ((fun x =>  ∑ i, f x i) x, semiAdjoint K (cderiv K (fun x =>  ∑ i, f x i) x))) = fun x =>
    let ydf := (f x, semiAdjoint K (cderiv K f x));
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)
Tactic:
fun_trans
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ( ∑ i, f x i, fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y)) = fun x =>
    ( ∑ i, f x i, fun dy => semiAdjoint K (cderiv K f x) fun x => dy)

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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ( ∑ i, f x i, fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y)) = fun x =>
    ( ∑ i, f x i, fun dy => semiAdjoint K (cderiv K f x) fun x => dy)
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
⊢ ( ∑ i, f x i, fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y) =
    ( ∑ i, f x i, fun dy => semiAdjoint K (cderiv K f x) fun x => dy)

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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
⊢ ( ∑ i, f x i, fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y) =
    ( ∑ i, f x i, fun dy => semiAdjoint K (cderiv K f x) fun x => dy)
Tactic:
simp
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
⊢ (fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y) = fun dy =>
    semiAdjoint K (cderiv K f x) fun x => dy

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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
⊢ (fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y) = fun dy =>
    semiAdjoint K (cderiv K f x) fun x => dy
Tactic:
funext dy
State after:
case 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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
dy : Y
⊢  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) dy = semiAdjoint K (cderiv K f x) fun x => dy

State before:
case 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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
dy : Y
⊢  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) dy = semiAdjoint K (cderiv K f x) fun x => dy
Tactic:
conv => rhs; rw[cderiv.pi_rule (hf := by fun_prop)];
State after:
case 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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
dy : Y
⊢  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) dy =
    semiAdjoint K ((fun x dx i => cderiv K (fun x => f x i) x dx) x) fun x => dy

State before:
case 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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
dy : Y
⊢  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) dy =
    semiAdjoint K ((fun x dx i => cderiv K (fun x => f x i) x dx) x) fun x => dy
Tactic:
fun_trans
State after:
no goals

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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
dy : Y
⊢ ∀ (i : ι), CDifferentiable K fun x => f x i
Tactic:
fun_prop
State after:
no goals