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?