[GOAL]
α : Type ?u.58
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
σ : Type u
x✝ : Nonempty (Cardinal.{u} ↪ σ)
f : Cardinal.{u} → σ
hf : Injective f
g : σ → Cardinal.{u} := Function.invFun f
x : σ
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ g x > sum g
[PROOFSTEP]
rw [hx]
[GOAL]
α : Type ?u.58
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
σ : Type u
x✝ : Nonempty (Cardinal.{u} ↪ σ)
f : Cardinal.{u} → σ
hf : Injective f
g : σ → Cardinal.{u} := Function.invFun f
x : σ
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ 2 ^ sum g > sum g
[PROOFSTEP]
exact cantor _
[GOAL]
α : Type ?u.20118
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : WellOrder
⊢ { α := o.α, r := o.r, wo := (_ : IsWellOrder o.α o.r) } = o
[PROOFSTEP]
cases o
[GOAL]
case mk
α : Type ?u.20118
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_3
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ { α := { α := α✝, r := r✝, wo := wo✝ }.α, r := { α := α✝, r := r✝, wo := wo✝ }.r,
      wo := (_ : IsWellOrder { α := α✝, r := r✝, wo := wo✝ }.α { α := α✝, r := r✝, wo := wo✝ }.r) } =
    { α := α✝, r := r✝, wo := wo✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.24026
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
w : WellOrder
⊢ Quotient.mk isEquivalent w = type w.r
[PROOFSTEP]
cases w
[GOAL]
case mk
α : Type ?u.24026
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_3
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } = type { α := α✝, r := r✝, wo := wo✝ }.r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
wo : IsWellOrder α r
⊢ Quotient.mk isEquivalent { α := α, r := r, wo := wo } = type r
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.24255
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ type (Quotient.out o).r = o
[PROOFSTEP]
rw [Ordinal.type, WellOrder.eta, Quotient.out_eq]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder α r
⊢ type r ≠ 0 ↔ Nonempty α
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.28990
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ IsEmpty (Quotient.out o).α ↔ o = 0
[PROOFSTEP]
rw [← @type_eq_zero_iff_isEmpty o.out.α (· < ·), type_lt]
[GOAL]
α : Type ?u.29806
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ Nonempty (Quotient.out o).α ↔ o ≠ 0
[PROOFSTEP]
rw [← @type_ne_zero_iff_nonempty o.out.α (· < ·), type_lt]
[GOAL]
α✝ : Type ?u.31118
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : β ≃ α
⊢ (type fun x y => r (↑f x) (↑f y)) = type r
[PROOFSTEP]
convert (RelIso.preimage f r).ordinal_type_eq
[GOAL]
α✝ : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69219}
h : α ≤ β
⊢ (fun x x_1 => x < x_1) ≼i fun x x_1 => x < x_1
[PROOFSTEP]
change α.out.r ≼i β.out.r
[GOAL]
α✝ : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69728}
h : α ≤ β
⊢ (Quotient.out α).r ≼i (Quotient.out β).r
[PROOFSTEP]
rw [← Quotient.out_eq α, ← Quotient.out_eq β] at h 
[GOAL]
α✝ : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69728}
h : Quotient.mk isEquivalent (Quotient.out α) ≤ Quotient.mk isEquivalent (Quotient.out β)
⊢ (Quotient.out α).r ≼i (Quotient.out β).r
[PROOFSTEP]
revert h
[GOAL]
α✝ : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69728}
⊢ Quotient.mk isEquivalent (Quotient.out α) ≤ Quotient.mk isEquivalent (Quotient.out β) →
    (Quotient.out α).r ≼i (Quotient.out β).r
[PROOFSTEP]
cases Quotient.out α
[GOAL]
case mk
α✝¹ : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝¹ → α✝¹ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69884}
α✝ : Type ?u.69884
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } ≤ Quotient.mk isEquivalent (Quotient.out β) →
    { α := α✝, r := r✝, wo := wo✝ }.r ≼i (Quotient.out β).r
[PROOFSTEP]
cases Quotient.out β
[GOAL]
case mk.mk
α✝² : Type ?u.68609
β✝ : Type u_1
γ : Type u_2
r : α✝² → α✝² → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.69942}
α✝¹ : Type ?u.69942
r✝¹ : α✝¹ → α✝¹ → Prop
wo✝¹ : IsWellOrder α✝¹ r✝¹
α✝ : Type ?u.69942
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝¹, r := r✝¹, wo := wo✝¹ } ≤
      Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } →
    { α := α✝¹, r := r✝¹, wo := wo✝¹ }.r ≼i { α := α✝, r := r✝, wo := wo✝ }.r
[PROOFSTEP]
exact Classical.choice
[GOAL]
α✝ : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.70918}
h : α < β
⊢ (fun x x_1 => x < x_1) ≺i fun x x_1 => x < x_1
[PROOFSTEP]
change α.out.r ≺i β.out.r
[GOAL]
α✝ : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.71427}
h : α < β
⊢ (Quotient.out α).r ≺i (Quotient.out β).r
[PROOFSTEP]
rw [← Quotient.out_eq α, ← Quotient.out_eq β] at h 
[GOAL]
α✝ : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.71427}
h : Quotient.mk isEquivalent (Quotient.out α) < Quotient.mk isEquivalent (Quotient.out β)
⊢ (Quotient.out α).r ≺i (Quotient.out β).r
[PROOFSTEP]
revert h
[GOAL]
α✝ : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.71427}
⊢ Quotient.mk isEquivalent (Quotient.out α) < Quotient.mk isEquivalent (Quotient.out β) →
    (Quotient.out α).r ≺i (Quotient.out β).r
[PROOFSTEP]
cases Quotient.out α
[GOAL]
case mk
α✝¹ : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝¹ → α✝¹ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.71563}
α✝ : Type ?u.71563
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } < Quotient.mk isEquivalent (Quotient.out β) →
    { α := α✝, r := r✝, wo := wo✝ }.r ≺i (Quotient.out β).r
[PROOFSTEP]
cases Quotient.out β
[GOAL]
case mk.mk
α✝² : Type ?u.70308
β✝ : Type u_1
γ : Type u_2
r : α✝² → α✝² → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.71621}
α✝¹ : Type ?u.71621
r✝¹ : α✝¹ → α✝¹ → Prop
wo✝¹ : IsWellOrder α✝¹ r✝¹
α✝ : Type ?u.71621
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝¹, r := r✝¹, wo := wo✝¹ } <
      Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } →
    { α := α✝¹, r := r✝¹, wo := wo✝¹ }.r ≺i { α := α✝, r := r✝, wo := wo✝ }.r
[PROOFSTEP]
exact Classical.choice
[GOAL]
α : Type ?u.72085
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
i : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) i < o
[PROOFSTEP]
simp_rw [← type_lt o]
[GOAL]
α : Type ?u.72085
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
i : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) i < type fun x x_1 => x < x_1
[PROOFSTEP]
apply typein_lt_type
[GOAL]
α✝ : Type ?u.73586
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i s
x✝ : ↑{b | s b f.top}
a : β
h : a ∈ {b | s b f.top}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b f.top}
            { toRelEmbedding := f.toRelEmbedding,
                init' :=
                  (_ :
                    ∀ (x : α) (x_1 : β),
                      s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) }.toRelEmbedding
            (_ : ∀ (a : α), s (↑f.toRelEmbedding a) f.top))
        a_1 =
      { val := a, property := h }
[PROOFSTEP]
rcases f.down.1 h with ⟨b, rfl⟩
[GOAL]
case intro
α✝ : Type ?u.73586
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i s
x✝ : ↑{b | s b f.top}
b : α
h : ↑f.toRelEmbedding b ∈ {b | s b f.top}
⊢ ∃ a,
    ↑(RelEmbedding.codRestrict {b | s b f.top}
            { toRelEmbedding := f.toRelEmbedding,
                init' :=
                  (_ :
                    ∀ (x : α) (x_1 : β),
                      s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) }.toRelEmbedding
            (_ : ∀ (a : α), s (↑f.toRelEmbedding a) f.top))
        a =
      { val := ↑f.toRelEmbedding b, property := h }
[PROOFSTEP]
exact ⟨b, rfl⟩
[GOAL]
α✝ : Type ?u.74324
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | r b a}
x : α
h : x ∈ {b | r b a}
⊢ ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding) { val := x, property := h } ∈
    {b | s b (↑f a)}
[PROOFSTEP]
rw [RelEmbedding.trans_apply]
[GOAL]
α✝ : Type ?u.74324
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | r b a}
x : α
h : x ∈ {b | r b a}
⊢ ↑f.toRelEmbedding (↑(Subrel.relEmbedding r {b | r b a}) { val := x, property := h }) ∈ {b | s b (↑f a)}
[PROOFSTEP]
exact f.toRelEmbedding.map_rel_iff.2 h
[GOAL]
α✝ : Type ?u.74324
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
x✝ : ↑{b | s b (↑f a)}
y : β
h : y ∈ {b | s b (↑f a)}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b (↑f a)}
            (RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding)
            (_ :
              ∀ (x : ↑{b | r b a}),
                ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a}) f.toRelEmbedding) x ∈ {b | s b (↑f a)}))
        a_1 =
      { val := y, property := h }
[PROOFSTEP]
rcases f.init h with ⟨a, rfl⟩
[GOAL]
case intro
α✝ : Type ?u.74324
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a✝ : α
x✝ : ↑{b | s b (↑f a✝)}
a : α
h : ↑f a ∈ {b | s b (↑f a✝)}
⊢ ∃ a_1,
    ↑(RelEmbedding.codRestrict {b | s b (↑f a✝)}
            (RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding)
            (_ :
              ∀ (x : ↑{b | r b a✝}),
                ↑(RelEmbedding.trans (Subrel.relEmbedding r {b | r b a✝}) f.toRelEmbedding) x ∈ {b | s b (↑f a✝)}))
        a_1 =
      { val := ↑f a, property := h }
