internlm/Lean-Github huggingface dataset:
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) ((starRingEnd K) (f w✝ w) * dx)
Tactic:
simp[mul_assoc,mul_comm,smul_push,add_assoc]
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
. simp[smul_push]; sorry_proof
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1
Tactic:
simp[smul_push]
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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ dw +
      ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1) =
    dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ dw +
      ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1) =
    dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
simp[smul_push]
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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
      (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
f g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
      (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.revDeriv2Proj_rule
Proof 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (revDeriv2Proj K Unit fun w x => f w x * g w x) = fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)
Tactic:
unfold revDeriv2Proj
Proof 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => f w x * g w x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)
Theorem: HMul.hMul.arg_a0a1.revDeriv2Proj_rule
Proof 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => f w x * g w x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)
Tactic:
simp only [HMul.hMul.arg_a0a1.revDeriv2_rule _ _ hf hg]
Proof 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
        ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
            ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
              dw)).1)) =
    fun w x x_1 =>
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Theorem: HMul.hMul.arg_a0a1.revDeriv2Proj_rule
Proof 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
        ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
            ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
              dw)).1)) =
    fun w x x_1 =>
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Tactic:
funext w x i
Proof state after:
case 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : Unit
⊢ (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
            dw)).1) =
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Theorem: HMul.hMul.arg_a0a1.revDeriv2Proj_rule
Proof state before:
case 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
f g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : Unit
⊢ (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
            dw)).1) =
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Tactic:
simp[revDeriv2, oneHot]
Proof state after:
no goals
Theorem: SciLean.decompose_has_unique_solution
Proof state before:
Xs : Type u_1
Ys : Type u_2
Zs : Type u_3
inst✝² : Nonempty Xs
inst✝¹ : Nonempty Ys
inst✝ : Nonempty Zs
f : Ys → Zs → Xs
hf : Function.Bijective (uncurryN 2 f)
P : Xs → Prop
Q₁ Q₂ : Ys → Zs → Prop
equiv : ∀ (ys : Ys) (zs : Zs), Q₁ ys zs ∧ Q₂ ys zs ↔ P (f ys zs)
unique : ∀ (ys : Ys), HasUniqueSolution (Q₁ ys)
⊢ HasUniqueSolution P ↔ HasUniqueSolution fun ys => Q₂ ys (solve zs, Q₁ ys zs)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.decomposeSolution
Proof state before:
Xs : Type u_1
Ys : Type u_2
Zs : Type u_3
inst✝² : Nonempty Xs
inst✝¹ : Nonempty Ys
inst✝ : Nonempty Zs
f : Ys → Zs → Xs
hf : Function.Bijective (uncurryN 2 f)
P : Xs → Prop
Q₁ Q₂ : Ys → Zs → Prop
equiv : ∀ (ys : Ys) (zs : Zs), Q₁ ys zs ∧ Q₂ ys zs ↔ P (f ys zs)
unique : ∀ (ys : Ys), HasUniqueSolution (Q₁ ys)
⊢ (solve xs, P xs) =
    let zs' := fun ys => solve zs, Q₁ ys zs;
    let ys := solve ys, Q₂ ys (zs' ys);
    let zs := zs' ys;
    f ys zs
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: getThe.arg.CDifferentiableValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.38472
inst✝² : Vec K X
Y : Type ?u.38483
inst✝¹ : Vec K Y
Z : Type ?u.38494
inst✝ : Vec K Z
⊢ CDifferentiableValM K (getThe S)
Tactic:
simp[getThe, MonadStateOf.get, StateT.get,CDifferentiableValM,CDifferentiableM]
Proof state after:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.38472
inst✝² : Vec K X
Y : Type ?u.38483
inst✝¹ : Vec K Y
Z : Type ?u.38494
inst✝ : Vec K Z
⊢ CDifferentiableM K fun xs => pure (xs.2, xs.2)
Theorem: getThe.arg.CDifferentiableValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.38472
inst✝² : Vec K X
Y : Type ?u.38483
inst✝¹ : Vec K Y
Z : Type ?u.38494
inst✝ : Vec K Z
⊢ CDifferentiableM K fun xs => pure (xs.2, xs.2)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: getThe.arg.fwdDerivValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.39987
inst✝² : Vec K X
Y : Type ?u.39998
inst✝¹ : Vec K Y
Z : Type ?u.40009
inst✝ : Vec K Z
⊢ fwdDerivValM K (getThe S) = getThe (S × S)
Tactic:
funext
Proof state after:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.39987
inst✝² : Vec K X
Y : Type ?u.39998
inst✝¹ : Vec K Y
Z : Type ?u.40009
inst✝ : Vec K Z
x✝ : S × S
⊢ fwdDerivValM K (getThe S) x✝ = getThe (S × S) x✝
Theorem: getThe.arg.fwdDerivValM_rule
Proof state before:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.39987
inst✝² : Vec K X
Y : Type ?u.39998
inst✝¹ : Vec K Y
Z : Type ?u.40009
inst✝ : Vec K Z
x✝ : S × S
⊢ fwdDerivValM K (getThe S) x✝ = getThe (S × S) x✝
Tactic:
simp[getThe, MonadStateOf.get, StateT.get,fwdDerivValM, fwdDerivM, pure, StateT.pure]
Proof state after:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.39987
inst✝² : Vec K X
Y : Type ?u.39998
inst✝¹ : Vec K Y
Z : Type ?u.40009
inst✝ : Vec K Z
x✝ : S × S
⊢ (do
      let r ← fwdDerivM K (fun xs => pure (xs.2, xs.2)) ((), x✝.1) ((), x✝.2)
      pure ((r.1.1, r.2.1), r.1.2, r.2.2)) =
    pure (x✝, x✝)
Theorem: getThe.arg.fwdDerivValM_rule
Proof state before:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.39987
inst✝² : Vec K X
Y : Type ?u.39998
inst✝¹ : Vec K Y
Z : Type ?u.40009
inst✝ : Vec K Z
x✝ : S × S
⊢ (do
      let r ← fwdDerivM K (fun xs => pure (xs.2, xs.2)) ((), x✝.1) ((), x✝.2)
      pure ((r.1.1, r.2.1), r.1.2, r.2.2)) =
    pure (x✝, x✝)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: MonadState.get.arg.CDifferentiableValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.43968
inst✝² : Vec K X
Y : Type ?u.43979
inst✝¹ : Vec K Y
Z : Type ?u.43990
inst✝ : Vec K Z
⊢ CDifferentiableValM K get
Tactic:
simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,CDifferentiableValM,CDifferentiableM]
Proof state after:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.43968
inst✝² : Vec K X
Y : Type ?u.43979
inst✝¹ : Vec K Y
Z : Type ?u.43990
inst✝ : Vec K Z
⊢ CDifferentiableM K fun xs => pure (xs.2, xs.2)
Theorem: MonadState.get.arg.CDifferentiableValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.43968
inst✝² : Vec K X
Y : Type ?u.43979
inst✝¹ : Vec K Y
Z : Type ?u.43990
inst✝ : Vec K Z
⊢ CDifferentiableM K fun xs => pure (xs.2, xs.2)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: MonadState.get.arg.fwdDerivValM_rule
Proof state before:
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.45496
inst✝² : Vec K X
Y : Type ?u.45507
inst✝¹ : Vec K Y
Z : Type ?u.45518
inst✝ : Vec K Z
⊢ fwdDerivValM K get = get
Tactic:
funext
Proof state after:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.45496
inst✝² : Vec K X
Y : Type ?u.45507
inst✝¹ : Vec K Y
Z : Type ?u.45518
inst✝ : Vec K Z
x✝ : S × S
⊢ fwdDerivValM K get x✝ = get x✝
Theorem: MonadState.get.arg.fwdDerivValM_rule
Proof state before:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.45496
inst✝² : Vec K X
Y : Type ?u.45507
inst✝¹ : Vec K Y
Z : Type ?u.45518
inst✝ : Vec K Z
x✝ : S × S
⊢ fwdDerivValM K get x✝ = get x✝
Tactic:
simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,fwdDerivValM, fwdDerivM]
Proof state after:
case h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : Vec K S
X : Type ?u.45496
inst✝² : Vec K X
Y : Type ?u.45507
inst✝¹ : Vec K Y
Z : Type ?u.45518
inst✝ : Vec K Z
x✝ : S × S
⊢ (do
      let r ← fwdDerivM K (fun xs => pure (xs.2, xs.2)) ((), x✝.1) ((), x✝.2)
      pure ((r.1.1, r.2.1), r.1.2, r.2.2)) =
    pure (x✝, x✝)