eqnsAtSimp.lean:2:6-2:12: warning: declaration uses `sorry`
eqnsAtSimp.lean:1:0-13:3: warning: declaration uses `sorry`