[PROOFSTEP]
exact ⟨⟨a, f.toRelEmbedding.map_rel_iff.1 h⟩, Subtype.eq <| RelEmbedding.trans_apply _ _ _⟩
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
⊢ r a b
[PROOFSTEP]
have : f.top.1 = a := by
  let f' := PrincipalSeg.ofElement r a
  let g' := f.trans (PrincipalSeg.ofElement r b)
  have : g'.top = f'.top := by rw [Subsingleton.elim f' g']
  exact this
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
⊢ ↑f.top = a
[PROOFSTEP]
let f' := PrincipalSeg.ofElement r a
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
⊢ ↑f.top = a
[PROOFSTEP]
let g' := f.trans (PrincipalSeg.ofElement r b)
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
⊢ ↑f.top = a
[PROOFSTEP]
have : g'.top = f'.top := by rw [Subsingleton.elim f' g']
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
⊢ g'.top = f'.top
[PROOFSTEP]
rw [Subsingleton.elim f' g']
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
f' : Subrel r {b | r b a} ≺i r := PrincipalSeg.ofElement r a
g' : Subrel r {b | r b a} ≺i r := PrincipalSeg.trans f (PrincipalSeg.ofElement r b)
this : g'.top = f'.top
⊢ ↑f.top = a
[PROOFSTEP]
exact this
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r a b
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
x✝ : typein r a < typein r b
f : Subrel r {b | r b a} ≺i Subrel r {b_1 | r b_1 b}
this : ↑f.top = a
⊢ r (↑f.top) b
[PROOFSTEP]
exact f.top.2
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal.{u_3}
h₁ : o₁ < type r
h₂ : o₂ < type r
⊢ r (enum r o₁ h₁) (enum r o₂ h₂) ↔ o₁ < o₂
[PROOFSTEP]
rw [← typein_lt_typein r, typein_enum, typein_enum]
[GOAL]
α✝ : Type ?u.98270
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (hr : o < type r) (hs : o < type s), ↑f (enum r o hr) = enum s o hs
[PROOFSTEP]
refine' inductionOn o _
[GOAL]
α✝ : Type ?u.98270
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), ↑f (enum r (type r_1) hr) = enum s (type r_1) hs
[PROOFSTEP]
rintro γ t wo ⟨g⟩ ⟨h⟩
[GOAL]
case intro.intro
α✝ : Type ?u.98270
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
[PROOFSTEP]
skip
[GOAL]
case intro.intro
α✝ : Type ?u.98270
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
[PROOFSTEP]
rw [enum_type g, enum_type (PrincipalSeg.ltEquiv g f)]
[GOAL]
case intro.intro
α✝ : Type ?u.98270
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f g.top = (PrincipalSeg.ltEquiv g f).top
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type ?u.98738
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
hr : o < type r
⊢ o < type s
[PROOFSTEP]
convert hr using 1
[GOAL]
case h.e'_4
α✝ : Type ?u.98738
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
hr : o < type r
⊢ type s = type r
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case h.e'_4.a
α✝ : Type ?u.98738
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
hr : o < type r
⊢ { α := β, r := s, wo := inst✝ } ≈ { α := α, r := r, wo := inst✝¹ }
[PROOFSTEP]
exact ⟨f.symm⟩
[GOAL]
α✝ : Type ?u.99459
β : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
wo : IsWellOrder α r
a x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)
o : Ordinal.{u_3}
h : o < typein r x
⊢ Acc (fun x x_1 => x < x_1) o
[PROOFSTEP]
rcases typein_surj r (lt_trans h (typein_lt_type r _)) with ⟨b, rfl⟩
[GOAL]
case intro
α✝ : Type ?u.99459
β : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
wo : IsWellOrder α r
a x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)
b : α
h : typein r b < typein r x
⊢ Acc (fun x x_1 => x < x_1) (typein r b)
[PROOFSTEP]
exact IH _ ((typein_lt_typein r).1 h)
[GOAL]
α✝ : Type ?u.101731
β : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
x✝ : IsWellOrder α r
h : card (type r) = 0
⊢ type r = 0
[PROOFSTEP]
haveI := Cardinal.mk_eq_zero_iff.1 h
[GOAL]
α✝ : Type ?u.101731
β : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
x✝ : IsWellOrder α r
h : card (type r) = 0
this : IsEmpty { α := α, r := r, wo := x✝ }.α
⊢ type r = 0
[PROOFSTEP]
apply type_eq_zero_of_empty
[GOAL]
α : Type ?u.101731
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
e : o = 0
⊢ card o = 0
[PROOFSTEP]
simp only [e, card_zero]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type (ULift.down ⁻¹'o r) = lift (type r)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ (type fun x y => r x.down y.down) = lift (type r)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type ?u.108304
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
[PROOFSTEP]
haveI := @RelEmbedding.isWellOrder _ _ (@Equiv.ulift.{max v w} α ⁻¹'o r) r (RelIso.preimage Equiv.ulift.{max v w} r) _
[GOAL]
α✝ : Type ?u.108304
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
[PROOFSTEP]
haveI := @RelEmbedding.isWellOrder _ _ (@Equiv.ulift.{max u w} β ⁻¹'o s) s (RelIso.preimage Equiv.ulift.{max u w} s) _
[GOAL]
α✝ : Type ?u.108304
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this✝ : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
this : IsWellOrder (ULift β) (↑Equiv.ulift ⁻¹'o s)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
[PROOFSTEP]
exact
  ⟨fun ⟨f⟩ =>
    ⟨(f.equivLT (RelIso.preimage Equiv.ulift r).symm).ltLe (InitialSeg.ofIso (RelIso.preimage Equiv.ulift s))⟩,
    fun ⟨f⟩ =>
    ⟨(f.equivLT (RelIso.preimage Equiv.ulift r)).ltLe (InitialSeg.ofIso (RelIso.preimage Equiv.ulift s).symm)⟩⟩
[GOAL]
α✝ : Type ?u.110330
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift (type r) ≤ lift (type s) ↔ type r ≤ type s
[PROOFSTEP]
rw [← lift_umax]
[GOAL]
α✝ : Type ?u.110330
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift (type r) ≤ lift (type s) ↔ type r ≤ type s
[PROOFSTEP]
exact lift_type_le.{_, _, u}
[GOAL]
α : Type ?u.110723
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{v}
⊢ lift a = lift b ↔ a = b
[PROOFSTEP]
simp only [le_antisymm_iff, lift_le]
[GOAL]
α : Type ?u.110994
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{v}
⊢ lift a < lift b ↔ a < b
[PROOFSTEP]
simp only [lt_iff_le_not_le, lift_le]
[GOAL]
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
e' : Cardinal.lift #α = card (type s)
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
rw [card_type, ← Cardinal.lift_id'.{max u v, u} #β, ← Cardinal.lift_umax.{u, v}, lift_mk_eq.{u, max u v, max u v}] at e' 
[GOAL]
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
e' : Nonempty (α ≃ β)
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
cases' e' with f
[GOAL]
case intro
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
have g := RelIso.preimage f s
[GOAL]
case intro
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
haveI := (g : f ⁻¹'o s ↪r s).isWellOrder
[GOAL]
case intro
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
have := lift_type_eq.{u, max u v, max u v}.2 ⟨g⟩
[GOAL]
case intro
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = lift (type s)
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
rw [lift_id, lift_umax.{u, v}] at this 
[GOAL]
case intro
α✝ : Type ?u.112020
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal.{u}
b : Ordinal.{max u v}
h : card b ≤ Cardinal.lift a
c : Cardinal.{u}
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = type s
⊢ ∃ a', lift a' = type s
[PROOFSTEP]
exact ⟨_, this⟩
[GOAL]
α : Type ?u.113147
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
b : Ordinal.{max u v}
h : b ≤ lift a
⊢ card b ≤ Cardinal.lift (card a)
[PROOFSTEP]
rw [lift_card]
[GOAL]
α : Type ?u.113147
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
b : Ordinal.{max u v}
h : b ≤ lift a
⊢ card b ≤ card (lift a)
[PROOFSTEP]
exact card_le_card h
[GOAL]
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
⊢ ∀ {a b : (α ⊕ β) ⊕ γ},
    Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) a) (↑(sumAssoc α β γ) b) ↔ Sum.Lex (Sum.Lex r s) t a b
[PROOFSTEP]
intros a b
[GOAL]
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a b : (α ⊕ β) ⊕ γ
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) a) (↑(sumAssoc α β γ) b) ↔ Sum.Lex (Sum.Lex r s) t a b
[PROOFSTEP]
rcases a with (⟨a | a⟩ | a)
[GOAL]
case inl.inl
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
b : (α ⊕ β) ⊕ γ
a : α
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl a))) (↑(sumAssoc α β γ) b) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inl a)) b
[PROOFSTEP]
rcases b with (⟨b | b⟩ | b)
[GOAL]
case inl.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
b : (α ⊕ β) ⊕ γ
a : β
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr a))) (↑(sumAssoc α β γ) b) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inr a)) b
[PROOFSTEP]
rcases b with (⟨b | b⟩ | b)
[GOAL]
case inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
b : (α ⊕ β) ⊕ γ
a : γ
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inr a)) (↑(sumAssoc α β γ) b) ↔ Sum.Lex (Sum.Lex r s) t (Sum.inr a) b
[PROOFSTEP]
rcases b with (⟨b | b⟩ | b)
[GOAL]
case inl.inl.inl.inl
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a b : α
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl a))) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inl a)) (Sum.inl (Sum.inl b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inl.inl.inl.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : α
b : β
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl a))) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inl a)) (Sum.inl (Sum.inr b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inl.inl.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : α
b : γ
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl a))) (↑(sumAssoc α β γ) (Sum.inr b)) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inl a)) (Sum.inr b)
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inl.inr.inl.inl
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : β
b : α
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr a))) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inr a)) (Sum.inl (Sum.inl b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inl.inr.inl.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a b : β
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr a))) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inr a)) (Sum.inl (Sum.inr b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inl.inr.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : β
b : γ
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr a))) (↑(sumAssoc α β γ) (Sum.inr b)) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inl (Sum.inr a)) (Sum.inr b)
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inr.inl.inl
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : γ
b : α
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inr a)) (↑(sumAssoc α β γ) (Sum.inl (Sum.inl b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inr a) (Sum.inl (Sum.inl b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inr.inl.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a : γ
b : β
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inr a)) (↑(sumAssoc α β γ) (Sum.inl (Sum.inr b))) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inr a) (Sum.inl (Sum.inr b))
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
case inr.inr
α✝ : Type ?u.132524
β✝ : Type u_1
γ✝ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
a b : γ
⊢ Sum.Lex r (Sum.Lex s t) (↑(sumAssoc α β γ) (Sum.inr a)) (↑(sumAssoc α β γ) (Sum.inr b)) ↔
    Sum.Lex (Sum.Lex r s) t (Sum.inr a) (Sum.inr b)
[PROOFSTEP]
simp only [sumAssoc_apply_inl_inl, sumAssoc_apply_inl_inr, sumAssoc_apply_inr, Sum.lex_inl_inl, Sum.lex_inr_inr,
  Sum.Lex.sep, Sum.lex_inr_inl]
[GOAL]
α : Type ?u.137403
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
⊢ card ↑n = ↑n
[PROOFSTEP]
induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]
[GOAL]
α : Type ?u.137403
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
⊢ card ↑n = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type ?u.137403
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ card ↑Nat.zero = ↑Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type ?u.137403
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n✝ : ℕ
n_ih✝ : card ↑n✝ = ↑n✝
⊢ card ↑(Nat.succ n✝) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp only [card_add, card_one, Nat.cast_succ, *]
[GOAL]
α : Type ?u.138586
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
h : a ≤ b
⊢ c + a ≤ c + b
[PROOFSTEP]
revert h c
[GOAL]
α : Type ?u.138586
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ ∀ (c : Ordinal.{u}), a ≤ b → c + a ≤ c + b
[PROOFSTEP]
refine inductionOn a (fun α₁ r₁ _ ↦ ?_)
[GOAL]
α : Type ?u.138586
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝ : IsWellOrder α₁ r₁
⊢ ∀ (c : Ordinal.{u}), type r₁ ≤ b → c + type r₁ ≤ c + b
[PROOFSTEP]
refine inductionOn b (fun α₂ r₂ _ ↦ ?_)
[GOAL]
α : Type ?u.138586
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝¹ : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝ : IsWellOrder α₂ r₂
⊢ ∀ (c : Ordinal.{u}), type r₁ ≤ type r₂ → c + type r₁ ≤ c + type r₂
[PROOFSTEP]
rintro c ⟨⟨⟨f, fo⟩, fi⟩⟩
[GOAL]
case intro.mk.mk
α : Type ?u.138586
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝¹ : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
⊢ c + type r₁ ≤ c + type r₂
[PROOFSTEP]
refine inductionOn c (fun β s _ ↦ ?_)
[GOAL]
case intro.mk.mk
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type s + type r₁ ≤ type s + type r₂
[PROOFSTEP]
have := (Embedding.refl β).sumMap f
[GOAL]
case intro.mk.mk
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
⊢ type s + type r₁ ≤ type s + type r₂
[PROOFSTEP]
refine ⟨⟨⟨(Embedding.refl.{u + 1} _).sumMap f, ?_⟩, ?_⟩⟩
[GOAL]
case intro.mk.mk.refine_1
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
⊢ ∀ {a b : β ⊕ α₁},
    Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
      Sum.Lex s r₁ a b
