α : Type ?u.17400
r : α → α → Prop
o : Ordinal
⊢ ∀ (α : Type v) (r : α → α → Prop) [inst : IsWellOrder α r], Cardinal.lift (cof (type r)) = cof (lift (type r))
α : Type ?u.17400
r : α → α → Prop
o : Ordinal
⊢ Cardinal.lift (cof o) = cof (lift o)
refine' inductionOn o _
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ Cardinal.lift (cof (type r)) = cof (lift (type r))
α : Type ?u.17400
r : α → α → Prop
o : Ordinal
⊢ ∀ (α : Type v) (r : α → α → Prop) [inst : IsWellOrder α r], Cardinal.lift (cof (type r)) = cof (lift (type r))
intro α r _
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ Cardinal.lift (cof (type r)) ≤ cof (lift (type r))

case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ Cardinal.lift (cof (type r)) = cof (lift (type r))
apply le_antisymm
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
⊢ Cardinal.lift (cof (type r)) ≤ (#↑S)
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ Cardinal.lift (cof (type r)) ≤ cof (lift (type r))
refine' le_cof_type.2 fun S H => _
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
this : Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ (#↑S)
⊢ Cardinal.lift (cof (type r)) ≤ (#↑S)
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
⊢ Cardinal.lift (cof (type r)) ≤ (#↑S)
have : Cardinal.lift.{u, v} (#(ULift.up ⁻¹' S)) ≤ (#(S : Type (max u v))) := by
  rw [← Cardinal.lift_umax.{v, u}, ← Cardinal.lift_id'.{v, u} (#S)]
  refine mk_preimage_of_injective_lift.{v, max u v} ULift.up S (ULift.up_injective.{u, v})
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
this : Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ (#↑S)
⊢ Unbounded r (ULift.up ⁻¹' S)
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
this : Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ (#↑S)
⊢ Cardinal.lift (cof (type r)) ≤ (#↑S)
refine' (Cardinal.lift_le.2 <| cof_type_le _).trans this
no goals
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
this : Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ (#↑S)
⊢ Unbounded r (ULift.up ⁻¹' S)
exact fun a =>
  let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩
  ⟨b, bs, br⟩
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
⊢ Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ Cardinal.lift (#↑S)
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
⊢ Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ (#↑S)
rw [← Cardinal.lift_umax.{v, u}, ← Cardinal.lift_id'.{v, u} (#S)]
no goals
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set (ULift { α := α, r := r, wo := inst✝ }.α)
H : Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) S
⊢ Cardinal.lift (#↑(ULift.up ⁻¹' S)) ≤ Cardinal.lift (#↑S)
refine mk_preimage_of_injective_lift.{v, max u v} ULift.up S (ULift.up_injective.{u, v})
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
case a
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
rcases cof_eq r with ⟨S, H, e'⟩
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (#↑S)
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
have : (#ULift.down.{u, v} ⁻¹' S) ≤ Cardinal.lift.{u, v} (#S) :=
  ⟨⟨fun ⟨⟨x⟩, h⟩ => ⟨⟨x, h⟩⟩, fun ⟨⟨x⟩, h₁⟩ ⟨⟨y⟩, h₂⟩ e => by
      simp at e; congr⟩⟩
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (cof (type r))
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (#↑S)
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
rw [e'] at this
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (cof (type r))
⊢ Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) (ULift.down ⁻¹' S)
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (cof (type r))
⊢ cof (lift (type r)) ≤ Cardinal.lift (cof (type r))
refine' (cof_type_le _).trans this
no goals
case a.intro.intro
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
this : (#↑(ULift.down ⁻¹' S)) ≤ Cardinal.lift (cof (type r))
⊢ Unbounded (ULift.down ⁻¹'o { α := α, r := r, wo := inst✝ }.r) (ULift.down ⁻¹' S)
exact fun ⟨a⟩ =>
  let ⟨b, bs, br⟩ := H a
  ⟨⟨b⟩, bs, br⟩
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
x✝¹ x✝ : ↑(ULift.down ⁻¹' S)
x : α
h₁ : { down := x } ∈ ULift.down ⁻¹' S
y : α
h₂ : { down := y } ∈ ULift.down ⁻¹' S
e : x = y
⊢ { val := { down := x }, property := h₁ } = { val := { down := y }, property := h₂ }
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
x✝¹ x✝ : ↑(ULift.down ⁻¹' S)
x : α
h₁ : { down := x } ∈ ULift.down ⁻¹' S
y : α
h₂ : { down := y } ∈ ULift.down ⁻¹' S
e :
  (fun x =>
        match x with
        | { val := { down := x }, property := h } => { down := { val := x, property := h } })
      { val := { down := x }, property := h₁ } =
    (fun x =>
        match x with
        | { val := { down := x }, property := h } => { down := { val := x, property := h } })
      { val := { down := y }, property := h₂ }
⊢ { val := { down := x }, property := h₁ } = { val := { down := y }, property := h₂ }
simp at e
no goals
α✝ : Type ?u.17400
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type v
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
H : Unbounded r S
e' : (#↑S) = cof (type r)
x✝¹ x✝ : ↑(ULift.down ⁻¹' S)
x : α
h₁ : { down := x } ∈ ULift.down ⁻¹' S
y : α
h₂ : { down := y } ∈ ULift.down ⁻¹' S
e : x = y
⊢ { val := { down := x }, property := h₁ } = { val := { down := y }, property := h₂ }
congr