[GOAL]
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
⊢ Ordinal.IsLimit (ord c)
[PROOFSTEP]
refine' ⟨fun h => aleph0_ne_zero _, fun a => lt_imp_lt_of_le_imp_le fun h => _⟩
[GOAL]
case refine'_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : ord c = 0
⊢ ℵ₀ = 0
[PROOFSTEP]
rw [← Ordinal.le_zero, ord_le] at h
[GOAL]
case refine'_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : c ≤ card 0
⊢ ℵ₀ = 0
[PROOFSTEP]
simpa only [card_zero, nonpos_iff_eq_zero] using co.trans h
[GOAL]
case refine'_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : ord c ≤ succ a
⊢ ord c ≤ a
[PROOFSTEP]
rw [ord_le] at h ⊢
[GOAL]
case refine'_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ card (succ a)
⊢ c ≤ card a
[PROOFSTEP]
rwa [← @add_one_of_aleph0_le (card a), ← card_succ]
[GOAL]
case refine'_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card a
[PROOFSTEP]
rw [← ord_le, ← le_succ_of_isLimit, ord_le]
[GOAL]
case refine'_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card (succ a)
[PROOFSTEP]
exact co.trans h
[GOAL]
case refine'_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit (ord ℵ₀)
[PROOFSTEP]
rw [ord_aleph0]
[GOAL]
case refine'_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit ω
[PROOFSTEP]
exact omega_isLimit
[GOAL]
a b : Cardinal.{u_1}
⊢ alephIdx a ≤ alephIdx b ↔ a ≤ b
[PROOFSTEP]
rw [← not_lt, ← not_lt, alephIdx_lt]
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
⊢ False
[PROOFSTEP]
have : ∀ c, alephIdx c < o := fun c => (e _).2 ⟨_, rfl⟩
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
⊢ False
[PROOFSTEP]
refine' Ordinal.inductionOn o _ this
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
⊢ ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α r], (∀ (c : Cardinal.{u}), alephIdx c < type r) → False
[PROOFSTEP]
intro α r _ h
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h : ∀ (c : Cardinal.{u}), alephIdx c < type r
⊢ False
[PROOFSTEP]
let s := ⨆ a, invFun alephIdx (Ordinal.typein r a)
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h : ∀ (c : Cardinal.{u}), alephIdx c < type r
s : Cardinal.{u} := ⨆ (a : α), Function.invFun alephIdx (typein r a)
⊢ False
[PROOFSTEP]
apply (lt_succ s).not_le
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h : ∀ (c : Cardinal.{u}), alephIdx c < type r
s : Cardinal.{u} := ⨆ (a : α), Function.invFun alephIdx (typein r a)
⊢ succ s ≤ s
[PROOFSTEP]
have I : Injective.{u + 2, u + 2} alephIdx := alephIdx.initialSeg.toEmbedding.injective
[GOAL]
x✝ : ∃ b, ∀ (x : Ordinal.{u}), x < b ↔ ∃ y, ↑initialSeg y = x
o : Ordinal.{u}
e : ∀ (x : Ordinal.{u}), x < o ↔ ∃ y, ↑initialSeg y = x
this : ∀ (c : Cardinal.{u}), alephIdx c < o
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h : ∀ (c : Cardinal.{u}), alephIdx c < type r
s : Cardinal.{u} := ⨆ (a : α), Function.invFun alephIdx (typein r a)
I : Injective alephIdx
⊢ succ s ≤ s
[PROOFSTEP]
simpa only [typein_enum, leftInverse_invFun I (succ s)] using
  le_ciSup (Cardinal.bddAbove_range.{u, u} fun a : α => invFun alephIdx (Ordinal.typein r a))
    (Ordinal.enum r _ (h (succ s)))
