An error when using local notation

Stream: new members

[Michael Novak]

I would really appreciate if someone could explain me the reason for the error in the last lemma. I think it's because of the local notation ψ . There's no need to read most of the previous code, just look at the lemma, I'm trying to rewrite some value by using a previous lemma where I proved a formula for it:

import Mathlib

open MeasureTheory intervalIntegral

/-- This is a version of the first part of FTC for a function which is continuous on an interval.
    Credit to Aaron Liu. -/
theorem derivWithin_integral_of_continuousOn_interval {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ}
  (h : ContinuousOn f I) (x₀ x : I) : HasDerivWithinAt (fun t ↦  ∫ τ in x₀..t, f τ) (f x) I x :=
  have : intervalIntegral.FTCFilter x (nhdsWithin x I) (nhdsWithin x I) := by
    refine @intervalIntegral.FTCFilter.mk x (nhdsWithin x I) (nhdsWithin x I) ⟨?_⟩ ?_ ?_ ?_
    · rw [Filter.tendsto_smallSets_iff]
      intro t ht
      rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at ht
      obtain ⟨u, hu, hut⟩ := ht
      obtain ⟨a, b, haxb, habx, habu⟩ := exists_Icc_mem_subset_of_mem_nhds hu
      have hab : Set.Icc a b ∩ I ∈ nhdsWithin x.1 I :=
        Set.inter_comm _ _ ▸ inter_mem_nhdsWithin I habx
      filter_upwards [Filter.prod_mem_prod hab hab] with (i, j) ⟨hi, hj⟩
      refine subset_trans (Set.subset_inter ?_ ?_) hut
      · refine subset_trans ?_ habu
        intro k hk
        exact ⟨hi.1.1.trans hk.1.le, hk.2.trans hj.1.2⟩
      · intro k hk
        exact Set.Icc_subset I hi.2 hj.2 (Set.Ioc_subset_Icc_self hk)
    · exact pure_le_nhdsWithin x.2
    · exact nhdsWithin_le_nhds
    · exact @Filter.inf_isMeasurablyGenerated _ _ _ _ _
        (Set.OrdConnected.measurableSet ‹_›).principal_isMeasurablyGenerated
  intervalIntegral.integral_hasDerivWithinAt_right
    ((h.mono (Set.OrdConnected.uIcc_subset ‹_› x₀.2 x.2)).intervalIntegrable)
    (h.stronglyMeasurableAtFilter_nhdsWithin (Set.OrdConnected.measurableSet ‹_›) x)
    (h.continuousWithinAt x.2)

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def arclengthParamTransformAux (t₀ : ℝ): ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransform (t₀ : ℝ) :=
  letI ψ := arclengthParamTransformAux c t₀
  ψ⁻¹

--Unit speed / arclength reparametrization of a parametrized curve
def arclengthReparamFrom (t₀ : ℝ) : ℝ → E :=
  letI φ := arclengthParamTransform c t₀
  c ∘ φ

-- We now also assume c is a parametrized curve of class Cʳ from the interval I, r≥1.
variable (I : Set ℝ) [I.OrdConnected] (hI : IsOpen I) {r : WithTop ℕ∞}
  (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I) (t₀ : I)

--Auxilary definition, so we don't have to type the full long expression everytime
local notation3 "ψ" => arclengthParamTransformAux c t₀

/-- An auxiliary lemma giving us the derivitive of the reverse parameter transformation on I. -/
lemma revParamTransform_deriv_eq_aux (t : I) (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I)
  (hI : IsOpen I) : HasDerivWithinAt ψ ‖deriv c t‖ I t := by
  have cont_speed : ContinuousOn (fun t ↦ ‖deriv c t‖) I :=
    Continuous.comp_continuousOn' continuous_norm (hc.continuousOn_deriv_of_isOpen hI once_diff)
  unfold arclengthParamTransformAux
  exact derivWithin_integral_of_continuousOn_interval cont_speed t₀ t

#check revParamTransform_deriv_eq_aux

lemma revParamTrasform_has_pos_deriv_aux (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I)
  (regular : ∀ t : I, deriv c t ≠ 0) (t₀ : I) (hI : IsOpen I) :
  ∀ t : I, derivWithin ψ I t > 0 := by
  intro t
  rw [(revParamTransform_deriv_eq_aux c I t₀ t once_diff hc hI).derivWithin]
  sorry

[Jakub Nowak]

If you use notation instead of notation3 then I think the error is pretty clear.
If you hover over ψ in the error message then you can see its type is @arclengthParamTransformAux E inst✝² inst✝¹ c ↑t₀, while the type in the target expression is arclengthParamTransformAux c ↑t₀✝. Notice t₀✝ instead of t₀.

[Jakub Nowak]

If you remove t₀ : I from the list of arguments of revParamTrasform_has_pos_deriv_aux then rw works.

[Michael Novak]

Thank you very much! Btw, what's the difference between notation and notation3?

[Jakub Nowak]

No idea. It's the first time I see notation3. In this case, replacing notation3 with notation disables pretty printer for that notation. But I assume that you want the pretty printer, that's why I crossed it out, and provided alternative that doesn't require you to disable pretty printer.

[Chris Henson]

See docs#Mathlib.Notation3.notation3