sorry_proof
case funProp.discharger
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ 2 ≠ 0
no goals