α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ card (type s)
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ ord (#α) ≤ type s ↔ (#α) ≤ card (type s)
let ⟨r, _, e⟩ := ord_eq α
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ card (type s)
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ card (type s)
skip
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ (#β)
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ card (type s)
simp only [card_type]
case mp
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : ord (#α) ≤ type s
⊢ (#α) ≤ (#β)

case mpr
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : (#α) ≤ (#β)
⊢ ord (#α) ≤ type s
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
⊢ ord (#α) ≤ type s ↔ (#α) ≤ (#β)
constructor <;> intro h
case mp
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : type r ≤ type s
⊢ (#α) ≤ (#β)
case mp
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : ord (#α) ≤ type s
⊢ (#α) ≤ (#β)
rw [e] at h
no goals
case mp
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : type r ≤ type s
⊢ (#α) ≤ (#β)
exact
  let ⟨f⟩ := h
  ⟨f.toEmbedding⟩
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
⊢ ord (#α) ≤ type s
case mpr
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
h : (#α) ≤ (#β)
⊢ ord (#α) ≤ type s
cases' h with f
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
⊢ ord (#α) ≤ type s
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
⊢ ord (#α) ≤ type s
have g := RelEmbedding.preimage f s
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ord (#α) ≤ type s
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
⊢ ord (#α) ≤ type s
haveI := RelEmbedding.isWellOrder g
no goals
case mpr.intro
α✝ : Type ?u.223328
β✝ : Type ?u.223331
γ : Type ?u.223334
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal
o : Ordinal
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord (#α) = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ord (#α) ≤ type s
exact le_trans (ord_le_type _) g.ordinal_type_le