set_theory.ordinal.arithmetic !4#2271

Stream: mathlib4

[Johan Commelin]

:warning: this file is not much fun

[Eric Wieser]

it looks like docs#rel_embedding.coe_fn_to_embedding and docs#rel_embedding.coe_fn_mk didn't get ported? I'd expect them to be after docs4#RelEmbedding.map_rel_iff

[Eric Wieser]

We could really do with a list of declarations from ported files in mathlib3 that don't exist in mathlib4 being shown on #port-dashboard

[Eric Wieser]

Oh, I guess here it was at least recorded:

https://github.com/leanprover-community/mathlib4/blob/f982df521660a71cd1eb4d659f23c30bb13f4cc2/Mathlib/Order/RelIso/Basic.lean#L272-L273

[Eric Wieser]

Should we abandon porting this file for now and split it first?

[Johan Commelin]

All of it has to be ported anyways

[Eric Wieser]

Two long and painful files sounds less bad than one very long and painful file

[Johan Commelin]

If it is easy to split, sure.

[Eric Wieser]

Although note that we can't actually use any backports at the moment as mathport is broken

[Eric Wieser]

#18441 does a split

[Pol'tta / Miyahara Kō]

I found the bug in add_le_of_limit. The long proof term is replaced to sorry.

theorem add_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c :=
 ⟨fun h b' l => (add_le_add_left l.le _).trans h, fun H =>
   le_of_not_lt <|
     inductionOn a sorry h H⟩
-- application type mismatch
--   inductionOn a
--     (sorryAx
--       (∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r],
--         IsLimit b → (∀ (b' : Ordinal), b' < b → type r + b' ≤ c) → ¬c < type r + b))
--     H
-- argument has type
--   ∀ (b' : Ordinal), b' < b → a + b' ≤ c
-- but function has type
--   IsLimit b → (∀ (b' : Ordinal), b' < b → a + b' ≤ c) → ¬c < a + b

The parser mistakes inductionOn a sorry h H for inductionOn a sorry H.

[Johan Commelin]

This parser mistake is very weird... I've seen it before

[Johan Commelin]

Can you trick Lean by going in tactic mode?

[Pol'tta / Miyahara Kō]

I fixed it in tactic mode.
Should we report this issue?

[Johan Commelin]

at least Mario is aware of it, because we noticed it during a video call. I never made an mwe for it.

[Johan Commelin]

@Pol'tta / Kô Miyahara Wow! You got it :check: Great work!