[GOAL]
⊢ (type fun x x_1 => x < x_1) = Ordinal.univ
[PROOFSTEP]
rw [Ordinal.univ_id]
[GOAL]
⊢ (type fun x x_1 => x < x_1) = type fun x x_1 => x < x_1
[PROOFSTEP]
exact Quotient.sound ⟨alephIdx.relIso⟩
[GOAL]
⊢ #Cardinal.{u} = univ
[PROOFSTEP]
simpa only [card_type, card_univ] using congr_arg card type_cardinal
[GOAL]
⊢ aleph' 0 = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, ← aleph'_alephIdx 0, aleph'_le]
[GOAL]
⊢ 0 ≤ alephIdx 0
[PROOFSTEP]
apply Ordinal.zero_le
[GOAL]
o : Ordinal.{u_1}
⊢ aleph' (succ o) = succ (aleph' o)
[PROOFSTEP]
apply (succ_le_of_lt <| aleph'_lt.2 <| lt_succ o).antisymm' (Cardinal.alephIdx_le.1 <| _)
[GOAL]
o : Ordinal.{u_1}
⊢ alephIdx (aleph' (succ o)) ≤ alephIdx (succ (aleph' o))
[PROOFSTEP]
rw [alephIdx_aleph', succ_le_iff, ← aleph'_lt, aleph'_alephIdx]
[GOAL]
o : Ordinal.{u_1}
⊢ aleph' o < succ (aleph' o)
[PROOFSTEP]
apply lt_succ
[GOAL]
n : ℕ
⊢ aleph' (succ ↑n) = ↑(Nat.succ n)
[PROOFSTEP]
rw [aleph'_succ, aleph'_nat n, nat_succ]
[GOAL]
o : Ordinal.{u_1}
l : Ordinal.IsLimit o
c : Cardinal.{u_1}
h : ∀ (o' : Ordinal.{u_1}), o' < o → aleph' o' ≤ c
⊢ aleph' o ≤ c
[PROOFSTEP]
rw [← aleph'_alephIdx c, aleph'_le, limit_le l]
[GOAL]
o : Ordinal.{u_1}
l : Ordinal.IsLimit o
c : Cardinal.{u_1}
h : ∀ (o' : Ordinal.{u_1}), o' < o → aleph' o' ≤ c
⊢ ∀ (x : Ordinal.{u_1}), x < o → x ≤ alephIdx c
[PROOFSTEP]
intro x h'
[GOAL]
o : Ordinal.{u_1}
l : Ordinal.IsLimit o
c : Cardinal.{u_1}
h : ∀ (o' : Ordinal.{u_1}), o' < o → aleph' o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ x ≤ alephIdx c
[PROOFSTEP]
rw [← aleph'_le, aleph'_alephIdx]
[GOAL]
o : Ordinal.{u_1}
l : Ordinal.IsLimit o
c : Cardinal.{u_1}
h : ∀ (o' : Ordinal.{u_1}), o' < o → aleph' o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ aleph' x ≤ c
[PROOFSTEP]
exact h _ h'
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ aleph' o = ⨆ (a : ↑(Iio o)), aleph' ↑a
[PROOFSTEP]
refine' le_antisymm _ (ciSup_le' fun i => aleph'_le.2 (le_of_lt i.2))
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ aleph' o ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
[PROOFSTEP]
rw [aleph'_le_of_limit ho]
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ ∀ (o' : Ordinal.{u_1}), o' < o → aleph' o' ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
[PROOFSTEP]
exact fun a ha => le_ciSup (bddAbove_of_small _) (⟨a, ha⟩ : Iio o)
[GOAL]
c : Cardinal.{u_1}
⊢ aleph' ω ≤ c ↔ ℵ₀ ≤ c
[PROOFSTEP]
simp only [aleph'_le_of_limit omega_isLimit, lt_omega, exists_imp, aleph0_le]
[GOAL]
c : Cardinal.{u_1}
⊢ (∀ (o' : Ordinal.{u_1}) (x : ℕ), o' = ↑x → aleph' o' ≤ c) ↔ ∀ (n : ℕ), ↑n ≤ c
[PROOFSTEP]
exact forall_swap.trans (forall_congr' fun n => by simp only [forall_eq, aleph'_nat])
[GOAL]
c : Cardinal.{u_1}
n : ℕ
⊢ (∀ (x : Ordinal.{u_1}), x = ↑n → aleph' x ≤ c) ↔ ↑n ≤ c
[PROOFSTEP]
simp only [forall_eq, aleph'_nat]
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
[PROOFSTEP]
cases' le_total (aleph o₁) (aleph o₂) with h h
[GOAL]
case inl
o₁ o₂ : Ordinal.{u_1}
h : aleph o₁ ≤ aleph o₂
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
[PROOFSTEP]
rw [max_eq_right h, max_eq_right (aleph_le.1 h)]
[GOAL]
case inr
o₁ o₂ : Ordinal.{u_1}
h : aleph o₂ ≤ aleph o₁
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
[PROOFSTEP]
rw [max_eq_left h, max_eq_left (aleph_le.1 h)]
[GOAL]
o : Ordinal.{u_1}
⊢ aleph (succ o) = succ (aleph o)
[PROOFSTEP]
rw [aleph, add_succ, aleph'_succ, aleph]
[GOAL]
⊢ aleph 0 = ℵ₀
[PROOFSTEP]
rw [aleph, add_zero, aleph'_omega]
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ aleph o = ⨆ (a : ↑(Iio o)), aleph ↑a
[PROOFSTEP]
apply le_antisymm _ (ciSup_le' _)
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ aleph o ≤ ⨆ (i : ↑(Iio o)), aleph ↑i
[PROOFSTEP]
rw [aleph, aleph'_limit (ho.add _)]
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ ⨆ (a : ↑(Iio (ω + o))), aleph' ↑a ≤ ⨆ (i : ↑(Iio o)), aleph ↑i
[PROOFSTEP]
refine' ciSup_mono' (bddAbove_of_small _) _
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio (ω + o))), ∃ i', aleph' ↑i ≤ aleph ↑i'
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mk
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
i : Ordinal.{u_1}
hi : i ∈ Iio (ω + o)
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
[PROOFSTEP]
cases' lt_or_le i ω with h h
[GOAL]
case mk.inl
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
i : Ordinal.{u_1}
hi : i ∈ Iio (ω + o)
h : i < ω
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
[PROOFSTEP]
rcases lt_omega.1 h with ⟨n, rfl⟩
[GOAL]
case mk.inl.intro
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ ∃ i', aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑i'
[PROOFSTEP]
use⟨0, ho.pos⟩
[GOAL]
case h
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑{ val := 0, property := (_ : 0 < o) }
[PROOFSTEP]
simpa using (nat_lt_aleph0 n).le
[GOAL]
case mk.inr
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
i : Ordinal.{u_1}
hi : i ∈ Iio (ω + o)
h : ω ≤ i
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
[PROOFSTEP]
exact ⟨⟨_, (sub_lt_of_le h).2 hi⟩, aleph'_le.2 (le_add_sub _ _)⟩
[GOAL]
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio o)), aleph ↑i ≤ aleph o
[PROOFSTEP]
exact fun i => aleph_le.2 (le_of_lt i.2)
[GOAL]
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ aleph' o ↔ ω ≤ o
[PROOFSTEP]
rw [← aleph'_omega, aleph'_le]
[GOAL]
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ aleph o
[PROOFSTEP]
rw [aleph, aleph0_le_aleph']
[GOAL]
o : Ordinal.{u_1}
⊢ ω ≤ ω + o
[PROOFSTEP]
apply Ordinal.le_add_right
[GOAL]
o : Ordinal.{u_1}
ho : 0 < o
⊢ 0 < aleph' o
[PROOFSTEP]
rwa [← aleph'_zero, aleph'_lt]
[GOAL]
o : Ordinal.{?u.105251}
⊢ Nonempty (Quotient.out (ord (aleph o))).α
[PROOFSTEP]
rw [out_nonempty_iff_ne_zero, ← ord_zero]
[GOAL]
o : Ordinal.{?u.105266}
⊢ ord (aleph o) ≠ ord 0
[PROOFSTEP]
exact fun h => (ord_injective h).not_gt (aleph_pos o)
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = aleph (alephIdx c - ω)
[PROOFSTEP]
rw [aleph, Ordinal.add_sub_cancel_of_le, aleph'_alephIdx]
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ alephIdx c
[PROOFSTEP]
rwa [← aleph0_le_aleph', aleph'_alephIdx]
[GOAL]
o : Ordinal.{u_1}
l : Ordinal.IsLimit o
a : Ordinal.{u_1}
⊢ (ord ∘ aleph') o ≤ a ↔ ∀ (b : Ordinal.{u_1}), b < o → (ord ∘ aleph') b ≤ a
[PROOFSTEP]
simp [ord_le, aleph'_le_of_limit l]
[GOAL]
⊢ succ ℵ₀ = aleph 1
[PROOFSTEP]
rw [← aleph_zero, ← aleph_succ, Ordinal.succ_zero]
[GOAL]
⊢ ℵ₀ < aleph 1
[PROOFSTEP]
rw [← succ_aleph0]
[GOAL]
⊢ ℵ₀ < succ ℵ₀
[PROOFSTEP]
apply lt_succ
[GOAL]
α : Type u_1
s : Set α
⊢ Set.Countable s ↔ #↑s < aleph 1
[PROOFSTEP]
rw [← succ_aleph0, lt_succ_iff, le_aleph0_iff_set_countable]
[GOAL]
a : Ordinal.{u_1}
⊢ ord (succ (card a)) ∈ {b | ord (card b) = b}
[PROOFSTEP]
dsimp
[GOAL]
a : Ordinal.{u_1}
⊢ ord (card (ord (succ (card a)))) = ord (succ (card a))
[PROOFSTEP]
rw [card_ord]
[GOAL]
o : Ordinal.{u_1}
ho : ord (card o) = o
⊢ ord (aleph' (↑alephIdx.relIso (card o))) = o
[PROOFSTEP]
simpa using ho
[GOAL]
⊢ ord ∘ aleph' = enumOrd {b | ord (card b) = b}
[PROOFSTEP]
rw [← eq_enumOrd _ ord_card_unbounded, range_eq_iff]
[GOAL]
⊢ StrictMono (ord ∘ aleph') ∧
    (∀ (a : Ordinal.{u_1}), (ord ∘ aleph') a ∈ {b | ord (card b) = b}) ∧
      ∀ (b : Ordinal.{u_1}), b ∈ {b | ord (card b) = b} → ∃ a, (ord ∘ aleph') a = b
[PROOFSTEP]
exact
  ⟨aleph'_isNormal.strictMono,
    ⟨fun a => by
      dsimp
      rw [card_ord], fun b hb => eq_aleph'_of_eq_card_ord hb⟩⟩
[GOAL]
a : Ordinal.{u_1}
⊢ (ord ∘ aleph') a ∈ {b | ord (card b) = b}
[PROOFSTEP]
dsimp
[GOAL]
a : Ordinal.{u_1}
⊢ ord (card (ord (aleph' a))) = ord (aleph' a)
[PROOFSTEP]
rw [card_ord]
[GOAL]
o : Ordinal.{u_1}
ho : ord (card o) = o
ho' : ω ≤ o
⊢ ∃ a, ord (aleph a) = o
[PROOFSTEP]
cases' eq_aleph'_of_eq_card_ord ho with a ha
[GOAL]
case intro
o : Ordinal.{u_1}
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : ord (aleph' a) = o
⊢ ∃ a, ord (aleph a) = o
[PROOFSTEP]
use a - ω
[GOAL]
case h
o : Ordinal.{u_1}
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : ord (aleph' a) = o
⊢ ord (aleph (a - ω)) = o
[PROOFSTEP]
unfold aleph
[GOAL]
case h
o : Ordinal.{u_1}
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : ord (aleph' a) = o
⊢ ord (aleph' (ω + (a - ω))) = o
[PROOFSTEP]
rwa [Ordinal.add_sub_cancel_of_le]
[GOAL]
case h
o : Ordinal.{u_1}
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : ord (aleph' a) = o
⊢ ω ≤ a
[PROOFSTEP]
rwa [← aleph0_le_aleph', ← ord_le_ord, ha, ord_aleph0]
[GOAL]
⊢ ord ∘ aleph = enumOrd {b | ord (card b) = b ∧ ω ≤ b}
[PROOFSTEP]
rw [← eq_enumOrd _ ord_card_unbounded']
[GOAL]
⊢ StrictMono (ord ∘ aleph) ∧ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
[PROOFSTEP]
use aleph_isNormal.strictMono
[GOAL]
case right
⊢ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
[PROOFSTEP]
rw [range_eq_iff]
[GOAL]
case right
⊢ (∀ (a : Ordinal.{u_1}), (ord ∘ aleph) a ∈ {b | ord (card b) = b ∧ ω ≤ b}) ∧
    ∀ (b : Ordinal.{u_1}), b ∈ {b | ord (card b) = b ∧ ω ≤ b} → ∃ a, (ord ∘ aleph) a = b
[PROOFSTEP]
refine' ⟨fun a => ⟨_, _⟩, fun b hb => eq_aleph_of_eq_card_ord hb.1 hb.2⟩
[GOAL]
case right.refine'_1
a : Ordinal.{u_1}
⊢ ord (card ((ord ∘ aleph) a)) = (ord ∘ aleph) a
[PROOFSTEP]
rw [Function.comp_apply, card_ord]
[GOAL]
case right.refine'_2
a : Ordinal.{u_1}
⊢ ω ≤ (ord ∘ aleph) a
[PROOFSTEP]
rw [← ord_aleph0, Function.comp_apply, ord_le_ord]
[GOAL]
case right.refine'_2
a : Ordinal.{u_1}
⊢ ℵ₀ ≤ aleph a
[PROOFSTEP]
exact aleph0_le_aleph _
[GOAL]
⊢ StrictMono beth
[PROOFSTEP]
intro a b
[GOAL]
a b : Ordinal.{u_1}
⊢ a < b → beth a < beth b
[PROOFSTEP]
induction' b using Ordinal.induction with b IH generalizing a
[GOAL]
case h
a✝ b : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < b → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
a : Ordinal.{u_1}
⊢ a < b → beth a < beth b
[PROOFSTEP]
intro h
[GOAL]
case h
a✝ b : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < b → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
a : Ordinal.{u_1}
h : a < b
⊢ beth a < beth b
[PROOFSTEP]
rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)
[GOAL]
case h.inl
a✝ a : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < 0 → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a < 0
⊢ beth a < beth 0
[PROOFSTEP]
exact (Ordinal.not_lt_zero a h).elim
[GOAL]
case h.inr.inl.intro
a✝ a c : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ c → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a < succ c
⊢ beth a < beth (succ c)
[PROOFSTEP]
rw [lt_succ_iff] at h
[GOAL]
case h.inr.inl.intro
a✝ a c : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ c → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < beth (succ c)
[PROOFSTEP]
rw [beth_succ]
[GOAL]
case h.inr.inl.intro
a✝ a c : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ c → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a < 2 ^ beth c
[PROOFSTEP]
apply lt_of_le_of_lt _ (cantor _)
[GOAL]
a✝ a c : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ c → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a ≤ c
⊢ beth a ≤ beth c
[PROOFSTEP]
rcases eq_or_lt_of_le h with (rfl | h)
[GOAL]
case inl
a✝ a : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ a → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h : a ≤ a
⊢ beth a ≤ beth a
[PROOFSTEP]
rfl
[GOAL]
case inr
a✝ a c : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < succ c → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
h✝ : a ≤ c
h : a < c
⊢ beth a ≤ beth c
[PROOFSTEP]
exact (IH c (lt_succ c) h).le
[GOAL]
case h.inr.inr
a✝ b : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < b → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
a : Ordinal.{u_1}
h : a < b
hb : Ordinal.IsLimit b
⊢ beth a < beth b
[PROOFSTEP]
apply (cantor _).trans_le
[GOAL]
case h.inr.inr
a✝ b : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < b → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
a : Ordinal.{u_1}
h : a < b
hb : Ordinal.IsLimit b
⊢ 2 ^ beth a ≤ beth b
[PROOFSTEP]
rw [beth_limit hb, ← beth_succ]
[GOAL]
case h.inr.inr
a✝ b : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < b → ∀ ⦃a : Ordinal.{u_1}⦄, a < k → beth a < beth k
a : Ordinal.{u_1}
h : a < b
hb : Ordinal.IsLimit b
⊢ beth (succ a) ≤ ⨆ (a : ↑(Iio b)), beth ↑a
[PROOFSTEP]
exact le_ciSup (bddAbove_of_small _) (⟨_, hb.succ_lt h⟩ : Iio b)
[GOAL]
o : Ordinal.{u_1}
⊢ aleph o ≤ beth o
[PROOFSTEP]
induction o using limitRecOn with
| H₁ => simp
| H₂ o h =>
  rw [aleph_succ, beth_succ, succ_le_iff]
  exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
| H₃ o ho IH =>
  rw [aleph_limit ho, beth_limit ho]
  exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2
[GOAL]
o : Ordinal.{u_1}
⊢ aleph o ≤ beth o
[PROOFSTEP]
induction o using limitRecOn with
| H₁ => simp
| H₂ o h =>
  rw [aleph_succ, beth_succ, succ_le_iff]
  exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
| H₃ o ho IH =>
  rw [aleph_limit ho, beth_limit ho]
  exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2
[GOAL]
case H₁
⊢ aleph 0 ≤ beth 0
[PROOFSTEP]

| H₁ => simp
[GOAL]
case H₁
⊢ aleph 0 ≤ beth 0
[PROOFSTEP]
simp
[GOAL]
case H₂
o : Ordinal.{u_1}
h : aleph o ≤ beth o
⊢ aleph (succ o) ≤ beth (succ o)
[PROOFSTEP]

| H₂ o h =>
  rw [aleph_succ, beth_succ, succ_le_iff]
  exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
[GOAL]
case H₂
o : Ordinal.{u_1}
h : aleph o ≤ beth o
⊢ aleph (succ o) ≤ beth (succ o)
[PROOFSTEP]
rw [aleph_succ, beth_succ, succ_le_iff]
[GOAL]
case H₂
o : Ordinal.{u_1}
h : aleph o ≤ beth o
⊢ aleph o < 2 ^ beth o
[PROOFSTEP]
exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
[GOAL]
case H₃
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal.{u_1}), o' < o → aleph o' ≤ beth o'
⊢ aleph o ≤ beth o
[PROOFSTEP]

| H₃ o ho IH =>
  rw [aleph_limit ho, beth_limit ho]
  exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2
[GOAL]
case H₃
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal.{u_1}), o' < o → aleph o' ≤ beth o'
⊢ aleph o ≤ beth o
[PROOFSTEP]
rw [aleph_limit ho, beth_limit ho]
[GOAL]
case H₃
o : Ordinal.{u_1}
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal.{u_1}), o' < o → aleph o' ≤ beth o'
⊢ ⨆ (a : ↑(Iio o)), aleph ↑a ≤ ⨆ (a : ↑(Iio o)), beth ↑a
[PROOFSTEP]
exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2
[GOAL]
o : Ordinal.{u}
ho : Ordinal.IsLimit o
a : Ordinal.{u}
ha : ∀ (b : Ordinal.{u}), b < o → ord (beth b) ≤ a
⊢ ord (beth o) ≤ a
[PROOFSTEP]
rw [beth_limit ho, ord_le]
[GOAL]
o : Ordinal.{u}
ho : Ordinal.IsLimit o
a : Ordinal.{u}
ha : ∀ (b : Ordinal.{u}), b < o → ord (beth b) ≤ a
⊢ ⨆ (a : ↑(Iio o)), beth ↑a ≤ card a
[PROOFSTEP]
exact ciSup_le' fun b => ord_le.1 (ha _ b.2)
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c * c = c
[PROOFSTEP]
refine'
  le_antisymm _
    (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c)
      -- the only nontrivial part is `c * c ≤ c`. We prove it inductively.
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c * c
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c * c ≤ c
[PROOFSTEP]
refine' Acc.recOn (Cardinal.lt_wf.apply c) (fun c _ => Quotient.inductionOn c fun α IH ol => _) h
[GOAL]
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), y < Quotient.mk isEquivalent α → ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
[PROOFSTEP]
rcases ord_eq α with ⟨r, wo, e⟩
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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 α
[PROOFSTEP]
skip
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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 α
[PROOFSTEP]
letI := linearOrderOfSTO r
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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 α
[PROOFSTEP]
haveI : IsWellOrder α (· < ·) := wo
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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 α
[PROOFSTEP]
let g : α × α → α := fun p => max p.1 p.2
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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 α
[PROOFSTEP]
let f : α × α ↪ Ordinal × α × α := ⟨fun p : α × α => (typein (· < ·) (g p), p), fun p q => congr_arg Prod.snd⟩
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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) }
⊢ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α
[PROOFSTEP]
let s :=
  f ⁻¹'o
    Prod.Lex (· < ·)
      (Prod.Lex (· < ·) (· < ·))
        -- this is a well order on `α × α`.
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α
[PROOFSTEP]
haveI : IsWellOrder _ s := (RelEmbedding.preimage _ _).isWellOrder
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α
[PROOFSTEP]
suffices type s ≤ type r by exact card_le_card this
[GOAL]
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α
[PROOFSTEP]
exact card_le_card this
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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
[PROOFSTEP]
refine' le_of_forall_lt fun o h => _
[GOAL]
case intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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.{u_1}
h : o < type s
⊢ o < type r
[PROOFSTEP]
rcases typein_surj s h with ⟨p, rfl⟩
[GOAL]
case intro.intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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
[PROOFSTEP]
rw [← e, lt_ord]
[GOAL]
case intro.intro.intro
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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) < #α
[PROOFSTEP]
refine' lt_of_le_of_lt (_ : _ ≤ card (succ (typein (· < ·) (g p))) * card (succ (typein (· < ·) (g p)))) _
[GOAL]
case intro.intro.intro.refine'_1
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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)))
[PROOFSTEP]
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)
[GOAL]
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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}
[PROOFSTEP]
intro q h
[GOAL]
c✝ : Cardinal.{u_1}
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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}
[PROOFSTEP]
simp only [Preimage, ge_iff_le, Embedding.coeFn_mk, Prod.lex_def, typein_lt_typein, typein_inj, mem_setOf_eq] at h
[GOAL]
c✝ : Cardinal.{u_1}
h✝¹ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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}
[PROOFSTEP]
exact max_le_iff.1 (le_iff_lt_or_eq.2 <| h.imp_right And.left)
[GOAL]
case intro.intro.intro.refine'_1
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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)))
[PROOFSTEP]
suffices H : (insert (g p) {x | r x (g p)} : Set α) ≃ Sum {x | r x (g p)} PUnit
[GOAL]
case intro.intro.intro.refine'_1
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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)))
[PROOFSTEP]
exact ⟨(Set.embeddingOfSubset _ _ this).trans ((Equiv.Set.prod _ _).trans (H.prodCongr H)).toEmbedding⟩
[GOAL]
case H
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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
[PROOFSTEP]
refine' (Equiv.Set.insert _).trans ((Equiv.refl _).sumCongr punitEquivPUnit)
[GOAL]
case H
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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)}
[PROOFSTEP]
apply @irrefl _ r
[GOAL]
case intro.intro.intro.refine'_2
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 (succ (typein (fun x x_1 => x < x_1) (g p))) * card (succ (typein (fun x x_1 => x < x_1) (g p))) < #α
[PROOFSTEP]
cases' lt_or_le (card (succ (typein (· < ·) (g p)))) ℵ₀ with qo qo
[GOAL]
case intro.intro.intro.refine'_2.inl
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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))) < #α
[PROOFSTEP]
exact (mul_lt_aleph0 qo qo).trans_le ol
[GOAL]
case intro.intro.intro.refine'_2.inr
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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))) < #α
[PROOFSTEP]
suffices : (succ (typein LT.lt (g p))).card < ⟦α⟧
[GOAL]
case intro.intro.intro.refine'_2.inr
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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))) < #α
[PROOFSTEP]
exact (IH _ this qo).trans_lt this
[GOAL]
case this
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α
[PROOFSTEP]
rw [← lt_ord]
[GOAL]
case this
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α)
[PROOFSTEP]
apply (ord_isLimit ol).2
[GOAL]
case this.a
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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 α)
[PROOFSTEP]
rw [mk'_def, e]
[GOAL]
case this.a
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ (y : Cardinal.{u_1}), y < c → Acc (fun x x_1 => x < x_1) y
α : Type u_1
IH : ∀ (y : Cardinal.{u_1}), 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.{u_1} × α × α :=
  { 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
[PROOFSTEP]
apply typein_lt_type
[GOAL]
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a
[GOAL]
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b
[PROOFSTEP]
simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ aleph o₁ * aleph o₂ = aleph (max o₁ o₂)
[PROOFSTEP]
rw [Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), max_aleph_eq]
[GOAL]
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c
[PROOFSTEP]
rw [mul_eq_self h]
[GOAL]
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
[PROOFSTEP]
exact max_lt h1 h2
[GOAL]
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b
[PROOFSTEP]
convert mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
[GOAL]
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ max a b = max a b * max a b
[PROOFSTEP]
rw [mul_eq_self]
[GOAL]
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b
[PROOFSTEP]
refine' h.trans (le_max_left a b)
[GOAL]
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
⊢ a * b = max a b
[PROOFSTEP]
cases' le_or_lt ℵ₀ b with hb hb
[GOAL]
case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = max a b
[PROOFSTEP]
exact mul_eq_max h hb
[GOAL]
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = max a b
[PROOFSTEP]
refine' (mul_le_max_of_aleph0_le_left h).antisymm _
[GOAL]
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ max a b ≤ a * b
[PROOFSTEP]
have : b ≤ a := hb.le.trans h
[GOAL]
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ max a b ≤ a * b
[PROOFSTEP]
rw [max_eq_left this]
[GOAL]
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b
[PROOFSTEP]
convert mul_le_mul_left' (one_le_iff_ne_zero.mpr h') a
[GOAL]
case h.e'_3
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b
[PROOFSTEP]
simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h
[GOAL]
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b
[PROOFSTEP]
rw [mul_comm, max_comm]
[GOAL]
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a
[PROOFSTEP]
exact mul_eq_max_of_aleph0_le_left h h'
[GOAL]
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = max a b
[PROOFSTEP]
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
[GOAL]
case intro.intro.inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b
[PROOFSTEP]
exact mul_eq_max_of_aleph0_le_left ha' hb
[GOAL]
case intro.intro.inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b
[PROOFSTEP]
exact mul_eq_max_of_aleph0_le_right ha hb'
[GOAL]
a b : Cardinal.{u_1}
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha0)
[GOAL]
case inl
b : Cardinal.{u_1}
⊢ 0 * b ≤ max (max 0 b) ℵ₀
[PROOFSTEP]
simp
[GOAL]
case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb0)
[GOAL]
case inr.inl
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with ha ha
[GOAL]
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rw [mul_eq_max_of_aleph0_le_left ha hb0]
[GOAL]
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ b with hb hb
[GOAL]
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
[GOAL]
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_of_le_right (mul_lt_aleph0 ha hb).le
[GOAL]
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ a * b = a
[PROOFSTEP]
rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]
[GOAL]
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ a * b = b
[PROOFSTEP]
rw [mul_comm, mul_eq_left hb ha ha']
[GOAL]
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
[PROOFSTEP]
convert mul_le_mul_right' (one_le_iff_ne_zero.mpr h) a
[GOAL]
case h.e'_3
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = 1 * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
[PROOFSTEP]
exact le_mul_left h
[GOAL]
a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
rw [max_le_iff]
[GOAL]
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with ha ha
[GOAL]
case refine'_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
have : a ≠ 0 := by
  rintro rfl
  exact ha.not_lt aleph0_pos
[GOAL]
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False
[PROOFSTEP]
exact ha.not_lt aleph0_pos
[GOAL]
case refine'_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
left
[GOAL]
case refine'_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
[PROOFSTEP]
rw [and_assoc]
[GOAL]
case refine'_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
[PROOFSTEP]
use ha
[GOAL]
case right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a
[PROOFSTEP]
rw [← not_lt]
[GOAL]
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b
[PROOFSTEP]
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
[GOAL]
case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False
[PROOFSTEP]
apply this
[GOAL]
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0
[PROOFSTEP]
rw [mul_zero] at h
[GOAL]
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0
[PROOFSTEP]
exact h.symm
[GOAL]
case refine'_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
[PROOFSTEP]
right
[GOAL]
case refine'_1.inr.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0
[PROOFSTEP]
by_cases h2a : a = 0
[GOAL]
case pos
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0
[PROOFSTEP]
exact Or.inr h2a
[GOAL]
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0
[PROOFSTEP]
have hb : b ≠ 0 := by
  rintro rfl
  apply h2a
  rw [mul_zero] at h
  exact h.symm
[GOAL]
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False
[PROOFSTEP]
apply h2a
[GOAL]
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0
[PROOFSTEP]
rw [mul_zero] at h
[GOAL]
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0
[PROOFSTEP]
exact h.symm
[GOAL]
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0
[PROOFSTEP]
left
[GOAL]
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
[PROOFSTEP]
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
[GOAL]
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
[PROOFSTEP]
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
[GOAL]
case neg.h.inl
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1
case neg.h.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1
case neg.h.inr.inr.intro.intro.intro n : ℕ h2a : ¬↑n = 0 m : ℕ hb : ↑m ≠ 0 h : ↑n * ↑m = ↑n ⊢ ↑m = 1
[PROOFSTEP]
contradiction
[GOAL]
case neg.h.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1
case neg.h.inr.inr.intro.intro.intro n : ℕ h2a : ¬↑n = 0 m : ℕ hb : ↑m ≠ 0 h : ↑n * ↑m = ↑n ⊢ ↑m = 1
[PROOFSTEP]
contradiction
[GOAL]
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
[PROOFSTEP]
rw [← Ne] at h2a
[GOAL]
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
[PROOFSTEP]
rw [← one_le_iff_ne_zero] at h2a hb
[GOAL]
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
[PROOFSTEP]
norm_cast at h2a hb h ⊢
[GOAL]
case neg.h.inr.inr.intro.intro.intro
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1
[PROOFSTEP]
apply le_antisymm _ hb
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1
[PROOFSTEP]
rw [← not_lt]
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
[PROOFSTEP]
apply fun h2b => ne_of_gt _ h
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m
[PROOFSTEP]
conv_rhs => left; rw [← mul_one n]
[GOAL]
case h₂
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
| n < n * m
[PROOFSTEP]
left; rw [← mul_one n]
[GOAL]
case h₂
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
| n < n * m
[PROOFSTEP]
left; rw [← mul_one n]
[GOAL]
case h₂
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
| n < n * m
[PROOFSTEP]
left
[GOAL]
case h₂
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
| n
[PROOFSTEP]
rw [← mul_one n]
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m
[PROOFSTEP]
rw [mul_lt_mul_left]
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m
n m : ℕ h2a : 1 ≤ n hb : 1 ≤ m h : n * m = n ⊢ 0 < n
[PROOFSTEP]
exact id
[GOAL]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
[PROOFSTEP]
apply Nat.lt_of_succ_le h2a
[GOAL]
case refine'_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
[PROOFSTEP]
rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
[GOAL]
case refine'_2.inl.intro.intro
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a
[PROOFSTEP]
rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
[GOAL]
case refine'_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a
case refine'_2.inr.inr b : Cardinal.{u_1} ⊢ 0 * b = 0
[PROOFSTEP]
all_goals simp
[GOAL]
case refine'_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0
[PROOFSTEP]
simp
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c
[PROOFSTEP]
convert mul_le_mul_right' ((nat_lt_aleph0 2).le.trans h) c using 1
[GOAL]
case h.e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c = ↑2 * c
[PROOFSTEP]
simp [two_mul, mul_eq_self h]
[GOAL]
case h.e'_4
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c * c
[PROOFSTEP]
simp [two_mul, mul_eq_self h]
[GOAL]
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ a + b = max a b
[PROOFSTEP]
rw [add_comm, max_comm, add_eq_max ha]
[GOAL]
a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with ha ha
[GOAL]
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rw [add_eq_max ha]
[GOAL]
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
case inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ b with hb hb
[GOAL]
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀
[PROOFSTEP]
rw [add_comm, add_eq_max hb, max_comm]
[GOAL]
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
[PROOFSTEP]
exact le_max_of_le_right (add_lt_aleph0 ha hb).le
[GOAL]
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b + max a b < c
[PROOFSTEP]
rw [add_eq_self h]
[GOAL]
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
[PROOFSTEP]
exact max_lt h1 h2
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b = c
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c
[PROOFSTEP]
rw [← h]
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b
[PROOFSTEP]
apply self_le_add_left
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b
[PROOFSTEP]
rw [← not_lt]
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
[PROOFSTEP]
intro hb
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False
[PROOFSTEP]
have : a + b < c := add_lt_of_lt hc ha hb
[GOAL]
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False
[PROOFSTEP]
simp [h, lt_irrefl] at this
[GOAL]
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a
[PROOFSTEP]
rw [add_eq_max ha, max_eq_left hb]
[GOAL]
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
⊢ a + b = b
[PROOFSTEP]
rw [add_comm, add_eq_left hb ha]
[GOAL]
a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0
[PROOFSTEP]
rw [max_le_iff]
[GOAL]
a b : Cardinal.{u_1}
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
a b : Cardinal.{u_1}
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with ha ha
[GOAL]
case refine'_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
[PROOFSTEP]
left
[GOAL]
case refine'_1.inl.h
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a
[PROOFSTEP]
use ha
[GOAL]
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a
[PROOFSTEP]
rw [← not_lt]
[GOAL]
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
[PROOFSTEP]
apply fun hb => ne_of_gt _ h
[GOAL]
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b
[PROOFSTEP]
intro hb
[GOAL]
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b
[PROOFSTEP]
exact hb.trans_le (self_le_add_left b a)
[GOAL]
case refine'_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
[PROOFSTEP]
right
[GOAL]
case refine'_1.inr.h
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ b = 0
[PROOFSTEP]
rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
[GOAL]
case refine'_1.inr.h
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0
[PROOFSTEP]
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
[GOAL]
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0
[PROOFSTEP]
norm_cast at h ⊢
[GOAL]
case refine'_1.inr.h.intro.intro.intro
n m : ℕ
h : n + m = n
⊢ m = 0
[PROOFSTEP]
rw [← add_right_inj, h, add_zero]
[GOAL]
case refine'_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a
[PROOFSTEP]
rintro (⟨h1, h2⟩ | h3)
[GOAL]
case refine'_2.inl.intro
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a
[PROOFSTEP]
rw [add_eq_max h1, max_eq_left h2]
[GOAL]
case refine'_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a
[PROOFSTEP]
rw [h3, add_zero]
[GOAL]
a b : Cardinal.{u_1}
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0
[PROOFSTEP]
rw [add_comm, add_eq_left_iff]
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
⊢ b = c
[PROOFSTEP]
cases' le_or_lt ℵ₀ b with hb hb
[GOAL]
case inl
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b = c
[PROOFSTEP]
have : a < b := ha.trans_le hb
[GOAL]
case inl
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
[PROOFSTEP]
rw [add_eq_right hb this.le, eq_comm] at h
[GOAL]
case inl
a b c : Cardinal.{u_1}
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
[PROOFSTEP]
rw [eq_of_add_eq_of_aleph0_le h this hb]
[GOAL]
case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c
[PROOFSTEP]
have hc : c < ℵ₀ := by
  rw [← not_le]
  intro hc
  apply lt_irrefl ℵ₀
  apply (hc.trans (self_le_add_left _ a)).trans_lt
  rw [← h]
  apply add_lt_aleph0 ha hb
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ c < ℵ₀
[PROOFSTEP]
rw [← not_le]
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ¬ℵ₀ ≤ c
[PROOFSTEP]
intro hc
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ False
[PROOFSTEP]
apply lt_irrefl ℵ₀
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ ℵ₀ < ℵ₀
[PROOFSTEP]
apply (hc.trans (self_le_add_left _ a)).trans_lt
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀
[PROOFSTEP]
rw [← h]
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + b < ℵ₀
[PROOFSTEP]
apply add_lt_aleph0 ha hb
[GOAL]
case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ b = c
[PROOFSTEP]
rw [lt_aleph0] at *
[GOAL]
case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c
[PROOFSTEP]
rcases ha with ⟨n, rfl⟩
[GOAL]
case inr.intro
b c : Cardinal.{u_1}
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
n : ℕ
h : ↑n + b = ↑n + c
⊢ b = c
[PROOFSTEP]
rcases hb with ⟨m, rfl⟩
[GOAL]
case inr.intro.intro
c : Cardinal.{u_1}
hc : ∃ n, c = ↑n
n m : ℕ
h : ↑n + ↑m = ↑n + c
⊢ ↑m = c
[PROOFSTEP]
rcases hc with ⟨k, rfl⟩
[GOAL]
case inr.intro.intro.intro
n m k : ℕ
h : ↑n + ↑m = ↑n + ↑k
⊢ ↑m = ↑k
[PROOFSTEP]
norm_cast at h ⊢
[GOAL]
case inr.intro.intro.intro
n m k : ℕ
h : n + m = n + k
⊢ m = k
[PROOFSTEP]
apply add_left_cancel h
[GOAL]
a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c
[PROOFSTEP]
rw [add_comm a b, add_comm c b] at h
[GOAL]
a b c : Cardinal.{u_1}
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c
[PROOFSTEP]
exact Cardinal.eq_of_add_eq_add_left h hb
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ aleph o₁ + aleph o₂ = aleph (max o₁ o₂)
[PROOFSTEP]
rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), max_aleph_eq]
[GOAL]
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < ord c
hb : b < ord c
⊢ (fun x x_1 => x + x_1) a b < ord c
[PROOFSTEP]
rw [lt_ord, Ordinal.card_add] at *
[GOAL]
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : card a < c
hb : card b < c
⊢ card a + card b < c
[PROOFSTEP]
exact add_lt_of_lt hc ha hb
[GOAL]
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β
[PROOFSTEP]
refine' ⟨fun h => _, fun h => add_le_add_right h γ⟩
[GOAL]
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β
[PROOFSTEP]
contrapose h
[GOAL]
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ
[PROOFSTEP]
rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
[GOAL]
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ
[PROOFSTEP]
exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩
[GOAL]
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑Nat.zero < ℵ₀
[PROOFSTEP]
rw [Nat.cast_zero, power_zero]
[GOAL]
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ 1 < ℵ₀
[PROOFSTEP]
exact one_lt_aleph0
[GOAL]
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
n : ℕ
ih : Quotient.mk isEquivalent α ^ ↑n ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑(Nat.succ n) ≤ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α
[PROOFSTEP]
rw [Nat.cast_succ, power_add, power_one]
[GOAL]
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
n : ℕ
ih : Quotient.mk isEquivalent α ^ ↑n ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑n * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α
[PROOFSTEP]
exact mul_le_mul_right' ih _
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^ c = 2 ^ c
[PROOFSTEP]
apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c
[PROOFSTEP]
exact power_le_power_right ((nat_lt_aleph0 2).le.trans h)
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c
[PROOFSTEP]
rw [← power_mul, mul_eq_self h]
[GOAL]
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ prod c = 2 ^ lift #ι
[PROOFSTEP]
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
[GOAL]
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ (prod fun i => lift (c i)) = lift (2 ^ #ι)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ (prod fun i => lift (c i)) ≤ lift (2 ^ #ι)
[PROOFSTEP]
refine' (prod_le_prod _ _ h₂).trans_eq _
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ (prod fun i => lift #ι) = lift (2 ^ #ι)
[PROOFSTEP]
rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ lift (2 ^ #ι) ≤ prod fun i => lift (c i)
[PROOFSTEP]
rw [← prod_const', lift_prod]
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
⊢ (prod fun i => lift 2) ≤ prod fun i => lift (c i)
[PROOFSTEP]
refine' prod_le_prod _ _ fun i => _
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
i : ι
⊢ lift 2 ≤ lift (c i)
[PROOFSTEP]
rw [lift_two, ← lift_two.{u, v}, lift_le]
[GOAL]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift #ι
i : ι
⊢ 2 ≤ c i
[PROOFSTEP]
exact h₁ i
[GOAL]
c : Cardinal.{u}
h : ℵ₀ ≤ c
n : ℕ
hn : 2 ≤ n
⊢ 2 ≤ ↑n
[PROOFSTEP]
assumption_mod_cast
[GOAL]
c : Cardinal.{u}
n : ℕ
h1 : ℵ₀ ≤ c
h2 : 1 ≤ n
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast h2
[GOAL]
c : Cardinal.{u}
n : ℕ
⊢ c ^ ↑n ≤ max c ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ c with hc hc
[GOAL]
case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀
[PROOFSTEP]
exact le_max_of_le_left (power_nat_le hc)
[GOAL]
case inr
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀
[PROOFSTEP]
exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le
[GOAL]
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c
[PROOFSTEP]
rw [powerlt_le]
[GOAL]
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ (x : Cardinal.{u_1}), x < ℵ₀ → c ^ x ≤ c
[PROOFSTEP]
intro c'
[GOAL]
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ c' < ℵ₀ → c ^ c' ≤ c
[PROOFSTEP]
rw [lt_aleph0]
[GOAL]
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ (∃ n, c' = ↑n) → c ^ c' ≤ c
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case a.intro
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
n : ℕ
⊢ c ^ ↑n ≤ c
[PROOFSTEP]
apply power_nat_le h
[GOAL]
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀
[PROOFSTEP]
convert le_powerlt c one_lt_aleph0
[GOAL]
case h.e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c ^ 1
[PROOFSTEP]
rw [power_one]
[GOAL]
c : Cardinal.{u_1}
⊢ c ^< ℵ₀ ≤ max c ℵ₀
[PROOFSTEP]
cases' le_or_lt ℵ₀ c with h h
[GOAL]
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀
[PROOFSTEP]
rw [powerlt_aleph0 h]
[GOAL]
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀
[PROOFSTEP]
apply le_max_left
[GOAL]
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
[PROOFSTEP]
rw [powerlt_le]
[GOAL]
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ (x : Cardinal.{u_1}), x < ℵ₀ → c ^ x ≤ max c ℵ₀
[PROOFSTEP]
exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)
[GOAL]
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a => [a]) x✝ = (fun a => [a]) a₂ → x✝ = a₂
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun x => #α) = #α
[PROOFSTEP]
simp [H1]
[GOAL]
α : Type u
inst✝ : Nonempty α
⊢ #(List α) = max #α ℵ₀
[PROOFSTEP]
cases finite_or_infinite α
[GOAL]
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #(List α) = max #α ℵ₀
[PROOFSTEP]
rw [mk_list_eq_aleph0, eq_comm, max_eq_right]
[GOAL]
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀
[PROOFSTEP]
exact mk_le_aleph0
[GOAL]
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #(List α) = max #α ℵ₀
[PROOFSTEP]
rw [mk_list_eq_mk, eq_comm, max_eq_left]
[GOAL]
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α
[PROOFSTEP]
exact aleph0_le_mk α
[GOAL]
α : Type u
⊢ #(List α) ≤ max ℵ₀ #α
[PROOFSTEP]
cases finite_or_infinite α
[GOAL]
case inl
α : Type u
h✝ : Finite α
⊢ #(List α) ≤ max ℵ₀ #α
[PROOFSTEP]
exact mk_le_aleph0.trans (le_max_left _ _)
[GOAL]
case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α
[PROOFSTEP]
rw [mk_list_eq_mk]
[GOAL]
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α
[PROOFSTEP]
apply le_max_right
[GOAL]
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = max (lift #α) (lift #β)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) ≤ max (lift #α) (lift #β)
[PROOFSTEP]
calc
  #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
  _ = #(α × β) := (mk_finset_of_infinite _)
  _ = max (lift.{v} #α) (lift.{u} #β) := by rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
[GOAL]
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α × β) = max (lift #α) (lift #β)
[PROOFSTEP]
rw [mk_prod, mul_eq_max_of_aleph0_le_left]
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ ℵ₀ ≤ lift #α
[PROOFSTEP]
simp
[GOAL]
case h'
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift #β ≠ 0
[PROOFSTEP]
simp
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ max (lift #α) (lift #β) ≤ #(α →₀ β)
[PROOFSTEP]
apply max_le
[GOAL]
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift #α ≤ #(α →₀ β)
[PROOFSTEP]
rw [← lift_id #(α →₀ β), ← lift_umax]
[GOAL]
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift #β ≤ #(α →₀ β)
[PROOFSTEP]
rw [← lift_id #(α →₀ β), ← lift_umax]
[GOAL]
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift #α ≤ lift #(α →₀ β)
[PROOFSTEP]
cases' exists_ne (0 : β) with b hb
[GOAL]
case a.h₁.intro
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift #α ≤ lift #(α →₀ β)
[PROOFSTEP]
exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
[GOAL]
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift #β ≤ lift #(α →₀ β)
[PROOFSTEP]
inhabit α
[GOAL]
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift #β ≤ lift #(α →₀ β)
[PROOFSTEP]
exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩
[GOAL]
α β : Type u
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = max #α #β
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = max (lift #α) (lift #β)
[PROOFSTEP]
cases fintypeOrInfinite α
[GOAL]
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ #(α →₀ β) = max (lift #α) (lift #β)
[PROOFSTEP]
rw [mk_finsupp_lift_of_fintype]
[GOAL]
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift #β ^ Fintype.card α = max (lift #α) (lift #β)
[PROOFSTEP]
have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)
[GOAL]
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift #β
⊢ lift #β ^ Fintype.card α = max (lift #α) (lift #β)
[PROOFSTEP]
rw [max_eq_right (le_trans _ this), power_nat_eq this]
[GOAL]
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift #β
⊢ 1 ≤ Fintype.card α
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift #β
⊢ lift #α ≤ ℵ₀
[PROOFSTEP]
exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le]
[GOAL]
case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ #(α →₀ β) = max (lift #α) (lift #β)
[PROOFSTEP]
apply mk_finsupp_lift_of_infinite
[GOAL]
α β : Type u
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = max #α #β
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = max #α ℵ₀
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Infinite α
⊢ #(Multiset α) = #α
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : IsEmpty α
⊢ #(α →₀ ℕ) = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : Countable α
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = ℵ₀
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #α ^ c
[PROOFSTEP]
refine' le_trans _ (by rw [← add_one_eq (aleph0_le_mk α)])
[GOAL]
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ ?m.211821 ≤ #α ^ c
[PROOFSTEP]
rw [← add_one_eq (aleph0_le_mk α)]
[GOAL]
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c
[PROOFSTEP]
induction' c using Cardinal.inductionOn with β
[GOAL]
case h
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β
[PROOFSTEP]
fapply mk_le_of_surjective
[GOAL]
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β => β → α) (α ⊕ ULift (Fin 1)) β → { t // #↑t ≤ #β }
[PROOFSTEP]
intro f
[GOAL]
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift (Fin 1)) β
⊢ { t // #↑t ≤ #β }
[PROOFSTEP]
use Sum.inl ⁻¹' range f
[GOAL]
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift (Fin 1)) β
⊢ #↑(Sum.inl ⁻¹' range f) ≤ #β
[PROOFSTEP]
refine' le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) _
[GOAL]
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift (Fin 1)) β
⊢ #↑(range f) ≤ #β
[PROOFSTEP]
apply mk_range_le
[GOAL]
case h.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }
[PROOFSTEP]
rintro ⟨s, ⟨g⟩⟩
[GOAL]
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a,
    (fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) a =
      { val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val else Sum.inr (ULift.up 0)
[GOAL]
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
      if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) =
    { val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case h.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) =
    ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
ext x
[GOAL]
case h.a.h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) ↔
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
constructor
[GOAL]
case h.a.h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) →
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
rintro ⟨y, h⟩
[GOAL]
case h.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) y = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
dsimp only at h
[GOAL]
case h.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
by_cases h' : ∃ z : s, g z = y
[GOAL]
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
rw [dif_pos h'] at h
[GOAL]
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
cases Sum.inl.inj h
[GOAL]
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl ↑(choose h')
⊢ ↑(choose h') ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
exact (Classical.choose h').2
[GOAL]
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
rw [dif_neg h'] at h
[GOAL]
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
[PROOFSTEP]
cases h
[GOAL]
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) } →
    x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 })
[PROOFSTEP]
intro h
[GOAL]
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 })
[PROOFSTEP]
have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
[GOAL]
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : #↑(Sum.inl ⁻¹' range f) ≤ #β) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 })
[PROOFSTEP]
use g ⟨x, h⟩
[GOAL]
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr { down := 0 }) (↑g { val := x, property := h }) =
    Sum.inl x
