case refine'_1
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
a : Ordinal
ha : a < Ordinal.lift (ord c)
⊢ a < ord (lift c)

case refine'_2
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
⊢ ord (lift c) ≤ Ordinal.lift (ord c)
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
⊢ Ordinal.lift (ord c) = ord (lift c)
refine' le_antisymm (le_of_forall_lt fun a ha => _) _
case refine'_1.intro.intro
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
a : Ordinal
right✝ : a < ord c
ha : Ordinal.lift a < Ordinal.lift (ord c)
⊢ Ordinal.lift a < ord (lift c)
case refine'_1
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
a : Ordinal
ha : a < Ordinal.lift (ord c)
⊢ a < ord (lift c)
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, rfl, _⟩
no goals
case refine'_1.intro.intro
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
a : Ordinal
right✝ : a < ord c
ha : Ordinal.lift a < Ordinal.lift (ord c)
⊢ Ordinal.lift a < ord (lift c)
rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
no goals
case refine'_2
α : Type ?u.229284
β : Type ?u.229287
γ : Type ?u.229290
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
⊢ ord (lift c) ≤ Ordinal.lift (ord c)
rw [ord_le, ← lift_card, card_ord]