Cardinal lift of aleph

Stream: mathlib4

[Violeta Hernández]

Does anyone have any ideas on how to golf down this proof?

import Mathlib

open Ordinal Cardinal

theorem lift_aleph' (o : Ordinal.{u}) : lift.{v} (aleph' o) = aleph' (Ordinal.lift.{v} o) := by
  refine o.limitRecOn ?_ ?_ ?_
  · simp
  · simp
  · intro o ho IH
    rw [aleph'_limit ho, aleph'_limit ((lift_isLimit o).2 ho), lift_iSup, iSup, iSup]
    congr
    ext c
    constructor <;>
    rintro ⟨⟨a, ha : a < _⟩, rfl⟩ <;>
    dsimp
    · rw [IH _ ha]
      let x : Set.Iio (Ordinal.lift.{v, u} o) := ⟨_, Ordinal.lift_lt.2 ha⟩
      exact Set.mem_range_self x
    · obtain ⟨b, rfl⟩ := Ordinal.lift_down ha.le
      rw [Ordinal.lift_lt] at ha
      exact ⟨⟨b, ha⟩, IH _ ha⟩
    · use aleph' o
      rintro a ⟨b, rfl⟩
      exact aleph'_le.2 b.2.le

A cleaner argument would go something like "both lift ⚬ aleph' and aleph' ⚬ lift are initial segment embeddings of Ordinal.{u} → Cardinal.{max u v}, hence equal". But I don't really know how to write this down nicely.

[Daniel Weber]

import Mathlib

open Ordinal Cardinal

universe u v

def Cardinal.lift.initialSeg : @InitialSeg Cardinal.{u} Cardinal.{max u v} (· < ·) (· < ·) :=
  ⟨⟨⟨lift.{v}, fun _ _ => lift_inj.1⟩, lift_lt⟩, fun _ _ h => lift_down (le_of_lt h)⟩

theorem lift_aleph' (o : Ordinal.{u}) : lift.{v} (aleph' o) = aleph' (Ordinal.lift.{v} o) := by
  change (InitialSeg.ofIso Cardinal.Aleph'.relIso).trans Cardinal.lift.initialSeg o =
      Ordinal.lift.initialSeg.trans (InitialSeg.ofIso Cardinal.Aleph'.relIso) o
  congr!
  subsingleton

[Violeta Hernández]

Whoa, this is exactly what I was looking for. Mind if I add this to my PR #16306?

[Daniel Weber]

Sure