[PROOFSTEP]
intros a b
[GOAL]
case intro.mk.mk.refine_1
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a b : β ⊕ α₁
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
    Sum.Lex s r₁ a b
[PROOFSTEP]
match a, b with
| Sum.inl a, Sum.inl b => exact Sum.lex_inl_inl.trans Sum.lex_inl_inl.symm
| Sum.inl a, Sum.inr b => apply iff_of_true <;> apply Sum.Lex.sep
| Sum.inr a, Sum.inl b => apply iff_of_false <;> exact Sum.lex_inr_inl
| Sum.inr a, Sum.inr b => exact Sum.lex_inr_inr.trans <| fo.trans Sum.lex_inr_inr.symm
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a b : β
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl a))
      (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl b)) ↔
    Sum.Lex s r₁ (Sum.inl a) (Sum.inl b)
[PROOFSTEP]
exact Sum.lex_inl_inl.trans Sum.lex_inl_inl.symm
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : β
b : α₁
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl a))
      (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr b)) ↔
    Sum.Lex s r₁ (Sum.inl a) (Sum.inr b)
[PROOFSTEP]
apply iff_of_true
[GOAL]
case ha
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : β
b : α₁
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl a))
    (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr b))
[PROOFSTEP]
apply Sum.Lex.sep
[GOAL]
case hb
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : β
b : α₁
⊢ Sum.Lex s r₁ (Sum.inl a) (Sum.inr b)
[PROOFSTEP]
apply Sum.Lex.sep
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : α₁
b : β
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr a))
      (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl b)) ↔
    Sum.Lex s r₁ (Sum.inr a) (Sum.inl b)
[PROOFSTEP]
apply iff_of_false
[GOAL]
case ha
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : α₁
b : β
⊢ ¬Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr a))
      (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inl b))
[PROOFSTEP]
exact Sum.lex_inr_inl
[GOAL]
case hb
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a : α₁
b : β
⊢ ¬Sum.Lex s r₁ (Sum.inr a) (Sum.inl b)
[PROOFSTEP]
exact Sum.lex_inr_inl
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ b✝ : β ⊕ α₁
a b : α₁
⊢ Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr a))
      (↑(Embedding.sumMap (Embedding.refl β) f) (Sum.inr b)) ↔
    Sum.Lex s r₁ (Sum.inr a) (Sum.inr b)
[PROOFSTEP]
exact Sum.lex_inr_inr.trans <| fo.trans Sum.lex_inr_inr.symm
[GOAL]
case intro.mk.mk.refine_2
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
⊢ ∀ (a : β ⊕ α₁) (b : β ⊕ α₂),
    Sum.Lex s r₂ b
        (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
              map_rel_iff' :=
                (_ :
                  ∀ {a b : β ⊕ α₁},
                    Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                        (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                      Sum.Lex s r₁ a b) }
          a) →
      ∃ a',
        ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
                map_rel_iff' :=
                  (_ :
                    ∀ {a b : β ⊕ α₁},
                      Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                          (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                        Sum.Lex s r₁ a b) }
            a' =
          b
[PROOFSTEP]
intros a b H
[GOAL]
case intro.mk.mk.refine_2
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a : β ⊕ α₁
b : β ⊕ α₂
H :
  Sum.Lex s r₂ b
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      a)
⊢ ∃ a',
    ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
            map_rel_iff' :=
              (_ :
                ∀ {a b : β ⊕ α₁},
                  Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                      (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                    Sum.Lex s r₁ a b) }
        a' =
      b
[PROOFSTEP]
match a, b, H with
| _, Sum.inl b, _ => exact ⟨Sum.inl b, rfl⟩
| Sum.inl a, Sum.inr b, H => exact (Sum.lex_inr_inl H).elim
| Sum.inr a, Sum.inr b, H =>
  let ⟨w, h⟩ := fi _ _ (Sum.lex_inr_inr.1 H)
  exact ⟨Sum.inr w, congr_arg Sum.inr h⟩
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝⁴ : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝³ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a : β ⊕ α₁
b✝ : β ⊕ α₂
H :
  Sum.Lex s r₂ b✝
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      a)
x✝¹ : β ⊕ α₁
b : β
x✝ :
  Sum.Lex s r₂ (Sum.inl b)
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      x✝¹)
⊢ ∃ a',
    ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
            map_rel_iff' :=
              (_ :
                ∀ {a b : β ⊕ α₁},
                  Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                      (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                    Sum.Lex s r₁ a b) }
        a' =
      Sum.inl b
[PROOFSTEP]
exact ⟨Sum.inl b, rfl⟩
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ : β ⊕ α₁
b✝ : β ⊕ α₂
H✝ :
  Sum.Lex s r₂ b✝
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      a✝)
a : β
b : α₂
H :
  Sum.Lex s r₂ (Sum.inr b)
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      (Sum.inl a))
⊢ ∃ a',
    ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
            map_rel_iff' :=
              (_ :
                ∀ {a b : β ⊕ α₁},
                  Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                      (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                    Sum.Lex s r₁ a b) }
        a' =
      Sum.inr b
[PROOFSTEP]
exact (Sum.lex_inr_inl H).elim
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ : β ⊕ α₁
b✝ : β ⊕ α₂
H✝ :
  Sum.Lex s r₂ b✝
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      a✝)
a : α₁
b : α₂
H :
  Sum.Lex s r₂ (Sum.inr b)
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      (Sum.inr a))
⊢ ∃ a',
    ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
            map_rel_iff' :=
              (_ :
                ∀ {a b : β ⊕ α₁},
                  Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                      (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                    Sum.Lex s r₁ a b) }
        a' =
      Sum.inr b
[PROOFSTEP]
let ⟨w, h⟩ := fi _ _ (Sum.lex_inr_inr.1 H)
[GOAL]
α : Type ?u.138586
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝¹ b✝¹ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
this : β ⊕ α₁ ↪ β ⊕ α₂
a✝ : β ⊕ α₁
b✝ : β ⊕ α₂
H✝ :
  Sum.Lex s r₂ b✝
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      a✝)
a : α₁
b : α₂
H :
  Sum.Lex s r₂ (Sum.inr b)
    (↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
          map_rel_iff' :=
            (_ :
              ∀ {a b : β ⊕ α₁},
                Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a) (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                  Sum.Lex s r₁ a b) }
      (Sum.inr a))
