case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
α✝ : Type ?u.171374
r : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
rcases ord_eq α with ⟨r, wo, re⟩
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
skip
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (ord (Quotient.mk isEquivalent α))
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
have := ord_isLimit h
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
⊢ (#α) < (#α) ^ Ordinal.cof (type r)
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (ord (Quotient.mk isEquivalent α))
⊢ Quotient.mk isEquivalent α < Quotient.mk isEquivalent α ^ Ordinal.cof (ord (Quotient.mk isEquivalent α))
rw [mk'_def, re] at this⊢
case intro.intro.intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
⊢ (#α) < (#α) ^ Ordinal.cof (type r)
case intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
re : ord (#α) = type r
this : Ordinal.IsLimit (type r)
⊢ (#α) < (#α) ^ Ordinal.cof (type r)
rcases cof_eq' r this with ⟨S, H, Se⟩
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (sum fun a => #{ x // r x ↑a }) < prod fun x => #α
⊢ (#α) < (#α) ^ Ordinal.cof (type r)

case intro.intro.intro.intro.refine_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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 a => #{ x // r x ↑a }) i < (fun x => #α) i
case intro.intro.intro.intro
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
⊢ (#α) < (#α) ^ Ordinal.cof (type r)
have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (#α) < (#↑S → α)
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (sum fun a => #{ x // r x ↑a }) < prod fun x => #α
⊢ (#α) < (#α) ^ Ordinal.cof (type r)
simp only [Cardinal.prod_const, Cardinal.lift_id, ← Se, ← mk_sigma, power_def] at this ⊢
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (#α) ≤ (#(i : ↑S) × { x // r x ↑i })
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (#α) < (#↑S → α)
refine' lt_of_le_of_lt _ this
case intro.intro.intro.intro.refine_2.refine'_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (i : ↑S) × { x // r x ↑i } → α

case intro.intro.intro.intro.refine_2.refine'_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ Surjective ?intro.intro.intro.intro.refine_2.refine'_1
case intro.intro.intro.intro.refine_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (#α) ≤ (#(i : ↑S) × { x // r x ↑i })
refine' ⟨Embedding.ofSurjective _ _⟩
no goals
case intro.intro.intro.intro.refine_2.refine'_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ (i : ↑S) × { x // r x ↑i } → α
exact fun x => x.2.1
no goals
case intro.intro.intro.intro.refine_2.refine'_2
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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)
this : (#(i : ↑S) × { x // r x ↑i }) < (#↑S → α)
⊢ Surjective fun x => ↑x.snd
exact fun a =>
  let ⟨b, h, ab⟩ := H a
  ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩
case intro.intro.intro.intro.refine_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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
this : typein r ↑i < type r
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i
case intro.intro.intro.intro.refine_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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 a => #{ x // r x ↑a }) i < (fun x => #α) i
have := typein_lt_type r i
no goals
case intro.intro.intro.intro.refine_1
α✝ : Type ?u.171374
r✝ : α✝ → α✝ → Prop
c : Cardinal
α : Type u
h : ℵ₀ ≤ Quotient.mk isEquivalent α
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
this : typein r ↑i < type r
⊢ (fun a => #{ x // r x ↑a }) i < (fun x => #α) i
rwa [← re, lt_ord] at this