coercion not being read properly in tactic state

Stream: new members

[Bashar Hamade]

Hello, I am trying to prove that if spectral radius less than 1 , then gelfand formula is also less than 1 , as I need to use this later for a bigger proof.
I found issues as the tactic state did not seem to understand the coercion . My code is :

def spectral_radius_less_than_one3 [NormedRing A] [NormedAlgebra ℂ A] (a : A) : Prop :=
  spectralRadius ℂ a < 1

theorem what_the_flop [NormedRing A] [NormedAlgebra ℂ A] (a : A) :
    Filter.limsup (fun n => ‖a ^ n‖₊ ^ (1 / n)) Filter.atTop < 1 ↔
    Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop < 1 := by
  have h : (fun n => ‖a ^ n‖₊ ^ (1 / n)) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) := by
    ext n
    simp only [← one_div]

  rw [h]


theorem gelfand_le_one_when_spectral_radius_le_one
    [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) :
    spectral_radius_less_than_one3 a →
    Filter.limsup (fun (n : ℕ) => ‖a ^ n‖₊ ^ (1 / n)) Filter.atTop < 1 := by
  intro h_spectral
  unfold spectral_radius_less_than_one3 at h_spectral
  -- Get the Gelfand formula inequality
  have h_gelfand := spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius a
  -- Now use the fact that the limsup is ≤ spectral radius < 1
  convert lt_of_le_of_lt h_gelfand h_spectral using 1
  -- This tells convert to unify at level 1, which should handle the coercions
  have h_eq : (fun (n : ℕ) => ‖a ^ n‖₊ ^ (1 / n)) = (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) := by
    ext n
    rfl

  sorry

sometimes the '↑' is not being read in the tactic state, for example in h_eq,which makes me not able to rewrite it. Also if I start the proof as proving : Filter.limsup (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop < 1 , it displays the goal in my tactic state without the coercion.
what am I missing to complete this (seemingly basic) proof?

[Aaron Liu]

The reason that there's no coercion in the tactic state is that there's actually no coercion there, it's not a bug in the display or anything. If you want to have a coercion then instead of writing in the ↑ I find that just specifying the type you want to coerce into with a type ascription usually works better. So in this case that would mean writing (‖a ^ n‖₊ : ENNReal) instead of ↑‖a ^ n‖₊ and (1 / n : ℝ) instead of 1 / ↑n.

[Aaron Liu]

The reason that there's no coercion is that Lean finds the identity coercion (coerce from α to α by doing nothing) as an acceptable solution for filling in your coercions.

[Bashar Hamade]

so my goal state right before 'sorry' is :
Filter.limsup (fun n => ‖a ^ n‖₊ ^ (1 / n)) Filter.atTop < 1 ↔ Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop < 1

shouldn't lean then be able to deduce the equivalence ? because it does not do that . Although it automatically does the coercion after I have h_eq

[Aaron Liu]

I don't see why these are equivalent. In fact, I have a strong suspicion that they are actually not equivalent.

[Bashar Hamade]

oh ok , issue is fixed..I am working with coercion for the first time and did not seem to grasp the full image.Thank you