w : α₁
h : ↑{ toEmbedding := f, map_rel_iff' := fo } w = b
⊢ ∃ a',
    ↑{ toEmbedding := Embedding.sumMap (Embedding.refl β) f,
            map_rel_iff' :=
              (_ :
                ∀ {a b : β ⊕ α₁},
                  Sum.Lex s r₂ (↑(Embedding.sumMap (Embedding.refl β) f) a)
                      (↑(Embedding.sumMap (Embedding.refl β) f) b) ↔
                    Sum.Lex s r₁ a b) }
        a' =
      Sum.inr b
[PROOFSTEP]
exact ⟨Sum.inr w, congr_arg Sum.inr h⟩
[GOAL]
α : Type ?u.140748
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
h : a ≤ b
⊢ Function.swap (fun x x_1 => x + x_1) c a ≤ Function.swap (fun x x_1 => x + x_1) c b
[PROOFSTEP]
revert h c
[GOAL]
α : Type ?u.140748
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ ∀ (c : Ordinal.{u}), a ≤ b → Function.swap (fun x x_1 => x + x_1) c a ≤ Function.swap (fun x x_1 => x + x_1) c b
[PROOFSTEP]
refine inductionOn a (fun α₁ r₁ _ ↦ ?_)
[GOAL]
α : Type ?u.140748
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝ : IsWellOrder α₁ r₁
⊢ ∀ (c : Ordinal.{u}),
    type r₁ ≤ b → Function.swap (fun x x_1 => x + x_1) c (type r₁) ≤ Function.swap (fun x x_1 => x + x_1) c b
[PROOFSTEP]
refine inductionOn b (fun α₂ r₂ _ ↦ ?_)
[GOAL]
α : Type ?u.140748
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝¹ : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝ : IsWellOrder α₂ r₂
⊢ ∀ (c : Ordinal.{u}),
    type r₁ ≤ type r₂ →
      Function.swap (fun x x_1 => x + x_1) c (type r₁) ≤ Function.swap (fun x x_1 => x + x_1) c (type r₂)
[PROOFSTEP]
rintro c ⟨⟨⟨f, fo⟩, fi⟩⟩
[GOAL]
case intro.mk.mk
α : Type ?u.140748
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝¹ : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
⊢ Function.swap (fun x x_1 => x + x_1) c (type r₁) ≤ Function.swap (fun x x_1 => x + x_1) c (type r₂)
[PROOFSTEP]
refine inductionOn c (fun β s _ ↦ ?_)
[GOAL]
case intro.mk.mk
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ Function.swap (fun x x_1 => x + x_1) (type s) (type r₁) ≤ Function.swap (fun x x_1 => x + x_1) (type s) (type r₂)
[PROOFSTEP]
exact
  @RelEmbedding.ordinal_type_le _ _ (Sum.Lex r₁ s) (Sum.Lex r₂ s) _ _
    ⟨f.sumMap (Embedding.refl _), by
      intro a b
      constructor <;> intro H
      · cases' a with a a <;> cases' b with b b <;> cases H <;> constructor <;> [rwa [← fo]; assumption]
      · cases H <;> constructor <;> [rwa [fo]; assumption]⟩
[GOAL]
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ ∀ {a b : α₁ ⊕ β},
    Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b) ↔
      Sum.Lex r₁ s a b
[PROOFSTEP]
intro a b
[GOAL]
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b) ↔
    Sum.Lex r₁ s a b
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b) →
    Sum.Lex r₁ s a b
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
⊢ Sum.Lex r₁ s a b →
    Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b)
[PROOFSTEP]
intro H
[GOAL]
case mp
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
H : Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b)
⊢ Sum.Lex r₁ s a b
[PROOFSTEP]
cases' a with a a <;> cases' b with b b <;> cases H <;> constructor <;> [rwa [← fo]; assumption]
[GOAL]
case mp
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
H : Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b)
⊢ Sum.Lex r₁ s a b
[PROOFSTEP]
cases' a with a a
[GOAL]
case mp.inl
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
b : α₁ ⊕ β
a : α₁
H : Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a)) (↑(Embedding.sumMap f (Embedding.refl β)) b)
⊢ Sum.Lex r₁ s (Sum.inl a) b
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
b : α₁ ⊕ β
a : β
H : Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr a)) (↑(Embedding.sumMap f (Embedding.refl β)) b)
⊢ Sum.Lex r₁ s (Sum.inr a) b
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inl.inl
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁
H :
  Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl b))
⊢ Sum.Lex r₁ s (Sum.inl a) (Sum.inl b)
[PROOFSTEP]
cases H
[GOAL]
case mp.inl.inr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a : α₁
b : β
H :
  Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr b))
⊢ Sum.Lex r₁ s (Sum.inl a) (Sum.inr b)
[PROOFSTEP]
cases H
[GOAL]
case mp.inr.inl
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a : β
b : α₁
H :
  Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr a))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl b))
⊢ Sum.Lex r₁ s (Sum.inr a) (Sum.inl b)
[PROOFSTEP]
cases H
[GOAL]
case mp.inr.inr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : β
H :
  Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr a))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr b))
⊢ Sum.Lex r₁ s (Sum.inr a) (Sum.inr b)
[PROOFSTEP]
cases H
[GOAL]
case mp.inl.inl.inl
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁
h✝ : r₂ (↑f a) (↑f b)
⊢ Sum.Lex r₁ s (Sum.inl a) (Sum.inl b)
[PROOFSTEP]
constructor
[GOAL]
case mp.inl.inr.sep
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a : α₁
b : β
⊢ Sum.Lex r₁ s (Sum.inl a) (Sum.inr b)
[PROOFSTEP]
constructor
[GOAL]
case mp.inr.inr.inr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : β
h✝ : s (↑(Embedding.refl β) a) (↑(Embedding.refl β) b)
⊢ Sum.Lex r₁ s (Sum.inr a) (Sum.inr b)
[PROOFSTEP]
constructor
[GOAL]
case mp.inl.inl.inl.h
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁
h✝ : r₂ (↑f a) (↑f b)
⊢ r₁ a b
[PROOFSTEP]
rwa [← fo]
[GOAL]
case mp.inr.inr.inr.h
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : β
h✝ : s (↑(Embedding.refl β) a) (↑(Embedding.refl β) b)
⊢ s a b
[PROOFSTEP]
assumption
[GOAL]
case mpr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
H : Sum.Lex r₁ s a b
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b)
[PROOFSTEP]
cases H <;> constructor <;> [rwa [fo]; assumption]
[GOAL]
case mpr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a✝ b✝ : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a b : α₁ ⊕ β
H : Sum.Lex r₁ s a b
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) a) (↑(Embedding.sumMap f (Embedding.refl β)) b)
[PROOFSTEP]
cases H
[GOAL]
case mpr.inl
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a₁✝ a₂✝ : α₁
h✝ : r₁ a₁✝ a₂✝
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a₁✝))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a₂✝))
[PROOFSTEP]
constructor
[GOAL]
case mpr.inr
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
b₁✝ b₂✝ : β
h✝ : s b₁✝ b₂✝
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr b₁✝))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr b₂✝))
[PROOFSTEP]
constructor
[GOAL]
case mpr.sep
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a✝ : α₁
b✝ : β
⊢ Sum.Lex r₂ s (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inl a✝))
    (↑(Embedding.sumMap f (Embedding.refl β)) (Sum.inr b✝))
