the outputs of ∂ ... rewrite_by fun_trans and ∂! are different

[Seasawher]

Thank you for creating a nice library!

Scientific Computing in Lean says that

Writing rewrite_by fun_trans every time we want to diferentiate an expression gets a bit tedious. We can add an exclamation mark after ∂ to indicate that we want to run fun_trans tactic to compute the derivative.

However, in the following example ∂ ... rewrite_by fun_trans and ∂! have different outputs.

import SciLean.Analysis.Calculus.Notation.Deriv
import SciLean.Analysis.Scalar.Notation

open SciLean Scalar

set_default_scalar ℝ

variable {x y : ℝ}

#check
  let g : ℝ → ℝ → ℝ := fun x y => x^2 + y^2
  ∂ x, ((∂ x, (g x y)) x) rewrite_by fun_trans

#check
  let g : ℝ → ℝ → ℝ := fun x y => x^2 + y^2
  ∂! x, ((∂! x, (g x y)) x)

This is because ∂! 's bug?

[ammkrn]

It's not clear what the outputs you got were since they're not included in your issue, but as of 53f112 these produce definitionally equal terms (though the file defining the notation hasn't changed since August). It's possible something upstream was fixed, or there was just a difference in the pretty-printed output.