case intro
α✝ : Type ?u.145277
r : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : Quotient.mk isEquivalent α = succ c
⊢ c < Ordinal.cof (ord (succ c))
α : Type ?u.145277
r : α → α → Prop
c : Cardinal
h : ℵ₀ ≤ c
⊢ c < Ordinal.cof (ord (succ c))
cases' Quotient.exists_rep (@succ Cardinal _ _ c) with α αe
case intro
α✝ : Type ?u.145277
r : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
⊢ c < Ordinal.cof (ord (succ c))
case intro
α✝ : Type ?u.145277
r : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : Quotient.mk isEquivalent α = succ c
⊢ c < Ordinal.cof (ord (succ c))
simp at αe
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ c < Ordinal.cof (ord (succ c))
case intro
α✝ : Type ?u.145277
r : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
⊢ c < Ordinal.cof (ord (succ c))
rcases ord_eq α with ⟨r, wo, re⟩
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ c < Ordinal.cof (ord (succ c))
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ c < Ordinal.cof (ord (succ c))
skip
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (ord (succ c))
⊢ c < Ordinal.cof (ord (succ c))
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ c < Ordinal.cof (ord (succ c))
have := ord_isLimit (h.trans (le_succ _))
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
⊢ c < Ordinal.cof (type r)
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (ord (succ c))
⊢ c < Ordinal.cof (ord (succ c))
rw [← αe, re] at this⊢
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c < Ordinal.cof (type r)
case intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
⊢ c < Ordinal.cof (type r)
rcases cof_eq' r this with ⟨S, H, Se⟩
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c < (#↑S)
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c < Ordinal.cof (type r)
rw [← Se]
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c * c < (#↑S) * c
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c < (#↑S)
apply lt_imp_lt_of_le_imp_le fun h => mul_le_mul_right' h c
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ sum fun x => c
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ c * c < (#↑S) * c
rw [mul_eq_self h, ← succ_le_iff, ← αe, ← sum_const']
case intro.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ sum fun x => card (typein r ↑x)

case intro.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
i : ↑S
⊢ (fun x => card (typein r ↑x)) i ≤ c
case intro.intro.intro.intro.intro
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ sum fun x => c
refine' le_trans _ (sum_le_sum (fun (x : S) => card (typein r (x : α))) _ fun i => _)
case intro.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ (#(i : ↑S) × { y // r y ↑i })
case intro.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ sum fun x => card (typein r ↑x)
simp only [← card_typein, ← mk_sigma]
no goals
case intro.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
⊢ (#α) ≤ (#(i : ↑S) × { y // r y ↑i })
exact
  ⟨Embedding.ofSurjective (fun x => x.2.1) fun a =>
      let ⟨b, h, ab⟩ := H a
      ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩⟩
case intro.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
i : ↑S
⊢ typein r ↑i < type r
case intro.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
i : ↑S
⊢ (fun x => card (typein r ↑x)) i ≤ c
rw [← lt_succ_iff, ← lt_ord, ← αe, re]
no goals
case intro.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.145277
r✝ : α✝ → α✝ → Prop
c : Cardinal
h : ℵ₀ ≤ c
α : Type u
αe : (#α) = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
S : Set α
H : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
Se : (#↑S) = Ordinal.cof (type r)
i : ↑S
⊢ typein r ↑i < type r
apply typein_lt_type