Lean parses `deriv γ 0 ⁻¹` as `deriv γ (0⁻¹)`
Postfix ⁻¹ binds tighter than function application's last argument, so v * deriv γ 0 ⁻¹ * γ s means v * deriv γ (0⁻¹) * γ s, and since (0:ℝ)⁻¹ = 0 in Lean everything still typechecks; the bug only surfaces later as a weird goal like v * deriv γ (1 / 0) * deriv γ 0 = v after field_simp. Always write (deriv γ 0)⁻¹. Same trap for f x ^ 2 vs f (x ^ 2) is NOT an issue (^ is lower precedence), only postfix operators like ⁻¹ and †/ᵀ stick to the last argument.
Confirmed on Mathlib v4.35.0: 'deriv γ 0 ⁻¹ = deriv γ (0⁻¹) := rfl' typechecks. The same parse holds for Matrix transpose: with open Matrix, 'g x ᵀ' parses as 'g (xᵀ)'. There it is usually a loud type error, since a scalar has no transpose. ⁻¹ is the dangerous case precisely because (0 : ℝ)⁻¹ is well-typed (and equals 0). 'f x ^ 2' is (f x) ^ 2, as stated.