Theorem: Prod.mk.arg_fstsnd.revDeriv2_rule (SciLean/Core/FunctionTransformations/RevDeriv2.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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Tactic:
simp at hf hg
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Tactic:
unfold revDeriv2
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((fun w x => (g w x, f w x)) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w x => (g w x, f w x)) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let ydg :=
      (g w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => g w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let zdf :=
      ((fun x x_1 =>
            match x with
            | (w, x) => f w x)
          (w, x) (),
        fun dy =>
        match (motive := (W × X) × Unit → W × X → (W × X) × Unit)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) =>
                  (fun x x_1 =>
                      match x with
                      | (w, x) => f w x)
                    w x)
              ((w, x), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((fun w x => (g w x, f w x)) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w x => (g w x, f w x)) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let ydg :=
      (g w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => g w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let zdf :=
      ((fun x x_1 =>
            match x with
            | (w, x) => f w x)
          (w, x) (),
        fun dy =>
        match (motive := (W × X) × Unit → W × X → (W × X) × Unit)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) =>
                  (fun x x_1 =>
                      match x with
                      | (w, x) => f w x)
                    w x)
              ((w, x), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Tactic:
simp
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((g w x, f w x), fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => (g x.1 x.2, f x.1 x.2)) (w, x)) dy).1,
          (semiAdjoint K (cderiv K (fun x => (g x.1 x.2, f x.1 x.2)) (w, x)) dy).2))) =
    fun w x =>
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((g w x, f w x), fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => (g x.1 x.2, f x.1 x.2)) (w, x)) dy).1,
          (semiAdjoint K (cderiv K (fun x => (g x.1 x.2, f x.1 x.2)) (w, x)) dy).2))) =
    fun w x =>
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)
Tactic:
conv => lhs; 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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((g w x, f w x), fun dy dw' =>
        (dw' +
            ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
              (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2))) =
    fun w x =>
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((g w x, f w x), fun dy dw' =>
        (dw' +
            ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
              (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2))) =
    fun w x =>
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)
Tactic:
funext w x
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
⊢ ((g w x, f w x), fun dy dw' =>
      (dw' +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2)) =
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
⊢ ((g w x, f w x), fun dy dw' =>
      (dw' +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2)) =
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)
Tactic:
simp
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
⊢ (fun dy dw' =>
      (dw' +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2)) =
    fun dyz dw =>
    (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
        (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
      (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
⊢ (fun dy dw' =>
      (dw' +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2)) =
    fun dyz dw =>
    (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
        (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
      (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1
Tactic:
funext (dy,dz) dw
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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
        ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
      (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
        (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
      (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1

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
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
        ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
      (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
        (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
      (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1
Tactic:
ext
State after:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).1

case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).2

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).1

case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).2
Tactic:
. simp[add_assoc]; sorry_proof
State after:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).2

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).2
Tactic:
. simp; sorry_proof
State after:
no goals

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).1
Tactic:
simp[add_assoc]
State after:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dz).1 =
    (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dz).1.1

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dz).1 =
    (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dz).1.1
Tactic:
sorry_proof
State after:
no goals

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (dw +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) (dy, dz).1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) (dy, dz).2).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) (dy, dz).1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) (dy, dz).2).1).2
Tactic:
simp
State after:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dz).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dz).1.2

State before:
case h.h.h.h.a
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
dy : Y
dz : Z
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dz).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dz).1.2
Tactic:
sorry_proof
State after:
no goals