α✝ β✝ : Type u
a : Cardinal
b : Cardinal
α : Type u
β : Type (max u v)
⊢ Nonempty (β ↪ α) → ∃ a', lift a' = lift (#β)
α✝ β✝ : Type u
a : Cardinal
b : Cardinal
α : Type u
β : Type (max u v)
⊢ (#β) ≤ lift (#α) → ∃ a', lift a' = (#β)
rw [← lift_id (#β), ← lift_umax, ← lift_umax.{u, v}, lift_mk_le.{_,_,v}]
no goals
α✝ β✝ : Type u
a : Cardinal
b : Cardinal
α : Type u
β : Type (max u v)
⊢ Nonempty (β ↪ α) → ∃ a', lift a' = lift (#β)
exact fun ⟨f⟩ =>
  ⟨#Set.range f,
    Eq.symm <| lift_mk_eq.{_, _, v}.2
      ⟨Function.Embedding.equivOfSurjective (Embedding.codRestrict _ f Set.mem_range_self)
          fun ⟨a, ⟨b, e⟩⟩ => ⟨b, Subtype.eq e⟩⟩⟩