[PROOFSTEP]
constructor
[GOAL]
case mpr.inl.h
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
a₁✝ a₂✝ : α₁
h✝ : r₁ a₁✝ a₂✝
⊢ r₂ (↑f a₁✝) (↑f a₂✝)
[PROOFSTEP]
rwa [fo]
[GOAL]
case mpr.inr.h
α : Type ?u.140748
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
α₁ : Type u
r₁ : α₁ → α₁ → Prop
x✝² : IsWellOrder α₁ r₁
α₂ : Type u
r₂ : α₂ → α₂ → Prop
x✝¹ : IsWellOrder α₂ r₂
c : Ordinal.{u}
f : α₁ ↪ α₂
fo : ∀ {a b : α₁}, r₂ (↑f a) (↑f b) ↔ r₁ a b
fi :
  ∀ (a : α₁) (b : α₂),
    r₂ b (↑{ toEmbedding := f, map_rel_iff' := fo } a) → ∃ a', ↑{ toEmbedding := f, map_rel_iff' := fo } a' = b
β : Type u
s : β → β → Prop
x✝ : IsWellOrder β s
b₁✝ b₂✝ : β
h✝ : s b₁✝ b₂✝
⊢ s (↑(Embedding.refl β) b₁✝) (↑(Embedding.refl β) b₂✝)
[PROOFSTEP]
assumption
[GOAL]
α : Type ?u.163180
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_3}
⊢ a ≤ a + b
[PROOFSTEP]
simpa only [add_zero] using add_le_add_left (Ordinal.zero_le b) a
[GOAL]
α : Type ?u.163578
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_3}
⊢ a ≤ b + a
[PROOFSTEP]
simpa only [zero_add] using add_le_add_right (Ordinal.zero_le b) a
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
h : b = a + b
x✝ : a < a + b ∨ a = a + b
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
h : b = a + b
x✝ : a < a + b ∨ a = a + b
⊢ a ≤ a + b ∨ a + b ≤ a
[PROOFSTEP]
exact Or.inl (le_add_right _ _)
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
x✝ : b < a + b ∨ b = a + b
h : a = a + b
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
x✝ : b < a + b ∨ b = a + b
h : a = a + b
⊢ a + b ≤ b ∨ b ≤ a + b
[PROOFSTEP]
exact Or.inr (le_add_left _ _)
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
h₁ : b < a + b
h₂ : a < a + b
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
revert h₁ h₂
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
⊢ b < a + b → a < a + b → a ≤ b ∨ b ≤ a
[PROOFSTEP]
refine inductionOn a ?_
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
⊢ ∀ (α : Type ?u.163980) (r : α → α → Prop) [inst : IsWellOrder α r],
    b < type r + b → type r < type r + b → type r ≤ b ∨ b ≤ type r
[PROOFSTEP]
intro α₁ r₁ _
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝ : IsWellOrder α₁ r₁
⊢ b < type r₁ + b → type r₁ < type r₁ + b → type r₁ ≤ b ∨ b ≤ type r₁
[PROOFSTEP]
refine inductionOn b ?_
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝ : IsWellOrder α₁ r₁
⊢ ∀ (α : Type ?u.163980) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r < type r₁ + type r → type r₁ < type r₁ + type r → type r₁ ≤ type r ∨ type r ≤ type r₁
[PROOFSTEP]
intro α₂ r₂ _ ⟨f⟩ ⟨g⟩
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
⊢ type r₁ ≤ type r₂ ∨ type r₂ ≤ type r₁
[PROOFSTEP]
rw [← typein_top f, ← typein_top g, le_iff_lt_or_eq, le_iff_lt_or_eq, typein_lt_typein, typein_lt_typein]
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
⊢ (Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top) ∨
    Sum.Lex r₁ r₂ f.top g.top ∨ typein (Sum.Lex r₁ r₂) f.top = typein (Sum.Lex r₁ r₂) g.top
[PROOFSTEP]
rcases trichotomous_of (Sum.Lex r₁ r₂) g.top f.top with (h | h | h) <;> [exact Or.inl (Or.inl h); (left; right; rw [h]);
  exact Or.inr (Or.inl h)]
[GOAL]
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
⊢ (Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top) ∨
    Sum.Lex r₁ r₂ f.top g.top ∨ typein (Sum.Lex r₁ r₂) f.top = typein (Sum.Lex r₁ r₂) g.top
[PROOFSTEP]
rcases trichotomous_of (Sum.Lex r₁ r₂) g.top f.top with (h | h | h)
[GOAL]
case inl
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
h : Sum.Lex r₁ r₂ g.top f.top
⊢ (Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top) ∨
    Sum.Lex r₁ r₂ f.top g.top ∨ typein (Sum.Lex r₁ r₂) f.top = typein (Sum.Lex r₁ r₂) g.top
[PROOFSTEP]
exact Or.inl (Or.inl h)
[GOAL]
case inr.inl
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
h : g.top = f.top
⊢ (Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top) ∨
    Sum.Lex r₁ r₂ f.top g.top ∨ typein (Sum.Lex r₁ r₂) f.top = typein (Sum.Lex r₁ r₂) g.top
[PROOFSTEP]
left
[GOAL]
case inr.inl.h
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
h : g.top = f.top
⊢ Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top
[PROOFSTEP]
right
[GOAL]
case inr.inl.h.h
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
h : g.top = f.top
⊢ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top
[PROOFSTEP]
rw [h]
[GOAL]
case inr.inr
α : Type ?u.163946
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
src✝ : PartialOrder Ordinal.{?u.163980} := inferInstanceAs (PartialOrder Ordinal.{?u.163980})
a b : Ordinal.{?u.163980}
α₁ : Type ?u.163980
r₁ : α₁ → α₁ → Prop
inst✝¹ : IsWellOrder α₁ r₁
α₂ : Type ?u.163980
r₂ : α₂ → α₂ → Prop
inst✝ : IsWellOrder α₂ r₂
f : r₂ ≺i Sum.Lex r₁ r₂
g : r₁ ≺i Sum.Lex r₁ r₂
h : Sum.Lex r₁ r₂ f.top g.top
⊢ (Sum.Lex r₁ r₂ g.top f.top ∨ typein (Sum.Lex r₁ r₂) g.top = typein (Sum.Lex r₁ r₂) f.top) ∨
    Sum.Lex r₁ r₂ f.top g.top ∨ typein (Sum.Lex r₁ r₂) f.top = typein (Sum.Lex r₁ r₂) g.top
[PROOFSTEP]
exact Or.inr (Or.inl h)
[GOAL]
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
⊢ type r + 1 ≤ type s
[PROOFSTEP]
haveI := hs
[GOAL]
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
⊢ type r + 1 ≤ type s
[PROOFSTEP]
refine' ⟨⟨RelEmbedding.ofMonotone (Sum.rec f fun _ => t) (fun a b ↦ _), fun a b ↦ _⟩⟩
[GOAL]
case refine'_1
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α ⊕ PUnit
⊢ Sum.Lex r EmptyRelation a b →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case refine'_1.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : α ⊕ PUnit
a : α
⊢ Sum.Lex r EmptyRelation (Sum.inl a) b →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case refine'_1.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : α ⊕ PUnit
val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝) b →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case refine'_1.inl.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a b : α
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))
[PROOFSTEP]
simpa only [Sum.lex_inl_inl] using f.map_rel_iff.2
[GOAL]
case refine'_1.inl.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
[PROOFSTEP]
intro
[GOAL]
case refine'_1.inl.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
[PROOFSTEP]
rw [hf]
[GOAL]
case refine'_1.inl.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝¹ b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α
val✝ : PUnit
a✝ : Sum.Lex r EmptyRelation (Sum.inl a) (Sum.inr val✝)
⊢ ∃ a_1, ↑f a_1 = (fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl a)
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case refine'_1.inr.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝ : PUnit
b : α
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝) (Sum.inl b) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inl b))
[PROOFSTEP]
exact False.elim ∘ Sum.lex_inr_inl
[GOAL]
case refine'_1.inr.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
val✝¹ val✝ : PUnit
⊢ Sum.Lex r EmptyRelation (Sum.inr val✝¹) (Sum.inr val✝) →
    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝¹))
      ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) (Sum.inr val✝))
[PROOFSTEP]
exact False.elim ∘ Sum.lex_inr_inr.1
[GOAL]
case refine'_2
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
a : α ⊕ PUnit
b : β
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case refine'_2.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inl a)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
[PROOFSTEP]
intro h
[GOAL]
case refine'_2.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
[PROOFSTEP]
have := @PrincipalSeg.init _ _ _ _ _ ⟨f, t, hf⟩ _ _ h
[GOAL]
case refine'_2.inl
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this✝ : IsWellOrder β s
b : β
a : α
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
this : ∃ a', ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding a' = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
[PROOFSTEP]
cases' this with w h
[GOAL]
case refine'_2.inl.intro
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a✝ b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
a : α
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inl a))
w : α
h : ↑{ toRelEmbedding := f, top := t, down' := hf }.toRelEmbedding w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
[PROOFSTEP]
exact ⟨Sum.inl w, h⟩
[GOAL]
case refine'_2.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
⊢ s b
      (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        (Sum.inr val✝)) →
    ∃ a',
      ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
              (_ :
                ∀ (a b : α ⊕ PUnit),
                  Sum.Lex r EmptyRelation a b →
                    s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
          a' =
        b
[PROOFSTEP]
intro h
[GOAL]
case refine'_2.inr
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
[PROOFSTEP]
cases' (hf b).1 h with w h
[GOAL]
case refine'_2.inr.intro
α✝ : Type ?u.169275
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ → γ → Prop
a b✝ : Ordinal.{u_3}
α : Type u_3
r : α → α → Prop
hr : IsWellOrder α r
β : Type u_3
s : β → β → Prop
hs : IsWellOrder β s
x✝ : type r < type s
f : r ↪r s
t : β
hf : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b
this : IsWellOrder β s
b : β
val✝ : PUnit
h✝ :
  s b
    (↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
          (_ :
            ∀ (a b : α ⊕ PUnit),
              Sum.Lex r EmptyRelation a b →
                s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
      (Sum.inr val✝))
w : α
h : ↑f w = b
⊢ ∃ a',
    ↑(RelEmbedding.ofMonotone (fun t_1 => Sum.rec (↑f) (fun x => t) t_1)
            (_ :
              ∀ (a b : α ⊕ PUnit),
                Sum.Lex r EmptyRelation a b →
                  s ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) a) ((fun t_1 => Sum.rec (↑f) (fun x => t) t_1) b)))
        a' =
      b
[PROOFSTEP]
exact ⟨Sum.inl w, h⟩
[GOAL]
α : Type ?u.179391
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ succ 1 = 2
[PROOFSTEP]
unfold instOfNat OfNat.ofNat
[GOAL]
α : Type ?u.179391
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ succ One.toOfNat1.1 = { ofNat := ↑2 }.1
[PROOFSTEP]
simpa using by rfl
[GOAL]
α : Type ?u.179391
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ One.toOfNat1.1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.180733
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ 1 ≤ o ↔ 0 < o
[PROOFSTEP]
rw [← succ_zero, succ_le_iff]
[GOAL]
α : Type ?u.181133
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ 1 ≤ o ↔ o ≠ 0
[PROOFSTEP]
rw [one_le_iff_pos, Ordinal.pos_iff_ne_zero]
[GOAL]
α : Type ?u.181722
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u_3}
⊢ a < 1 ↔ a = 0
[PROOFSTEP]
simpa using @lt_succ_bot_iff _ _ _ a _ _
[GOAL]
α : Type ?u.182584
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u_3}
⊢ a ≤ 1 ↔ a = 0 ∨ a = 1
[PROOFSTEP]
simpa using @le_succ_bot_iff _ _ _ a _
[GOAL]
α : Type ?u.183756
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ card (succ o) = card o + 1
[PROOFSTEP]
simp only [← add_one_eq_succ, card_add, card_one]
[GOAL]
α : Type ?u.184700
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 0 ∈ Iio 1
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 0 < type fun x x_1 => x < x_1
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : (Quotient.out 1).α
⊢ a = default
[PROOFSTEP]
unfold default
[GOAL]
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : (Quotient.out 1).α
⊢ a = { default := enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1) }.1
[PROOFSTEP]
rw [← @enum_typein _ (· < ·) (isWellOrder_out_lt _) a]
[GOAL]
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : (Quotient.out 1).α
⊢ enum (fun x x_1 => x < x_1) (typein (fun x x_1 => x < x_1) a)
      (_ : typein (fun x x_1 => x < x_1) a < type fun x x_1 => x < x_1) =
    { default := enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1) }.1