[PROOFSTEP]
dsimp only
[GOAL]
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (if h_1 : ∃ x_1, ↑g x_1 = ↑g { val := x, property := h } then Sum.inl ↑(choose h_1) else Sum.inr { down := 0 }) =
    Sum.inl x
[PROOFSTEP]
rw [dif_pos this]
[GOAL]
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Sum.inl ↑(choose this) = Sum.inl x
[PROOFSTEP]
congr
[GOAL]
case h.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ ↑(choose this) = x
[PROOFSTEP]
suffices : Classical.choose this = ⟨x, h⟩
[GOAL]
case h.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this✝ : ∃ z, ↑g z = ↑g { val := x, property := h }
this : choose this✝ = { val := x, property := h }
⊢ ↑(choose this✝) = x
case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
[PROOFSTEP]
exact congr_arg Subtype.val this
[GOAL]
case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
[PROOFSTEP]
apply g.2
[GOAL]
case this.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Embedding.toFun g (choose this) = Embedding.toFun g { val := x, property := h }
[PROOFSTEP]
exact Classical.choose_spec this
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c
[PROOFSTEP]
trans #{ t : Set (Sum (ULift.{u} ℕ) α) // #t ≤ c }
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #{ t // #↑t ≤ c }
[PROOFSTEP]
refine' ⟨Embedding.subtypeMap _ _⟩
[GOAL]
case refine'_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift ℕ ⊕ α)
case refine'_2 α : Type u c : Cardinal.{u} ⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(↑?refine'_1 x) ≤ c
[PROOFSTEP]
apply Embedding.image
[GOAL]
case refine'_1.f
α : Type u
c : Cardinal.{u}
⊢ α ↪ ULift ℕ ⊕ α
case refine'_2 α : Type u c : Cardinal.{u} ⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(↑(Embedding.image ?refine'_1.f) x) ≤ c
[PROOFSTEP]
use Sum.inr
[GOAL]
case inj'
α : Type u
c : Cardinal.{u}
⊢ Injective Sum.inr
case refine'_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(↑(Embedding.image { toFun := Sum.inr, inj' := ?inj' }) x) ≤ c
[PROOFSTEP]
apply Sum.inr.inj
[GOAL]
case refine'_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄,
    #↑x ≤ c →
      #↑(↑(Embedding.image
                  { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
              x) ≤
        c
