c : Cardinal
h : ℵ₀ ≤ c
⊢ c * c ≤ c
c : Cardinal
h : ℵ₀ ≤ c
⊢ c * c = c
refine' le_antisymm _ (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c)
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
c : Cardinal
h : ℵ₀ ≤ c
⊢ c * c ≤ c
refine' Acc.recOn (Cardinal.lt_wf.apply c) (fun c _ => Quotient.inductionOn c fun α IH ol => _) h
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
rcases ord_eq α with ⟨r, wo, e⟩
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
skip
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
letI := linearOrderOfSTO r
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝ : LinearOrder α := linearOrderOfSTO r
this : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝ : LinearOrder α := linearOrderOfSTO r
this : IsWellOrder α fun x x_1 => x < x_1
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
let g : α × α → α := fun p => max p.1 p.2
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝ : LinearOrder α := linearOrderOfSTO r
this : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
haveI : IsWellOrder _ s := (RelEmbedding.preimage _ _).isWellOrder
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
⊢ type s ≤ type r
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
suffices type s ≤ type r by exact card_le_card this
case intro.intro
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
o : Ordinal
h : o < type s
⊢ o < type r
case intro.intro
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
⊢ type s ≤ type r
refine' le_of_forall_lt fun o h => _
case intro.intro.intro
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
⊢ typein s p < type r
case intro.intro
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
o : Ordinal
h : o < type s
⊢ o < type r
rcases typein_surj s h with ⟨p, rfl⟩
case intro.intro.intro
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
⊢ card (typein s p) < (#α)
case intro.intro.intro
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
⊢ typein s p < type r
rw [← e, lt_ord]
no goals
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ≤ c * c
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c
no goals
c✝ : Cardinal
h : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
this : type s ≤ type r
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
exact card_le_card this
case intro.intro.intro.refine'_1
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ card (typein s p) ≤
    card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p)))
case intro.intro.intro.refine'_1
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
⊢ card (typein s p) ≤
    card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p)))
have : { q | s q p } ⊆ insert (g p) { x | x < g p } ×ˢ insert (g p) { x | x < g p } := by
  intro q h
  simp only [Preimage, ge_iff_le, Embedding.coeFn_mk, Prod.lex_def, typein_lt_typein,
    typein_inj, mem_setOf_eq] at h
  exact max_le_iff.1 (le_iff_lt_or_eq.2 <| h.imp_right And.left)
case intro.intro.intro.refine'_1
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
H : ↑(insert (g p) {x | r x (g p)}) ≃ ↑{x | r x (g p)} ⊕ PUnit
⊢ card (typein s p) ≤
    card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p)))

case H
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ ↑(insert (g p) {x | r x (g p)}) ≃ ↑{x | r x (g p)} ⊕ PUnit
case intro.intro.intro.refine'_1
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ card (typein s p) ≤
    card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p)))
suffices H : (insert (g p) { x | r x (g p) } : Set α) ≃ Sum { x | r x (g p) } PUnit
case H
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ ¬g p ∈ {x | r x (g p)}
case H
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ ↑(insert (g p) {x | r x (g p)}) ≃ ↑{x | r x (g p)} ⊕ PUnit
refine' (Equiv.Set.insert _).trans ((Equiv.refl _).sumCongr punitEquivPUnit)
no goals
case H
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
⊢ ¬g p ∈ {x | r x (g p)}
apply @irrefl _ r
c✝ : Cardinal
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h✝ : typein s p < type s
q : α × α
h : q ∈ {q | s q p}
⊢ q ∈ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
⊢ {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
intro q h
c✝ : Cardinal
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h✝ : typein s p < type s
q : α × α
h :
  max q.fst q.snd < max p.fst p.snd ∨
    max q.fst q.snd = max p.fst p.snd ∧ (q.fst < p.fst ∨ q.fst = p.fst ∧ q.snd < p.snd)
⊢ q ∈ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
c✝ : Cardinal
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h✝ : typein s p < type s
q : α × α
h : q ∈ {q | s q p}
⊢ q ∈ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
simp only [Preimage, ge_iff_le, Embedding.coeFn_mk, Prod.lex_def, typein_lt_typein,
  typein_inj, mem_setOf_eq] at h
no goals
c✝ : Cardinal
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h✝ : typein s p < type s
q : α × α
h :
  max q.fst q.snd < max p.fst p.snd ∨
    max q.fst q.snd = max p.fst p.snd ∧ (q.fst < p.fst ∨ q.fst = p.fst ∧ q.snd < p.snd)
⊢ q ∈ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
exact max_le_iff.1 (le_iff_lt_or_eq.2 <| h.imp_right And.left)
no goals
case intro.intro.intro.refine'_1
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
this : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p}
H : ↑(insert (g p) {x | r x (g p)}) ≃ ↑{x | r x (g p)} ⊕ PUnit
⊢ card (typein s p) ≤
    card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p)))
exact
  ⟨(Set.embeddingOfSubset _ _ this).trans
      ((Equiv.Set.prod _ _).trans (H.prodCongr H)).toEmbedding⟩
no goals
case intro.intro.intro.refine'_2.inl
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : card (succ (typein (fun x x_1 => x < x_1) (g p))) < ℵ₀
⊢ card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p))) < (#α)
exact (mul_lt_aleph0 qo qo).trans_le ol
case intro.intro.intro.refine'_2.inr
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
this : card (succ (typein LT.lt (g p))) < Quotient.mk isEquivalent α
⊢ card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p))) < (#α)

case this
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ card (succ (typein LT.lt (g p))) < Quotient.mk isEquivalent α
case intro.intro.intro.refine'_2.inr
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p))) < (#α)
suffices : (succ (typein LT.lt (g p))).card < ⟦α⟧
case this
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ succ (typein LT.lt (g p)) < ord (Quotient.mk isEquivalent α)
case this
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ card (succ (typein LT.lt (g p))) < Quotient.mk isEquivalent α
rw [← lt_ord]
case this.a
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ typein LT.lt (g p) < ord (Quotient.mk isEquivalent α)
case this
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ succ (typein LT.lt (g p)) < ord (Quotient.mk isEquivalent α)
apply (ord_isLimit ol).2
case this.a
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ typein LT.lt (g p) < type r
case this.a
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ typein LT.lt (g p) < ord (Quotient.mk isEquivalent α)
rw [mk'_def, e]
no goals
case this.a
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
⊢ typein LT.lt (g p) < type r
apply typein_lt_type
no goals
case intro.intro.intro.refine'_2.inr
c✝ : Cardinal
h✝ : ℵ₀ ≤ c✝
c : Cardinal
x✝ : ∀ (y : Cardinal), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
r : α → α → Prop
wo : IsWellOrder α r
e : ord (#α) = type r
this✝² : LinearOrder α := linearOrderOfSTO r
this✝¹ : IsWellOrder α fun x x_1 => x < x_1
g : α × α → α := fun p => max p.fst p.snd
f : α × α ↪ Ordinal × α × α :=
  { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p),
    inj' :=
      (_ :
        ∀ (p q : α × α),
          (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p =
              (fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q →
            ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) p).snd =
              ((fun p => (typein (fun x x_1 => x < x_1) (g p), p)) q).snd) }
s : α × α → α × α → Prop :=
  ↑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
this✝ : IsWellOrder (α × α) s
p : α × α
h : typein s p < type s
qo : ℵ₀ ≤ card (succ (typein (fun x x_1 => x < x_1) (g p)))
this : card (succ (typein LT.lt (g p))) < Quotient.mk isEquivalent α
⊢ card (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p))) < (#α)
exact (IH _ this qo).trans_lt this