[PROOFSTEP]
congr
[GOAL]
case e_o
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : (Quotient.out 1).α
⊢ typein (fun x x_1 => x < x_1) a = 0
[PROOFSTEP]
rw [← lt_one_iff_zero]
[GOAL]
case e_o
α : Type ?u.185352
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : (Quotient.out 1).α
⊢ typein (fun x x_1 => x < x_1) a < 1
[PROOFSTEP]
apply typein_lt_self
[GOAL]
α : Type ?u.187460
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : (Quotient.out 1).α
⊢ 0 < type fun x x_1 => x < x_1
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.188563
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : (Quotient.out 1).α
⊢ typein (fun x x_1 => x < x_1) x = 0
[PROOFSTEP]
rw [one_out_eq x, typein_enum]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x x' : α
⊢ typein r x ≤ typein r x' ↔ ¬r x' x
[PROOFSTEP]
rw [← not_lt, typein_lt_typein]
[GOAL]
α : Type ?u.190090
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
x x' : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) x ≤ typein (fun x x_1 => x < x_1) x' ↔ x ≤ x'
[PROOFSTEP]
rw [typein_le_typein]
[GOAL]
α : Type ?u.190090
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
x x' : (Quotient.out o).α
⊢ ¬x' < x ↔ x ≤ x'
[PROOFSTEP]
exact not_lt
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o o' : Ordinal.{u_3}
ho : o < type r
ho' : o' < type r
⊢ ¬r (enum r o' ho') (enum r o ho) ↔ o ≤ o'
[PROOFSTEP]
rw [← @not_lt _ _ o' o, enum_lt_enum ho']
[GOAL]
α : Type ?u.192624
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a o o' : Ordinal.{u_3}
ho : o < type fun x x_1 => x < x_1
ho' : o' < type fun x x_1 => x < x_1
⊢ enum (fun x x_1 => x < x_1) o ho ≤ enum (fun x x_1 => x < x_1) o' ho' ↔ o ≤ o'
[PROOFSTEP]
rw [← @enum_le_enum _ (· < ·) (isWellOrder_out_lt _), ← not_lt]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r a (enum r 0 h0)
[PROOFSTEP]
rw [← enum_typein r a, enum_le_enum r]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ 0 ≤ typein r a
[PROOFSTEP]
apply Ordinal.zero_le
[GOAL]
α : Type ?u.196508
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.196642}
h0 : 0 < o
a : (Quotient.out o).α
⊢ 0 < type fun x x_1 => x < x_1
[PROOFSTEP]
rwa [type_lt]
[GOAL]
α : Type ?u.196508
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
h0 : 0 < o
a : (Quotient.out o).α
⊢ enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1) ≤ a
[PROOFSTEP]
rw [← not_lt]
[GOAL]
α : Type ?u.196508
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
h0 : 0 < o
a : (Quotient.out o).α
⊢ ¬a < enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1)
[PROOFSTEP]
apply enum_zero_le
[GOAL]
α : Type ?u.197714
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.197839}
a : (Quotient.out (succ o)).α
⊢ o < type fun x x_1 => x < x_1
[PROOFSTEP]
rw [type_lt]
[GOAL]
α : Type ?u.197714
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.197839}
a : (Quotient.out (succ o)).α
⊢ o < succ o
[PROOFSTEP]
exact lt_succ o
[GOAL]
α : Type ?u.197714
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
a : (Quotient.out (succ o)).α
⊢ a ≤ enum (fun x x_1 => x < x_1) o (_ : o < type fun x x_1 => x < x_1)
[PROOFSTEP]
rw [← @enum_typein _ (· < ·) (isWellOrder_out_lt _) a, enum_le_enum', ← lt_succ_iff]
[GOAL]
α : Type ?u.197714
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
a : (Quotient.out (succ o)).α
⊢ typein (fun x x_1 => x < x_1) a < succ o
[PROOFSTEP]
apply typein_lt_self
[GOAL]
α : Type ?u.201785
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.203623}
x : ↑(Iio o)
⊢ ↑x < type fun x x_1 => x < x_1
[PROOFSTEP]
rw [type_lt]
[GOAL]
α : Type ?u.201785
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.203623}
x : ↑(Iio o)
⊢ ↑x < o
[PROOFSTEP]
exact x.2
[GOAL]
α : Type ?u.201785
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.203623}
⊢ ∀ {a b : ↑(Iio o)},
    ↑{ toFun := fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1),
              invFun := fun x =>
                { val := typein (fun x x_1 => x < x_1) x, property := (_ : typein (fun x x_1 => x < x_1) x < o) },
              left_inv :=
                (_ :
                  ∀ (x : ↑(Iio o)),
                    (fun x =>
                          { val := typein (fun x x_1 => x < x_1) x,
                            property := (_ : typein (fun x x_1 => x < x_1) x < o) })
                        ((fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1)) x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (h : (Quotient.out o).α),
                    enum (fun x x_1 => x < x_1) (typein (fun x x_1 => x < x_1) h)
                        (_ : typein (fun x x_1 => x < x_1) h < type fun x x_1 => x < x_1) =
                      h) }
          a ≤
        ↑{ toFun := fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1),
              invFun := fun x =>
                { val := typein (fun x x_1 => x < x_1) x, property := (_ : typein (fun x x_1 => x < x_1) x < o) },
              left_inv :=
                (_ :
                  ∀ (x : ↑(Iio o)),
                    (fun x =>
                          { val := typein (fun x x_1 => x < x_1) x,
                            property := (_ : typein (fun x x_1 => x < x_1) x < o) })
                        ((fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1)) x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (h : (Quotient.out o).α),
                    enum (fun x x_1 => x < x_1) (typein (fun x x_1 => x < x_1) h)
                        (_ : typein (fun x x_1 => x < x_1) h < type fun x x_1 => x < x_1) =
                      h) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro ⟨a, _⟩ ⟨b, _⟩
[GOAL]
case mk.mk
α : Type ?u.201785
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o a : Ordinal.{?u.203623}
property✝¹ : a ∈ Iio o
b : Ordinal.{?u.203623}
property✝ : b ∈ Iio o
⊢ ↑{ toFun := fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1),
            invFun := fun x =>
              { val := typein (fun x x_1 => x < x_1) x, property := (_ : typein (fun x x_1 => x < x_1) x < o) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Iio o)),
                  (fun x =>
                        { val := typein (fun x x_1 => x < x_1) x,
                          property := (_ : typein (fun x x_1 => x < x_1) x < o) })
                      ((fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (h : (Quotient.out o).α),
                  enum (fun x x_1 => x < x_1) (typein (fun x x_1 => x < x_1) h)
                      (_ : typein (fun x x_1 => x < x_1) h < type fun x x_1 => x < x_1) =
                    h) }
        { val := a, property := property✝¹ } ≤
      ↑{ toFun := fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1),
            invFun := fun x =>
              { val := typein (fun x x_1 => x < x_1) x, property := (_ : typein (fun x x_1 => x < x_1) x < o) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Iio o)),
                  (fun x =>
                        { val := typein (fun x x_1 => x < x_1) x,
                          property := (_ : typein (fun x x_1 => x < x_1) x < o) })
                      ((fun x => enum (fun x x_1 => x < x_1) ↑x (_ : ↑x < type fun x x_1 => x < x_1)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (h : (Quotient.out o).α),
                  enum (fun x x_1 => x < x_1) (typein (fun x x_1 => x < x_1) h)
                      (_ : typein (fun x x_1 => x < x_1) h < type fun x x_1 => x < x_1) =
                    h) }
        { val := b, property := property✝ } ↔
    { val := a, property := property✝¹ } ≤ { val := b, property := property✝ }
[PROOFSTEP]
apply enum_le_enum'
[GOAL]
α : Type ?u.208873
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.208900}
ho : 0 < o
⊢ 0 < type fun x x_1 => x < x_1
[PROOFSTEP]
rwa [type_lt]
[GOAL]
α : Type ?u.211339
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (b : Ordinal.{max (u + 1) v}), b < univ ↔ ∃ a, ↑initialSeg.toRelEmbedding a = b
[PROOFSTEP]
refine' fun b => inductionOn b _
[GOAL]
α : Type ?u.211339
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r < univ ↔ ∃ a, ↑initialSeg.toRelEmbedding a = type r
[PROOFSTEP]
intro β s _
[GOAL]
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < univ ↔ ∃ a, ↑initialSeg.toRelEmbedding a = type s
[PROOFSTEP]
rw [univ, ← lift_umax]
[GOAL]
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift (type fun x x_1 => x < x_1) ↔ ∃ a, ↑initialSeg.toRelEmbedding a = type s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift (type fun x x_1 => x < x_1) → ∃ a, ↑initialSeg.toRelEmbedding a = type s
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ (∃ a, ↑initialSeg.toRelEmbedding a = type s) → type s < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift (type fun x x_1 => x < x_1)
⊢ ∃ a, ↑initialSeg.toRelEmbedding a = type s
[PROOFSTEP]
rw [← lift_id (type s)] at h ⊢
[GOAL]
case mp
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
⊢ ∃ a, ↑initialSeg.toRelEmbedding a = lift (type s)
[PROOFSTEP]
cases' lift_type_lt.{_, _, v}.1 h with f
[GOAL]
case mp.intro
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ≺i fun x x_1 => x < x_1
⊢ ∃ a, ↑initialSeg.toRelEmbedding a = lift (type s)
[PROOFSTEP]
cases' f with f a hf
[GOAL]
case mp.intro.mk
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b < a ↔ ∃ a, ↑f a = b
⊢ ∃ a, ↑initialSeg.toRelEmbedding a = lift (type s)
[PROOFSTEP]
exists a
[GOAL]
case mp.intro.mk
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b < a ↔ ∃ a, ↑f a = b
⊢ ↑initialSeg.toRelEmbedding a = lift (type s)
[PROOFSTEP]
revert hf
[GOAL]
case mp.intro.mk
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
⊢ (∀ (b : Ordinal.{u}), b < a ↔ ∃ a, ↑f a = b) → ↑initialSeg.toRelEmbedding a = lift (type s)
[PROOFSTEP]
refine inductionOn a ?_
[GOAL]
case mp.intro.mk
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
⊢ ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α r],
    (∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b) → ↑initialSeg.toRelEmbedding (type r) = lift (type s)
