WithTop ℤ casting not working.

Stream: new members

[Giulio Caflisch]

Please can someone explain to me why, for integers, the casting from integers to upwards extended integers is not working?

import Mathlib

open Nat

variable (p : ℕ) [hp : Fact (Nat.Prime p)]

theorem Padic.norm_lt_iff_addValuation_gt (x : ℚ_[p]) (m : ℕ) :
    ‖x‖ < (p : ℝ)^(-(m : ℤ)) ↔ Padic.addValuation x > m := by
  by_cases hx : x = 0
  · repeat rw [hx]
    rw [Padic.addValuation.map_zero]
    simp only [norm_zero, WithTop.natCast_lt_top, iff_true, zpow_neg, zpow_natCast, inv_pos]
    apply pow_pos
    rw [cast_pos]
    exact hp.out.pos
  · rw [← ne_eq] at hx
    rw [Padic.norm_eq_pow_val]
    rw [Padic.addValuation.apply]
      -- have hx' ::= solve ↑p ^ (-x.valuation) < ↑p ^ (-↑m) for x.valuation
      -- exact hx'
    rw [gt_iff_lt]
    nth_rewrite 2 [cast_lt] -- why isn't this working?
    nth_rewrite 2 [← neg_lt_neg_iff]
    apply Real.pow_lt_pow_iff_right
    · exact hx
    · exact hx

[Edward van de Meent]

it seems the issue is that the right argument you're trying to rewrite isn't Nat.cast but rather WithTop.some

[Etienne Marion]

Does this help?

rw [gt_iff_lt, ← WithTop.coe_natCast, WithTop.coe_lt_coe]

[Giulio Caflisch]

It works, thanks to both

[Giulio Caflisch]

Sorry to disturb again.

import Mathlib

open Nat

variable (p : ℕ) [hp : Fact (Nat.Prime p)]

theorem Padic.norm_lt_iff_addValuation_gt (x : ℚ_[p]) (m : ℕ) :
    ‖x‖ < (p : ℝ)^(-(m : ℤ)) ↔ Padic.addValuation x > m := by
  by_cases hx : x = 0
  · repeat rw [hx]
    rw [Padic.addValuation.map_zero]
    simp only [norm_zero, WithTop.natCast_lt_top, iff_true, zpow_neg, zpow_natCast, inv_pos]
    apply pow_pos
    rw [cast_pos]
    exact hp.out.pos
  · rw [← ne_eq] at hx
    have hp' : 1 < p := by
      apply Nat.Prime.one_lt hp.out
    rw [Padic.norm_eq_pow_val]
    rw [Padic.addValuation.apply]
      -- have hx' ::= solution_with_proof ↑p ^ (-x.valuation) < ↑p ^ (-↑m) for x.valuation
      -- exact hx'
    rw [gt_iff_lt]
    rw [← WithTop.coe_natCast, WithTop.coe_lt_coe]
    nth_rewrite 2 [← neg_lt_neg_iff]
    repeat rw [← Real.rpow_intCast]
    rw [Real.rpow_lt_rpow_left_iff]
    simp only [Int.cast_neg]
    simp only [neg_lt_neg_iff]
    sorry -- rw [Real.intCast_lt]
    · simp only [one_lt_cast]
      exact hp'
    · exact hx
    · exact hx

I need one last line to finish the proof.
In mathlib there is the theorem

Real.ratCast_lt

but I need the exact same thing byt of the form Real.intCast_lt but this doesn't exist as far as I looked in Mathlib

[Etienne Marion]

You want docs#Int.cast_lt

[Etienne Marion]

I found it by typing Int.cast, _ < _ in #loogle

[Giulio Caflisch]

Thanks a lot. I also used #loogle and somehow, searching

↑?a < ↑?b ↔ ?a < ?b

nothing useful came out.

[Etienne Marion]

I think loogle does not really know how to interpret the arrows because they can mean any coercion, so it just ignores it, thus your request is the same as _ < _ ↔ _ < _, which is too general.

[David Loeffler]

Hi Giulio! One very useful trick I find when searching for an unknown lemma is to write it down carefully as a self-contained example and then use exact?. In situations like this one, when your goal has things like ↑a involved whose meaning is context-dependent, exact? works best if you add explicit type annotations to make sure that all the types have been elaborated correctly before searching.

E.g. if you type

example (a b : ℤ) : (a : WithTop ℤ) < (b : WithTop ℤ) ↔ a < b := by exact?

in to a lean file in VSCode, it will think for a few seconds and respond Try this: exact WithTop.coe_lt_coe.