case inl
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) = 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)

case inr
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
rcases eq_or_ne (#α) 0 with (ha | ha)
case inr
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
case inr
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
have h' : IsStrongLimit (#α) := ⟨ha, h⟩
case inr.intro.intro
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
case inr
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
rcases ord_eq α with ⟨r, wo, hr⟩
case inr.intro.intro
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
case inr.intro.intro
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
haveI := wo
case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) ≤ (#α)

case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#α) ≤ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) })
case inr.intro.intro
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
apply le_antisymm
case inl
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) = 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord 0) }) = 0
case inl
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) = 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) = (#α)
rw [ha]
no goals
case inl
α✝ : Type ?u.117471
r : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) = 0
⊢ (#{ s // (#↑s) < Ordinal.cof (ord 0) }) = 0
simp [fun s => (Cardinal.zero_le s).not_lt]
case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) ≤ (#{ s // Bounded r s })
case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) ≤ (#α)
conv_rhs => rw [← mk_bounded_subset h hr]
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (fun x =>
      Quotient.liftOn₂ (#↑x) (Ordinal.cof (ord (#α))) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
        ¬Quotient.liftOn₂ (Ordinal.cof (ord (#α))) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1) ⊆
    fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) }) ≤ (#{ s // Bounded r s })
apply mk_le_mk_of_subset
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (Ordinal.cof (ord (#α))) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
      ¬Quotient.liftOn₂ (Ordinal.cof (ord (#α))) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
⊢ s ∈ fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (fun x =>
      Quotient.liftOn₂ (#↑x) (Ordinal.cof (ord (#α))) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
        ¬Quotient.liftOn₂ (Ordinal.cof (ord (#α))) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1) ⊆
    fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
intro s hs
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (Ordinal.cof (type r)) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
      ¬Quotient.liftOn₂ (Ordinal.cof (type r)) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
⊢ s ∈ fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (Ordinal.cof (ord (#α))) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
      ¬Quotient.liftOn₂ (Ordinal.cof (ord (#α))) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
⊢ s ∈ fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
rw [hr] at hs
no goals
case inr.intro.intro.a.h
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (Ordinal.cof (type r)) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1 ∧
      ¬Quotient.liftOn₂ (Ordinal.cof (type r)) (#↑x) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
⊢ s ∈ fun x => ∃ a, ∀ (b : α), b ∈ x → r b a
exact lt_cof_type hs
case inr.intro.intro.a.refine'_1
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
x : α
⊢ (#↑{x}) < Ordinal.cof (ord (#α))

case inr.intro.intro.a.refine'_2
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ Injective fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }
case inr.intro.intro.a
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ (#α) ≤ (#{ s // (#↑s) < Ordinal.cof (ord (#α)) })
refine' @mk_le_of_injective α _ (fun x => Subtype.mk {x} _) _
case inr.intro.intro.a.refine'_1
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
x : α
⊢ 1 < Ordinal.cof (ord (#α))
case inr.intro.intro.a.refine'_1
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
x : α
⊢ (#↑{x}) < Ordinal.cof (ord (#α))
rw [mk_singleton]
no goals
case inr.intro.intro.a.refine'_1
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
x : α
⊢ 1 < Ordinal.cof (ord (#α))
exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (ord_isLimit h'.isLimit.aleph0_le))
case inr.intro.intro.a.refine'_2
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
a b : α
hab :
  (fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }) a =
    (fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }) b
⊢ a = b
case inr.intro.intro.a.refine'_2
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
⊢ Injective fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }
intro a b hab
no goals
case inr.intro.intro.a.refine'_2
α✝ : Type ?u.117471
r✝ : α✝ → α✝ → Prop
α : Type u_1
h : ∀ (x : Cardinal), x < (#α) → 2 ^ x < (#α)
ha : (#α) ≠ 0
h' : IsStrongLimit (#α)
r : α → α → Prop
wo : IsWellOrder α r
hr : ord (#α) = type r
this : IsWellOrder α r
a b : α
hab :
  (fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }) a =
    (fun x => { val := {x}, property := (_ : (#↑{x}) < Ordinal.cof (ord (#α))) }) b
⊢ a = b
simpa [singleton_eq_singleton_iff] using hab