α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : c < Cardinal.univ
⊢ c < cof univ
α : Type ?u.103379
r : α → α → Prop
⊢ Cardinal.univ ≤ cof univ
refine' le_of_forall_lt fun c h => _
case intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : Cardinal.lift c < Cardinal.univ
⊢ Cardinal.lift c < cof univ
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : c < Cardinal.univ
⊢ c < cof univ
rcases lt_univ'.1 h with ⟨c, rfl⟩
case intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
⊢ Cardinal.lift c < (#↑S)
case intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
⊢ Cardinal.lift c < cof univ
rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]
case intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
⊢ False
case intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
⊢ Cardinal.lift c < (#↑S)
refine' lt_of_not_ge fun h => _
case intro.intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e : Cardinal.lift a = (#↑S)
⊢ False
case intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
⊢ False
cases' Cardinal.lift_down h with a e
case intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
⊢ False
case intro.intro.intro.intro
α : Type ?u.103379
r : α → α → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e : Cardinal.lift a = (#↑S)
⊢ False
refine' Quotient.inductionOn a (fun α e => _) e
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f : ULift α ≃ ↑S
⊢ False
case intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
⊢ False
cases' Quotient.exact e with f
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
⊢ False
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f : ULift α ≃ ↑S
⊢ False
have f := Equiv.ulift.symm.trans f
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
⊢ False
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
⊢ False
let g a := (f a).1
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
⊢ False
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
⊢ False
let o := succ (sup.{u, u} g)
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ False
case intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
⊢ False
rcases H o with ⟨b, h, l⟩
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ b ≤ sup g
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ False
refine' l (lt_succ_iff.2 _)
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ g (↑f.symm { val := b, property := h }) ≤ sup g
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ b ≤ sup g
rw [← show g (f.symm ⟨b, h⟩) = b by simp]
no goals
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ g (↑f.symm { val := b, property := h }) ≤ sup g
apply le_sup
no goals
α✝ : Type ?u.103379
r : α✝ → α✝ → Prop
c : Cardinal
h✝¹ : Cardinal.lift c < Cardinal.univ
S : Set Ordinal
H : Unbounded (fun x x_1 => x < x_1) S
Se : (#↑S) = cof (type fun x x_1 => x < x_1)
h✝ : Cardinal.lift c ≥ (#↑S)
a : Cardinal
e✝ : Cardinal.lift a = (#↑S)
α : Type u
e : Cardinal.lift (Quotient.mk Cardinal.isEquivalent α) = (#↑S)
f✝ : ULift α ≃ ↑S
f : α ≃ ↑S
g : α → Ordinal := fun a => ↑(↑f a)
o : Ordinal := succ (sup g)
b : Ordinal
h : b ∈ S
l : ¬(fun x x_1 => x < x_1) b o
⊢ g (↑f.symm { val := b, property := h }) = b
simp