[PROOFSTEP]
intro α r _ hf
[GOAL]
case mp.intro.mk
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
⊢ ↑initialSeg.toRelEmbedding (type r) = lift (type s)
[PROOFSTEP]
refine' lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2 ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone _ _) _).symm⟩
[GOAL]
case mp.intro.mk.refine'_1
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
⊢ β → α
[PROOFSTEP]
exact fun b => enum r (f b) ((hf _).2 ⟨_, rfl⟩)
[GOAL]
case mp.intro.mk.refine'_2
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
⊢ ∀ (a b : β), s a b → r (enum r (↑f a) (_ : ↑f a < type r)) (enum r (↑f b) (_ : ↑f b < type r))
[PROOFSTEP]
refine' fun a b h => (typein_lt_typein r).1 _
[GOAL]
case mp.intro.mk.refine'_2
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h✝ : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a✝ : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a b : β
h : s a b
⊢ typein r (enum r (↑f a) (_ : ↑f a < type r)) < typein r (enum r (↑f b) (_ : ↑f b < type r))
[PROOFSTEP]
rw [typein_enum, typein_enum]
[GOAL]
case mp.intro.mk.refine'_2
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h✝ : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a✝ : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a b : β
h : s a b
⊢ ↑f a < ↑f b
[PROOFSTEP]
exact f.map_rel_iff.2 h
[GOAL]
case mp.intro.mk.refine'_3
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
⊢ Surjective
    ↑(RelEmbedding.ofMonotone (fun b => enum r (↑f b) (_ : ↑f b < type r))
        (_ : ∀ (a b : β), s a b → r (enum r (↑f a) (_ : ↑f a < type r)) (enum r (↑f b) (_ : ↑f b < type r))))
[PROOFSTEP]
intro a'
[GOAL]
case mp.intro.mk.refine'_3
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a' : α
⊢ ∃ a,
    ↑(RelEmbedding.ofMonotone (fun b => enum r (↑f b) (_ : ↑f b < type r))
            (_ : ∀ (a b : β), s a b → r (enum r (↑f a) (_ : ↑f a < type r)) (enum r (↑f b) (_ : ↑f b < type r))))
        a =
      a'
[PROOFSTEP]
cases' (hf _).1 (typein_lt_type _ a') with b e
[GOAL]
case mp.intro.mk.refine'_3.intro
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a' : α
b : β
e : ↑f b = typein r a'
⊢ ∃ a,
    ↑(RelEmbedding.ofMonotone (fun b => enum r (↑f b) (_ : ↑f b < type r))
            (_ : ∀ (a b : β), s a b → r (enum r (↑f a) (_ : ↑f a < type r)) (enum r (↑f b) (_ : ↑f b < type r))))
        a =
      a'
[PROOFSTEP]
exists b
[GOAL]
case mp.intro.mk.refine'_3.intro
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a' : α
b : β
e : ↑f b = typein r a'
⊢ ↑(RelEmbedding.ofMonotone (fun b => enum r (↑f b) (_ : ↑f b < type r))
          (_ : ∀ (a b : β), s a b → r (enum r (↑f a) (_ : ↑f a < type r)) (enum r (↑f b) (_ : ↑f b < type r))))
      b =
    a'
[PROOFSTEP]
simp
[GOAL]
case mp.intro.mk.refine'_3.intro
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift (type s) < lift (type fun x x_1 => x < x_1)
f : s ↪r fun x x_1 => x < x_1
a : Ordinal.{u}
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b < type r ↔ ∃ a, ↑f a = b
a' : α
b : β
e : ↑f b = typein r a'
⊢ enum r (↑f b) (_ : ↑f b < type r) = a'
[PROOFSTEP]
simp [e]
[GOAL]
case mpr
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : ∃ a, ↑initialSeg.toRelEmbedding a = type s
⊢ type s < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
cases' h with a e
[GOAL]
case mpr.intro
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : ↑initialSeg.toRelEmbedding a = type s
⊢ type s < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
rw [← e]
[GOAL]
case mpr.intro
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : ↑initialSeg.toRelEmbedding a = type s
⊢ ↑initialSeg.toRelEmbedding a < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
refine inductionOn a ?_
[GOAL]
case mpr.intro
α : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : ↑initialSeg.toRelEmbedding a = type s
⊢ ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α r],
    ↑initialSeg.toRelEmbedding (type r) < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
