α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
⊢ ∃ a, type r = succ a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
⊢ ∃ a, type r = succ a
skip
case intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = cof (type r)
⊢ ∃ a, type r = succ a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
⊢ ∃ a, type r = succ a
rcases cof_eq r with ⟨S, hl, e⟩
case intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
⊢ ∃ a, type r = succ a
case intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = cof (type r)
⊢ ∃ a, type r = succ a
rw [z] at e
case intro.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
⊢ ∃ a, type r = succ a
case intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
⊢ ∃ a, type r = succ a
cases' mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero) with a
case intro.intro.intro.refine'_1
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
⊢ ↑{b | r b ↑a} ⊕ PUnit → α

case intro.intro.intro.refine'_2
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x y : ↑{b | r b ↑a} ⊕ PUnit
⊢ Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
    r (?intro.intro.intro.refine'_1 x) (?intro.intro.intro.refine'_1 y)

case intro.intro.intro.refine'_3
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ ∃ a_1,
    ↑(RelEmbedding.ofMonotone ?intro.intro.intro.refine'_1
            (_ :
              ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                  r (?intro.intro.intro.refine'_1 x) (?intro.intro.intro.refine'_1 y)))
        a_1 =
      x
case intro.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
⊢ ∃ a, type r = succ a
refine'
  ⟨typein r a,
    Eq.symm <|
      Quotient.sound
        ⟨RelIso.ofSurjective (RelEmbedding.ofMonotone _ fun x y => _) fun x => _⟩⟩
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
⊢ 1 ≠ 0
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
⊢ (#?m.47037) ≠ 0
rw [e]
no goals
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
⊢ 1 ≠ 0
exact one_ne_zero
no goals
case intro.intro.intro.refine'_1
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
⊢ ↑{b | r b ↑a} ⊕ PUnit → α
apply Sum.rec <;> [exact Subtype.val; exact fun _ => a]
case intro.intro.intro.refine'_2.inl.inr.unit
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : ↑{b | r b ↑a}
⊢ r ↑x ↑a
case intro.intro.intro.refine'_2
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x y : ↑{b | r b ↑a} ⊕ PUnit
⊢ Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
    r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)
rcases x with (x | ⟨⟨⟨⟩⟩⟩) <;> rcases y with (y | ⟨⟨⟨⟩⟩⟩) <;>
  simp [Subrel, Order.Preimage, EmptyRelation]
no goals
case intro.intro.intro.refine'_2.inl.inr.unit
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : ↑{b | r b ↑a}
⊢ r ↑x ↑a
exact x.2
case intro.intro.intro.refine'_3
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ ∃ a_1,
    ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
            (_ :
              ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                  r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
        a_1 =
      x

case this
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
case intro.intro.intro.refine'_3
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ ∃ a_1,
    ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
            (_ :
              ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                  r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
        a_1 =
      x
suffices : r x a ∨ ∃ _ : PUnit.{u}, ↑a = x
case this
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
case intro.intro.intro.refine'_3
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ ∃ a_1,
    ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
            (_ :
              ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                  r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
        a_1 =
      x

case this
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
. convert this
  dsimp [RelEmbedding.ofMonotone]; simp
case this.inl
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r x ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

case this.inr.inl
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : x = ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

case this.inr.inr
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
case this
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
rcases trichotomous_of r x a with (h | h | h)
case a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1,
      ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
              (_ :
                ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                  Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                    r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
          a_1 =
        x) ↔
    r x ↑a ∨ ∃ x_1, ↑a = x
case intro.intro.intro.refine'_3
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ ∃ a_1,
    ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
            (_ :
              ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                  r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
        a_1 =
      x
convert this
case a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1, Sum.rec Subtype.val (fun x => ↑a) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x
case a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1,
      ↑(RelEmbedding.ofMonotone (Sum.rec Subtype.val fun x => ↑a)
              (_ :
                ∀ (x y : ↑{b | r b ↑a} ⊕ PUnit),
                  Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y →
                    r (Sum.rec Subtype.val (fun x => ↑a) x) (Sum.rec Subtype.val (fun x => ↑a) y)))
          a_1 =
        x) ↔
    r x ↑a ∨ ∃ x_1, ↑a = x
dsimp [RelEmbedding.ofMonotone]
no goals
case a
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
this : r x ↑a ∨ ∃ x_1, ↑a = x
⊢ (∃ a_1, Sum.rec Subtype.val (fun x => ↑a) a_1 = x) ↔ r x ↑a ∨ ∃ x_1, ↑a = x
simp
no goals
case this.inl
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r x ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
exact Or.inl h
no goals
case this.inr.inl
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : x = ↑a
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
exact Or.inr ⟨PUnit.unit, h.symm⟩
case this.inr.inr.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
case this.inr.inr
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
rcases hl x with ⟨a', aS, hn⟩
case this.inr.inr.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x a' : α
h : r a' x
aS : a' ∈ S
hn : ¬r a' x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x

α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ ↑a = a'
case this.inr.inr.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
rw [(_ : ↑a = a')] at h
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ a = { val := a', property := aS }
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ ↑a = a'
refine' congr_arg Subtype.val (_ : a = ⟨a', aS⟩)
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
this : Subsingleton ↑S
⊢ a = { val := a', property := aS }
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
⊢ a = { val := a', property := aS }
haveI := le_one_iff_subsingleton.1 (le_of_eq e)
no goals
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x : α
h : r (↑a) x
a' : α
aS : a' ∈ S
hn : ¬r a' x
this : Subsingleton ↑S
⊢ a = { val := a', property := aS }
apply Subsingleton.elim
no goals
case this.inr.inr.intro.intro
α✝ : Type ?u.46575
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
z : cof (type r) = 1
S : Set α
hl : Unbounded r S
e : (#↑S) = 1
a : ↑S
x a' : α
h : r a' x
aS : a' ∈ S
hn : ¬r a' x
⊢ r x ↑a ∨ ∃ x_1, ↑a = x
exact absurd h hn
no goals
α : Type ?u.46575
r : α → α → Prop
o : Ordinal
x✝ : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ cof o = 1
simp [e]