Theorem: SciLean.surfaceDirac_dirac (SciLean/Core/Distribution/SurfaceDirac.lean)

State before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
⊢ surfaceDirac {x} f 0 = Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)
Tactic:
ext φ
State after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (surfaceDirac {x} f 0) φ = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ

State before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (surfaceDirac {x} f 0) φ = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
unfold surfaceDirac
State after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (fun φ ⊸[R] ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x}) φ =
    (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ

State before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (fun φ ⊸[R] ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x}) φ =
    (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
dsimp
State after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x} = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ

State before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x} = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
sorry_proof
State after:
no goals