Diagonosing a breaking change in analysis

Stream: mathlib4

[Wrenna Robson]

I have a PR up currently, but it isn't passing CI. It tweaks one definition, that of Fin.snoc, to be consistent with Fin.cons.

This is predictably causing minor breakages in various places. Most I can fix! I have a most mysterious one in the Analysis files, though. I can't seem to work out why it's happened or how to fix it.

The PR is #9571. The latest build is https://github.com/leanprover-community/mathlib4/actions/runs/7460747928/job/20299451883?pr=9571. The error I'd like help with is in Mathlib/Analysis/Calculus/FDeriv/Analytic.lean.

[Wrenna Robson]

My concern is that whatever is causing this to break in my PR, it indicates perhaps that these proofs are fairly brittle and need another look - it seems the tweak in definition is hence causing some kind of typeclass inference to fail.

[Riccardo Brasca]

It is something related to currying. In current mathlib this works

theorem HasFPowerSeriesAt.hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x := by
  refine IsBigO.trans_isLittleO (isBigO_image_sub_norm_mul_norm_sub h) ?_
  refine' IsLittleO.of_norm_right _
  refine' isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, _, EventuallyEq.rfl⟩
  refine' (continuous_id.sub continuous_const).norm.tendsto' _ _ _
  rw [_root_.id, sub_self, norm_zero]

but in your branch it gives the error (at the first line)

application type mismatch
  IsBigO.trans_isLittleO (isBigO_image_sub_norm_mul_norm_sub h)
argument
  isBigO_image_sub_norm_mul_norm_sub h
has type
  (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[nhds (x, x)] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖ : Prop
but is expected to have type
  (fun p_1 ↦ f p_1.1 - f p_1.2 - ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (p_1.1 - p_1.2)) =O[nhds (x, x)]
    ?m.12631 : Prop

[Wrenna Robson]

Ah, it seems refine rather than refine' gave different results...?

[Wrenna Robson]

In that that's a different error

[Wrenna Robson]

Not sure how to fix it though.

[Riccardo Brasca]

refine is what show term gave me with current mathlib, I don't think it is really relevant.

[Wrenna Robson]

Oh fair

[Wrenna Robson]

It's just that the error I was getting was a failure to synthesise a Norm

[Wrenna Robson]

Ultimately the issue appears to be that the proof uses (overuses?) definitional equality to work, and now something isn't fitting.

[Riccardo Brasca]

Yes, I noticed. I don't have any more time today (it is Lean together time!), but I can have a look tomorrow.

[Wrenna Robson]

Oh goodness yes so it is