α : Type ?u.113662
β : Type ?u.113665
γ : Type ?u.113668
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
b : Ordinal
h : b ≤ lift a
⊢ card b ≤ card (lift a)
α : Type ?u.113662
β : Type ?u.113665
γ : Type ?u.113668
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
b : Ordinal
h : b ≤ lift a
⊢ card b ≤ Cardinal.lift (card a)
rw [lift_card]
no goals
α : Type ?u.113662
β : Type ?u.113665
γ : Type ?u.113668
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
b : Ordinal
h : b ≤ lift a
⊢ card b ≤ card (lift a)
exact card_le_card h