Theorem: SciLean.parDistribRevDeriv.HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (SciLean/Core/Distribution/ParametricDistribRevDeriv.lean)

State before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
⊢ (parDistribRevDeriv fun w => f w + g w) = fun w =>
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
Tactic:
funext w
State after:
case h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
⊢ parDistribRevDeriv (fun w => f w + g w) w =
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg

State before:
case h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
⊢ parDistribRevDeriv (fun w => f w + g w) w =
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
Tactic:
ext φ
State after:
case h.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).1 =
    ((let ydf := parDistribRevDeriv f w;
        let ydg := parDistribRevDeriv g w;
        ydf + ydg)
        φ).1

case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝

State before:
case h.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).1 =
    ((let ydf := parDistribRevDeriv f w;
        let ydg := parDistribRevDeriv g w;
        ydf + ydg)
        φ).1

case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Tactic:
simp[parDistribRevDeriv]
State after:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝

State before:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
Tactic:
simp[parDistribRevDeriv]
State after:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ semiAdjoint R (fun dx => ∂ (x:=w;dx), ((f x) φ + (g x) φ)) x✝ =
    semiAdjoint R (fun dx => ∂ (x:=w;dx), (f x) φ) x✝ + semiAdjoint R (fun dx => ∂ (x:=w;dx), (g x) φ) x✝

State before:
case h.a.a.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
φ : 𝒟 X
x✝ : Y
⊢ semiAdjoint R (fun dx => ∂ (x:=w;dx), ((f x) φ + (g x) φ)) x✝ =
    semiAdjoint R (fun dx => ∂ (x:=w;dx), (f x) φ) x✝ + semiAdjoint R (fun dx => ∂ (x:=w;dx), (g x) φ) x✝
Tactic:
sorry_proof
State after:
no goals