Cardinal lift problem

Stream: Is there code for X?

[Peter Nelson]

I've run into a strange example where exact? gives a blue underline which fails to unify.

import Mathlib

universe u u₁ u₂

open Cardinal

example (a₁ : Cardinal.{max u u₁}) (a₂ : Cardinal.{max u u₂})
    (h : lift.{max u u₁, max u u₂} a₂ = lift.{max u u₂, max u u₁} a₁) :
    lift.{u₁, max u u₂} a₂ = lift.{u₂, max u u₁} a₁ := by
  /- `exact?` gives a blue-underlined `exact lift_umax_eq.mpr h`,
    which gives
    failed to solve universe constraint
      u₁ =?= max (max u u₁) ?u.17
    while trying to unify
      lift.{u₁, max u u₂} a₂ = lift.{u₂, max u u₁} a₁ : Prop
    with
      lift.{max (max u u₁) u₂, max u u₂} a₂
      = lift.{max (max u u₂) (max u u₁) u₂, max u u₁} a₁ : Prop -/
  sorry

[Peter Nelson]

exact? giving a false positive isn't ideal, but more simply, does anyone know to prove this goal?

[Aaron Liu]

import Mathlib

universe u u₁ u₂

open Cardinal

example (a₁ : Cardinal.{max u u₁}) (a₂ : Cardinal.{max u u₂})
    (h : lift.{max u u₁, max u u₂} a₂ = lift.{max u u₂, max u u₁} a₁) :
    lift.{u₁, max u u₂} a₂ = lift.{u₂, max u u₁} a₁ := by
  conv =>
    congr
    · rw [← Cardinal.lift_umax]
    · rw [← Cardinal.lift_umax]
  conv at h =>
    congr
    · rw [← Cardinal.lift_umax]
    · rw [← Cardinal.lift_umax]
  exact h

[Aaron Liu]

This works

[Peter Nelson]

Thanks! This also works, it seems (to be clear, I only got this by looking at your proof) .

example (a₁ : Cardinal.{max u u₁}) (a₂ : Cardinal.{max u u₂})
    (h : lift.{max u u₁, max u u₂} a₂ = lift.{max u u₂, max u u₁} a₁) :
    lift.{u₁, max u u₂} a₂ = lift.{u₂, max u u₁} a₁ := by
  simp_rw [← Cardinal.lift_umax] at h ⊢
  exact h

[Kevin Buzzard]

I suspect that the problem is that the proof might work but universes might need to be explicitly supplied in the proof term. Having said that, even with pp.all on the output of exact? fails, possibly because it still prints a result with underscores for universes. Your error seems to indicate that Lean used different universes when doing the unification to the ones which it has chosen after the proof is supplied; the universe unification problem it's stuck on is clearly unsolvable.