Diff vector fun iff Diff components in latest Mathlib

Stream: new members

[Michael Novak]

Aristotle gave me this solution to small part of a proof that I got stuck on:

import Mathlib

noncomputable section

theorem exam {I : Set ℝ} {c : ℝ →  EuclideanSpace ℝ (Fin 2)} (h_diff : DifferentiableOn ℝ (deriv c) I ) : DifferentiableOn ℝ (fun t ↦ !₂[-(deriv c t) 1, (deriv c t) 0]) I := by
    rw [differentiableOn_pi] at *
    intro i
    fin_cases i <;> simp [h_diff]

But the problem is that Aristole uses Mathlib version 4.24 and when I try to use this code on the latest version of Mathlib it doesn't work. In particular, the part where theorem docs#differentiableOn_pi is used, i.e., the equivalence between differentiability and components wise differentiability seems to fail, it seems like Lean can't recognize the pattern, even though it does work with the older version of Mathlib. Any suggestions how to make it work with the latest version of Mathlib?

[Ruben Van de Velde]

I tried with more explicit arguments:

import Mathlib

noncomputable section

theorem exam {I : Set ℝ} {c : ℝ →  EuclideanSpace ℝ (Fin 2)} (h_diff : DifferentiableOn ℝ (deriv c) I ) :
    DifferentiableOn ℝ (fun t ↦ !₂[-(deriv c t) 1, (deriv c t) 0]) I := by
  rw [differentiableOn_pi (𝕜 := ℝ) (Φ := (fun t ↦ !₂[-(deriv c t) 1, (deriv c t) 0])) (s := I)]
  intro i
  fin_cases i <;> simp [h_diff]

and got

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  DifferentiableOn ℝ (fun t => !₂[-(deriv c t).ofLp 1, (deriv c t).ofLp 0].ofLp) I
in the target expression
  DifferentiableOn ℝ (fun t => !₂[-(deriv c t).ofLp 1, (deriv c t).ofLp 0]) I

so it seems like it might be the result of mathlib or lean getting stricter about the equivalence between X and WithLp X

[Michael Novak]

Ruben Van de Velde said:

I tried with more explicit arguments:

import Mathlib

noncomputable section

theorem exam {I : Set ℝ} {c : ℝ →  EuclideanSpace ℝ (Fin 2)} (h_diff : DifferentiableOn ℝ (deriv c) I ) :
    DifferentiableOn ℝ (fun t ↦ !₂[-(deriv c t) 1, (deriv c t) 0]) I := by
  rw [differentiableOn_pi (𝕜 := ℝ) (Φ := (fun t ↦ !₂[-(deriv c t) 1, (deriv c t) 0])) (s := I)]
  intro i
  fin_cases i <;> simp [h_diff]

and got

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  DifferentiableOn ℝ (fun t => !₂[-(deriv c t).ofLp 1, (deriv c t).ofLp 0].ofLp) I
in the target expression
  DifferentiableOn ℝ (fun t => !₂[-(deriv c t).ofLp 1, (deriv c t).ofLp 0]) I

so it seems like it might be the result of mathlib or lean getting stricter about the equivalence between X and WithLp X

Yes, that's what I suspected as well. Thank you very much, I'll try to read more about WithLp and try to figure it out.

[Michael Novak]

O.k, turnout the solution was really simple, I just need to replace differentiableOn_pi with differentiableOn_piLp :joy: