Strange error in rewriting a cardinal term

Stream: maths

[Roselyn Baxter]

Hello everyone, I've been playing around with cardinal numbers in Lean 3 as practice, and I've run into an error that I don't understand. I have the following situation:

import data.finite.basic
import set_theory.cardinal.basic

namespace cardinal
open_locale cardinal

lemma nat_eq_fin (n : ℕ) : (n : cardinal) = #(fin n) :=
sorry -- this part works, implementation omitted

protected def finite (κ : cardinal) : Prop :=
quot.lift_on κ finite (sorry /-also works-/)

example (α : Type*) : cardinal.finite (#α) = finite α :=
rfl

theorem nat_finite (n : ℕ) : cardinal.finite (n : cardinal) :=
begin
  rw nat_eq_fin n, -- error
  sorry,
end

end cardinal

The error I get is:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ↑n
state:
n : ℕ
⊢ ↑n.finite

I don't understand why the rewrite fails, the pattern should be exactly present in the goal. There is as far as I know only one coercion from nat to cardinal. Could anyone point me in the right direction?

[Kevin Buzzard]

It's a universe issue I think.

[Kevin Buzzard]

theorem nat_finite (n : ℕ) : cardinal.finite (n : cardinal.{0}) :=
begin
  rw nat_eq_fin n, -- works
  sorry,
end

[Reid Barton]

In nat_finite the universe level of n : cardinal is inferred as arbitrary, while in nat_eq_fin it has to be cardinal.{0} because that's where #(fin n) lives.

[Roselyn Baxter]

Kevin Buzzard said:

It's a universe issue I think.

Oh, you're absolutely right! Changing (n : cardinal) to (n : cardinal.{0}) in both definitions makes it work. I was hoping I was gonna be able to ignore universes, but I guess I'll need to learn how the lift function works >:/

[Kevin Buzzard]

I figured it out by doing this:

--set_option pp.all true
theorem nat_finite (n : ℕ) : cardinal.finite (n : cardinal) :=
begin
  suffices : (#(fin n)).finite,
  { rw ← nat_eq_fin n at this,
    convert this, -- ↑n.finite = ↑n.finite
    -- refl -- fails
    -- now uncomment `set_option pp.all true`
    -- and observe that the universes don't match up
    sorry, },
  sorry,
end

[Kevin Buzzard]

Reid figured it out by pure thought ;-)

[Patrick Massot]

cardinal is clearly not in the area of math where you can ignore size issues.

[Reid Barton]

I was pretty confused though until you mentioned universes.