[PROOFSTEP]
intro s hs
[GOAL]
case refine'_2
α : Type u
c : Cardinal.{u}
s : Set α
hs : #↑s ≤ c
⊢ #↑(↑(Embedding.image { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
          s) ≤
    c
[PROOFSTEP]
exact mk_image_le.trans hs
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c
[PROOFSTEP]
apply (mk_bounded_set_le_of_infinite (Sum (ULift.{u} ℕ) α) c).trans
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ #(ULift ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
[PROOFSTEP]
rw [max_comm, ← add_eq_max]
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ #(ULift ℕ ⊕ α) ^ c ≤ (ℵ₀ + #α) ^ c
[PROOFSTEP]
rfl
[GOAL]
α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀
[PROOFSTEP]
rfl
[GOAL]
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ max #↑s ℵ₀ ^ c
[PROOFSTEP]
refine' le_trans _ (mk_bounded_set_le s c)
[GOAL]
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }
[PROOFSTEP]
refine' ⟨Embedding.codRestrict _ _ _⟩
[GOAL]
case refine'_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s
case refine'_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }),
    ↑?refine'_1 a ∈ fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
[PROOFSTEP]
use fun t => (↑) ⁻¹' t.1
[GOAL]
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
⊢ Injective fun t => Subtype.val ⁻¹' ↑t
[PROOFSTEP]
rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h
[GOAL]
case inj'.mk.intro.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ #↑t ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ #↑t' ≤ c) }
⊢ { val := t, property := (_ : t ⊆ s ∧ #↑t ≤ c) } = { val := t', property := (_ : t' ⊆ s ∧ #↑t' ≤ c) }
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ #↑t ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ #↑t' ≤ c) }
⊢ ↑{ val := t, property := (_ : t ⊆ s ∧ #↑t ≤ c) } = ↑{ val := t', property := (_ : t' ⊆ s ∧ #↑t' ≤ c) }
[PROOFSTEP]
dsimp only at h ⊢
[GOAL]
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t = t'
[PROOFSTEP]
refine' (preimage_eq_preimage' _ _).1 h
[GOAL]
case inj'.mk.intro.mk.intro.a.refine'_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ range Subtype.val
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
case inj'.mk.intro.mk.intro.a.refine'_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ range Subtype.val
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
case inj'.mk.intro.mk.intro.a.refine'_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s
[PROOFSTEP]
assumption
[GOAL]
case inj'.mk.intro.mk.intro.a.refine'_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }),
    ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t,
            inj' :=
              (_ :
                ∀ ⦃a₁ a₂ : { t // t ⊆ s ∧ #↑t ≤ c }⦄,
                  (fun t => Subtype.val ⁻¹' ↑t) a₁ = (fun t => Subtype.val ⁻¹' ↑t) a₂ → a₁ = a₂) }
        a ∈
      fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
[PROOFSTEP]
rintro ⟨t, _, h2t⟩
[GOAL]
case refine'_2.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left✝ : t ⊆ s
h2t : #↑t ≤ c
⊢ ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : { t // t ⊆ s ∧ #↑t ≤ c }⦄,
                (fun t => Subtype.val ⁻¹' ↑t) a₁ = (fun t => Subtype.val ⁻¹' ↑t) a₂ → a₁ = a₂) }
      { val := t, property := (_ : t ⊆ s ∧ #↑t ≤ c) } ∈
    fun t =>
    Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b)) c
