Theorem: SciLean.revDeriv2Proj.let_rule
Proof state before:
case h.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 : W → X → Y → Z
g : W → X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ (dw +
        ((semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
              (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                    (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1),
      (semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
              (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
            (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).2) =
    (dw +
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
              (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
              (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1
Tactic:
ext
Proof state after:
case h.h.h.h.h.a
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 : W → X → Y → Z
g : W → X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ (dw +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                      (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                    (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).2).1 =
    ((dw +
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1,
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1) +
        (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1).1

case h.h.h.h.h.a
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 : W → X → Y → Z
g : W → X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ (dw +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                      (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                    (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).2).2 =
    ((dw +
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1,
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1) +
        (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1).2