-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_le {c o} : ord c ≤ o ↔ c ≤ o.card :=
  inductionOn c fun α =>
    Ordinal.inductionOn o fun β s _ => by
      let ⟨r, _, e⟩ := ord_eq α
      simp only [card_type]; constructor <;> intro h
      · rw [e] at h
        exact
          let ⟨f⟩ := h
          ⟨f.toEmbedding⟩
      · obtain ⟨f⟩ := h
        have g := RelEmbedding.preimage f s
        haveI := RelEmbedding.isWellOrder g
        exact le_trans (ord_le_type _) g.ordinal_type_le

Proof state:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : 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

Tactic:
exact le_trans (ord_le_type _) g.ordinal_type_le

Result:
no goals

Proof state:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ #β

Tactic:
rw [e] at h

Result:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ #β

Proof state:
case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ #β
⊢ (#α).ord ≤ type s

Tactic:
obtain ⟨f⟩ := h

Result:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ β
⊢ (#α).ord ≤ type s

Proof state:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ #β

Tactic:
constructor <;> intro h

Result:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ #β

case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ #β
⊢ (#α).ord ≤ type s

Proof state:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ #β

Tactic:
exact
  let ⟨f⟩ := h
  ⟨f.toEmbedding⟩

Result:
no goals

Proof state:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ β
⊢ (#α).ord ≤ type s

Tactic:
have g := RelEmbedding.preimage f s

Result:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : 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

Proof state:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
let ⟨r, _, e⟩ := ord_eq α

Result:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Proof state:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : 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

Tactic:
haveI := RelEmbedding.isWellOrder g

Result:
case mpr.intro
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : 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

Proof state:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
simp only [card_type]

Result:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ #β