Theorem: SciLean.postExtAction_postComp (SciLean/Core/Distribution/Eval.lean)

State before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => Distribution.extAction' T φ
Tactic:
unfold Distribution.extAction'
State after:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => T.extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)

State before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => T.extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Tactic:
fun_prop
State after:
no goals

State before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => Distribution.extAction' (y u) φ
Tactic:
unfold Distribution.extAction'
State after:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => (y u).extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)

State before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => (y u).extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Tactic:
fun_prop
State after:
no goals

State before:
R : Type u_1
inst✝¹⁰ : RealScalar R
X : Type u_2
inst✝⁹ : Vec R X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
U : Type u_3
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ Distribution.postComp (Distribution.postComp x y) (fun T ⊸ Distribution.extAction' T φ) =
    Distribution.postComp x (fun u ⊸ Distribution.extAction' (y u) φ)
Tactic:
sorry_proof
State after:
no goals