Theorem: SciLean.gaussian.arg_μσx.CDifferentiable_rule (SciLean/Core/Functions/Gaussian.lean)

State before:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x
hσ' : ∀ (w : W), σ w ≠ 0
⊢ CDifferentiable R fun w => gaussian (μ w) (σ w) (x w)
Tactic:
intro x
State after:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x✝ w)) x

State before:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x✝ w)) x
Tactic:
fun_prop (disch:=aesop)
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ σ x ≠ 0
Tactic:
aesop
State after:
no goals