Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule (SciLean/Core/Distribution/SurfaceDirac.lean)

State before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (parDistribDeriv fun w => ↑fun x => f w x) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x
Tactic:
unfold parDistribDeriv
State after:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x

State before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x
Tactic:
funext x dx
State after:
case h.h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = ↑fun x_1 => ∂ (x:=x;dx), f x x_1

State before:
case h.h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = ↑fun x_1 => ∂ (x:=x;dx), f x x_1
Tactic:
ext φ
State after:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) φ = (↑fun x_1 => ∂ (x:=x;dx), f x x_1) φ

State before:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) φ = (↑fun x_1 => ∂ (x:=x;dx), f x x_1) φ
Tactic:
simp[Function.toDistribution]
State after:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ ∂ (x':=x;dx), ∫' x, φ x • f x' x = ∫' x_1, φ x_1 • ∂ (x:=x;dx), f x x_1

State before:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ ∂ (x':=x;dx), ∫' x, φ x • f x' x = ∫' x_1, φ x_1 • ∂ (x:=x;dx), f x x_1
Tactic:
sorry_proof
State after:
no goals