intro α r _
[GOAL]
case mpr.intro
α✝ : Type ?u.211339
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
a : Ordinal.{u}
e : ↑initialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ ↑initialSeg.toRelEmbedding (type r) < lift (type fun x x_1 => x < x_1)
[PROOFSTEP]
exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein.principalSeg r⟩
[GOAL]
α : Type ?u.221999
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ principalSeg.top = type fun x x_1 => x < x_1
[PROOFSTEP]
simp only [lift.principalSeg_top, univ_id]
[GOAL]
α : Type ?u.222301
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
⊢ card (type (?m.222405 o)) = card o
[PROOFSTEP]
rw [Ordinal.type_lt]
[GOAL]
α : Type ?u.222528
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
⊢ ∀ (a b : Type u), Setoid.r a b → F a = F b
[PROOFSTEP]
suffices : ∀ {α β}, α ≈ β → F α ≤ F β
[GOAL]
α : Type ?u.222528
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
this : ∀ {α β : Type u}, α ≈ β → F α ≤ F β
⊢ ∀ (a b : Type u), Setoid.r a b → F a = F b
case this
α : Type ?u.222528
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
⊢ ∀ {α β : Type u}, α ≈ β → F α ≤ F β
[PROOFSTEP]
exact fun α β h => (this h).antisymm (this (Setoid.symm h))
[GOAL]
case this
α : Type ?u.222528
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
⊢ ∀ {α β : Type u}, α ≈ β → F α ≤ F β
[PROOFSTEP]
rintro α β ⟨f⟩
[GOAL]
case this.intro
α✝ : Type ?u.222528
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
α β : Type u
f : α ≃ β
⊢ F α ≤ F β
[PROOFSTEP]
refine' le_ciInf_iff'.2 fun i => _
[GOAL]
case this.intro
α✝ : Type ?u.222528
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
α β : Type u
f : α ≃ β
i : { r // IsWellOrder β r }
⊢ F α ≤ type ↑i
[PROOFSTEP]
haveI := @RelEmbedding.isWellOrder _ _ (f ⁻¹'o i.1) _ (↑(RelIso.preimage f i.1)) i.2
[GOAL]
case this.intro
α✝ : Type ?u.222528
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
F : Type u → Ordinal.{u} := fun α => ⨅ (r : { r // IsWellOrder α r }), type ↑r
α β : Type u
f : α ≃ β
i : { r // IsWellOrder β r }
this : IsWellOrder α (↑f ⁻¹'o ↑i)
⊢ F α ≤ type ↑i
[PROOFSTEP]
exact
  (ciInf_le' _ (Subtype.mk (f ⁻¹'o i.val) (@RelEmbedding.isWellOrder _ _ _ _ (↑(RelIso.preimage f i.1)) i.2))).trans_eq
    (Quot.sound ⟨RelIso.preimage f i.1⟩)
[GOAL]
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ ord #α ≤ type s ↔ #α ≤ card (type s)
[PROOFSTEP]
let ⟨r, _, e⟩ := ord_eq α
[GOAL]
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ ord #α ≤ type s ↔ #α ≤ card (type s)
[PROOFSTEP]
skip
[GOAL]
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ ord #α ≤ type s ↔ #α ≤ card (type s)
[PROOFSTEP]
simp only [card_type]
[GOAL]
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ ord #α ≤ type s ↔ #α ≤ #β
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ ord #α ≤ type s → #α ≤ #β
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ #α ≤ #β → ord #α ≤ type s
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
h : ord #α ≤ type s
⊢ #α ≤ #β
[PROOFSTEP]
rw [e] at h 
[GOAL]
case mp
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
h : type r ≤ type s
⊢ #α ≤ #β
[PROOFSTEP]
exact
  let ⟨f⟩ := h
  ⟨f.toEmbedding⟩
[GOAL]
case mpr
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
h : #α ≤ #β
⊢ ord #α ≤ type s
[PROOFSTEP]
cases' h with f
[GOAL]
case mpr.intro
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
f : α ↪ β
⊢ ord #α ≤ type s
[PROOFSTEP]
have g := RelEmbedding.preimage f s
[GOAL]
case mpr.intro
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
⊢ ord #α ≤ type s
[PROOFSTEP]
haveI := RelEmbedding.isWellOrder g
[GOAL]
case mpr.intro
α✝ : Type ?u.225629
β✝ : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
o : Ordinal.{u_3}
α β : Type u_3
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
f : α ↪ β
g : ↑f ⁻¹'o s ↪r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ord #α ≤ type s
[PROOFSTEP]
exact le_trans (ord_le_type _) g.ordinal_type_le
[GOAL]
α✝ : Type ?u.226993
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
α : Type u_3
⊢ card (ord (Quotient.mk isEquivalent α)) = Quotient.mk isEquivalent α
[PROOFSTEP]
let ⟨r, _, e⟩ := ord_eq α
[GOAL]
α✝ : Type ?u.226993
β : Type u_1
γ : Type u_2
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
α : Type u_3
r : α → α → Prop
w✝ : IsWellOrder α r
e : ord #α = type r
⊢ card (ord (Quotient.mk isEquivalent α)) = Quotient.mk isEquivalent α
[PROOFSTEP]
simp only [mk'_def, e, card_type]
[GOAL]
α : Type ?u.229821
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
⊢ ↑n ≤ ord ↑n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type ?u.229821
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ↑Nat.zero ≤ ord ↑Nat.zero
[PROOFSTEP]
apply Ordinal.zero_le
[GOAL]
case succ
α : Type ?u.229821
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
IH : ↑n ≤ ord ↑n
⊢ ↑(Nat.succ n) ≤ ord ↑(Nat.succ n)
[PROOFSTEP]
exact succ_le_of_lt (IH.trans_lt <| ord_lt_ord.2 <| natCast_lt.2 (Nat.lt_succ_self n))
[GOAL]
α : Type ?u.230856
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ord 1 = 1
[PROOFSTEP]
simpa using ord_nat 1
[GOAL]
α : Type ?u.231632
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{v}
⊢ Ordinal.lift (ord c) = ord (lift c)
[PROOFSTEP]
refine' le_antisymm (le_of_forall_lt fun a ha => _) _
[GOAL]
case refine'_1
α : Type ?u.231632
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift (ord c)
⊢ a < ord (lift c)
[PROOFSTEP]
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, rfl, _⟩
[GOAL]
case refine'_1.intro.intro
α : Type ?u.231632
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{v}
a : Ordinal.{v}
right✝ : a < ord c
ha : Ordinal.lift a < Ordinal.lift (ord c)
⊢ Ordinal.lift a < ord (lift c)
[PROOFSTEP]
rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
[GOAL]
case refine'_2
α : Type ?u.231632
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{v}
⊢ ord (lift c) ≤ Ordinal.lift (ord c)
[PROOFSTEP]
rw [ord_le, ← lift_card, card_ord]
[GOAL]
α : Type ?u.232210
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
⊢ #(Quotient.out (ord c)).α = c
[PROOFSTEP]
simp
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : ord #α = type r
⊢ card (typein r x) < #α
[PROOFSTEP]
rw [← lt_ord, h]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : ord #α = type r
⊢ typein r x < type r
[PROOFSTEP]
apply typein_lt_type
[GOAL]
α : Type ?u.232559
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
x : (Quotient.out (ord c)).α
⊢ card (typein (fun x x_1 => x < x_1) x) < c
[PROOFSTEP]
rw [← lt_ord]
[GOAL]
α : Type ?u.232559
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u_3}
x : (Quotient.out (ord c)).α
⊢ typein (fun x x_1 => x < x_1) x < ord c
[PROOFSTEP]
apply typein_lt_self
[GOAL]
α : Type ?u.233731
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective ord
[PROOFSTEP]
intro c c' h
[GOAL]
α : Type ?u.233731
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c c' : Cardinal.{u_3}
h : ord c = ord c'
⊢ c = c'
[PROOFSTEP]
rw [← card_ord c, ← card_ord c', h]
[GOAL]
α : Type ?u.236029
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
⊢ lift c < univ
[PROOFSTEP]
simpa only [lift.principalSeg_coe, lift_ord, lift_succ, ord_le, succ_le_iff] using
  le_of_lt (lift.principalSeg.{u, u + 1}.lt_top (succ c).ord)
[GOAL]
α : Type ?u.236679
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
⊢ lift c < univ
[PROOFSTEP]
have := lift_lt.{_, max (u + 1) v}.2 (lift_lt_univ c)
[GOAL]
α : Type ?u.236679
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
this : lift (lift c) < lift univ
⊢ lift c < univ
[PROOFSTEP]
rw [lift_lift, lift_univ, univ_umax.{u, v}] at this 
[GOAL]
α : Type ?u.236679
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
this : lift c < univ
⊢ lift c < univ
[PROOFSTEP]
exact this
[GOAL]
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ord univ = Ordinal.univ
[PROOFSTEP]
refine' le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_
[GOAL]
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ
⊢ card o < univ
[PROOFSTEP]
have := lift.principalSeg.{u, v}.down.1 (by simpa only [lift.principalSeg_coe] using h)
[GOAL]
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ
⊢ ?m.237120 < lift.principalSeg.top
[PROOFSTEP]
simpa only [lift.principalSeg_coe] using h
[GOAL]
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ
this : ∃ a, ↑lift.principalSeg.toRelEmbedding a = o
⊢ card o < univ
[PROOFSTEP]
rcases this with ⟨o, h'⟩
[GOAL]
case intro
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ
o : Ordinal.{u}
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ card o✝ < univ
[PROOFSTEP]
rw [← h', lift.principalSeg_coe, ← lift_card]
[GOAL]
case intro
α : Type ?u.236823
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ
o : Ordinal.{u}
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ lift (card o) < univ
[PROOFSTEP]
apply lift_lt_univ'
[GOAL]
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
have := ord_lt_ord.2 h
[GOAL]
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this : ord c < ord univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
rw [ord_univ] at this 
[GOAL]
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this : ord c < Ordinal.univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
cases' lift.principalSeg.{u, u + 1}.down.1 (by simpa only [lift.principalSeg_top]) with o e
[GOAL]
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this : ord c < Ordinal.univ
⊢ ?m.237589 < lift.principalSeg.top
[PROOFSTEP]
simpa only [lift.principalSeg_top]
[GOAL]
case intro
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this : ord c < Ordinal.univ
o : Ordinal.{u}
e : ↑lift.principalSeg.toRelEmbedding o = ord c
⊢ ∃ c', c = lift c'
[PROOFSTEP]
have := card_ord c
[GOAL]
case intro
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal.{u}
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : card (ord c) = c
⊢ ∃ c', c = lift c'
[PROOFSTEP]
rw [← e, lift.principalSeg_coe, ← lift_card] at this 
[GOAL]
case intro
α : Type ?u.237323
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u + 1}
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal.{u}
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : lift (card o) = c
⊢ ∃ c', c = lift c'
[PROOFSTEP]
exact ⟨_, this.symm⟩
[GOAL]
α : Type ?u.237859
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{max (u + 1) v}
h : c < univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
let ⟨a, e, h'⟩ := lt_lift_iff.1 h
[GOAL]
α : Type ?u.237859
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{max (u + 1) v}
h : c < univ
a : Cardinal.{u + 1}
e : lift a = c
h' : a < #Ordinal.{u}
⊢ ∃ c', c = lift c'
[PROOFSTEP]
rw [← univ_id] at h' 
[GOAL]
α : Type ?u.237859
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{max (u + 1) v}
h : c < univ
a : Cardinal.{u + 1}
e : lift a = c
h' : a < univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
[GOAL]
case intro
α : Type ?u.237859
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{max (u + 1) v}
h : c < univ
c' : Cardinal.{u}
e : lift (lift c') = c
h' : lift c' < univ
⊢ ∃ c', c = lift c'
[PROOFSTEP]
exact ⟨c', by simp only [e.symm, lift_lift]⟩
[GOAL]
α : Type ?u.237859
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{max (u + 1) v}
h : c < univ
c' : Cardinal.{u}
e : lift (lift c') = c
h' : lift c' < univ
⊢ c = lift c'
[PROOFSTEP]
simp only [e.symm, lift_lift]
[GOAL]
α✝ : Type ?u.238384
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small.{v, u} α ↔ lift #α < univ
[PROOFSTEP]
rw [lt_univ']
[GOAL]
α✝ : Type ?u.238384
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift #α = lift c'
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type ?u.238384
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small.{v, u} α → ∃ c', lift #α = lift c'
[PROOFSTEP]
rintro ⟨β, e⟩
[GOAL]
case mp.mk.intro
α✝ : Type ?u.238384
β✝ : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift #α = lift c'
[PROOFSTEP]
exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩
[GOAL]
case mpr
α✝ : Type ?u.238384
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ (∃ c', lift #α = lift c') → Small.{v, u} α
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case mpr.intro
α✝ : Type ?u.238384
β : Type u_1
γ : Type u_2
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
c : Cardinal.{v}
hc : lift #α = lift c
⊢ Small.{v, u} α
[PROOFSTEP]
exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩
[GOAL]
α : Type ?u.238720
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
n : ℕ
⊢ ↑n ≤ card o ↔ ↑n ≤ o
[PROOFSTEP]
rw [← Cardinal.ord_le, Cardinal.ord_nat]
[GOAL]
α : Type ?u.239208
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
n : ℕ
⊢ ↑n < card o ↔ ↑n < o
[PROOFSTEP]
rw [← succ_le_iff, ← succ_le_iff, ← nat_succ, nat_le_card]
[GOAL]
α : Type ?u.239208
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
n : ℕ
⊢ ↑(Nat.succ n) ≤ o ↔ succ ↑n ≤ o
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.241773
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_3}
n : ℕ
⊢ card o = ↑n ↔ o = ↑n
[PROOFSTEP]
simp only [le_antisymm_iff, card_le_nat, nat_le_card]
[GOAL]
α : Type u_3
β : Type u_1
γ : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)
[PROOFSTEP]
rw [← card_eq_nat, card_type, mk_fintype]
[GOAL]
α : Type ?u.243192
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
⊢ (type fun x x_1 => x < x_1) = ↑n
[PROOFSTEP]
simp
