chore: bump to v4.28.0

[zhikaip]

@or4nge19 In v4.28.0 the definition of BilinForm.Nondegenerate changed to an abbrev of LinearMap.Nondegenerate. (see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Nondegenerate.20bilinear.20.2F.20quadratic.20forms/with/568863325 and leanprover-community/mathlib4#34110). In particular, this proof in https://github.com/lean-phys-community/PhysLean/blob/master/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean broke:

@[simp]
lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) :
    (toBilinForm g x).Nondegenerate := by
  intro v hv; simp_rw [toBilinForm_apply] at hv; exact g.nondegenerate x v hv

but I thought you might want to check if the whole definition needs updating.

[zhikaip]

@jstoobysmith line 358 of https://github.com/lean-phys-community/PhysLean/blob/master/PhysLean/SpaceAndTime/Time/TimeTransMan.lean broke, the fun_prop doesn't work in v4.28.0. I tried to dig through the fun_prop trace but can't really figure out what changed, and I don't have access to physlean on v4.27.0 anymore. do you mind having a look and check what changed? (the issue is fun_prop can't prove Continuous Time.val.)

edit: managed to prove by exact Isometry.continuous fun x1 => congrFun rfl, is this correct? (Isometry Time ℝ) or definitions need tweaking? still would like to know why fun_prop previously worked but failed in v4.28.0

[jstoobysmith]

Here is a mwe:

import Mathlib 

example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Continuous f := by fun_prop -- works in v4.27.0 but not in v4.28.0

[zhikaip]

I think I managed to get both, PseudoRiemannianMetric is symmetric therefore one side is enough, the proof can probably be golfed though.

The Time.val issue is due to a change in #34345. Moved zulip discussion to new thread at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60fun_prop.60.20doesn't.20apply.20Differentiable.2Econtinuous/with/575029767

[jstoobysmith]

Approved - many thanks for being on top of this. Hopefully this was somewhat less painful then v4.27.0

[jstoobysmith]

#954 - link to issue for reference.