the outputs of `∂ ... rewrite_by fun_trans` and `∂!` are different
Thank you for creating a nice library!
[Scientific Computing in Lean](https://lecopivo.github.io/scientific-computing-lean/-Differentiation/Symbolic-Differentiation/#Scientific-Computing-in-Lean---Differentiation--Symbolic-Differentiation--Notation) 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.
```lean
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?
1 条评论