!4#3312

Stream: mathlib4

[Jeremy Tan]

!4#3312 compiles but suffers a Name.append error in mk_real:

theorem mk_real : (#ℝ) = 𝔠 := by
  apply le_antisymm
  · rw [Real.equivCauchy.cardinal_eq]
    apply mk_quotient_le.trans
    apply (mk_subtype_le _).trans_eq
    rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
  · convert mk_le_of_injective (cantorFunction_injective _ _)
    rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
    exact 1 / 3
    norm_num
    norm_num

How do I fix the Name.append error?

[Jeremy Tan]

More specifically it's at the convert line convert mk_le_of_injective (cantorFunction_injective _ _)

[Eric Wieser]

Maybe @Kyle Miller can help, since I think they recently improved convert

[Jeremy Tan]

No, I think the same problem occurred with a closed PR that @Chris Hughes created

[Kyle Miller]

If there's a Name.append error, I'd guess it has something to do with the errors in this message and the next, which point to an error in Lean 4.

[Alex J. Best]

I think I've tracked it down, will PR in a minute

[Kyle Miller]

@Alex J. Best What did you end up tracking down?

[Alex J. Best]

!4#3314