[PROOFSTEP]
exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t
[GOAL]
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑sᶜ = #α
[PROOFSTEP]
refine' eq_of_add_eq_of_aleph0_le _ h2 (aleph0_le_mk α)
[GOAL]
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑s + #↑sᶜ = #α
[PROOFSTEP]
exact mk_sum_compl s
[GOAL]
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑(↑s)ᶜ = #α
[PROOFSTEP]
apply mk_compl_of_infinite
[GOAL]
case h2
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑↑s < #α
[PROOFSTEP]
exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)
[GOAL]
α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #↑sᶜ = #↑tᶜ
[PROOFSTEP]
rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]
[GOAL]
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift #α = lift #β
h2 : lift #↑s = lift #↑t
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift #α = lift #β
h2 : lift #↑s = lift #↑t
val✝ : Fintype α
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
rcases lift_mk_eq.{u, v, w}.1 h1 with ⟨e⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift #α = lift #β
h2 : lift #↑s = lift #↑t
val✝ : Fintype α
e : α ≃ β
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
letI : Fintype β := Fintype.ofEquiv α e
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift #α = lift #β
h2 : lift #↑s = lift #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift #↑s = lift #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
classical
lift s to Finset α using s.toFinite
lift t to Finset β using t.toFinite
simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl, lift_natCast, Nat.cast_inj, h1,
  h2]
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift #↑s = lift #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
lift s to Finset α using s.toFinite
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
t : Set β
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
h2 : lift #↑↑s = lift #↑t
⊢ lift #↑(↑s)ᶜ = lift #↑tᶜ
[PROOFSTEP]
lift t to Finset β using t.toFinite
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : lift #↑↑s = lift #↑↑t
⊢ lift #↑(↑s)ᶜ = lift #↑(↑t)ᶜ
[PROOFSTEP]
simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : Finset.card s = Finset.card t
⊢ lift #↑(↑s)ᶜ = lift #↑(↑t)ᶜ
[PROOFSTEP]
simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl, lift_natCast, Nat.cast_inj, h1,
  h2]
[GOAL]
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑sᶜ = #↑tᶜ
[PROOFSTEP]
rw [← lift_inj.{u, max u v}]
[GOAL]
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift #↑sᶜ = lift #↑tᶜ
[PROOFSTEP]
apply mk_compl_eq_mk_compl_finite_lift.{u, u, max u v}
[GOAL]
case h1
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift #α = lift #β
[PROOFSTEP]
rwa [lift_inj]
[GOAL]
case h2
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift #↑s = lift #↑t
[PROOFSTEP]
rwa [lift_inj]
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
have := h
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h this : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
cases' this with g
[GOAL]
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ↑f)ᶜ
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
let h : α ≃ β :=
  (Set.sumCompl (s : Set α)).symm.trans ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
[GOAL]
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ↑f)ᶜ
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
refine' ⟨h, _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ↑f)ᶜ
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∀ (x : ↑s), ↑h ↑x = ↑f x
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ↑f)ᶜ
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
x : α
hx : x ∈ s
⊢ ↑h ↑{ val := x, property := hx } = ↑f { val := x, property := hx }
[PROOFSTEP]
simp [Set.sumCompl_symm_apply_of_mem, hx]
[GOAL]
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
apply extend_function.{v, u} f
[GOAL]
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
cases' id h with g
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
rw [← lift_mk_eq.{u, v, max u v}] at h
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift #α = lift #β
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
rw [← lift_mk_eq.{u, v, max u v}, mk_compl_eq_mk_compl_finite_lift.{u, v, max u v} h]
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift #α = lift #β
g : α ≃ β
⊢ lift #↑s = lift #↑(range ↑f)
[PROOFSTEP]
rw [mk_range_eq_lift.{u, v, max u v}]
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift #α = lift #β
g : α ≃ β
⊢ Injective ↑f
[PROOFSTEP]
exact f.2
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
cases fintypeOrInfinite α
[GOAL]
case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
exact extend_function_finite f h
[GOAL]
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
[PROOFSTEP]
apply extend_function f
[GOAL]
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
cases' id h with g
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
haveI := Infinite.of_injective _ g.injective
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑sᶜ ≃ ↑(range ↑f)ᶜ)
[PROOFSTEP]
rw [← lift_mk_eq'] at h ⊢
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift #α = lift #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift #↑sᶜ = lift #↑(range ↑f)ᶜ
[PROOFSTEP]
rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
[GOAL]
case inr.intro.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift #α = lift #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ↑f) < #β
[PROOFSTEP]
rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]