import data.fintype.big_operators

import data.finsupp.defs

import data.nat.part_enat

import data.set.countable

import logic.small.basic

import order.conditionally_complete_lattice.basic

import order.succ_pred.limit

import set_theory.cardinal.schroeder_bernstein

import tactic.positivity

open function set order

open_locale big_operators classical

noncomputable theory

universes u v w

variables {α β : Type u}

instance cardinal.is_equivalent : setoid (Type u) :=

{ r := λ α β, nonempty (α ≃ β),

iseqv := ⟨λ α,

⟨equiv.refl α⟩,

λ α β ⟨e⟩, ⟨e.symm⟩,

λ α β γ ⟨e₁⟩ ⟨e₂⟩, ⟨e₁.trans e₂⟩⟩ }

def cardinal : Type (u + 1) := quotient cardinal.is_equivalent

namespace cardinal

def mk : Type u → cardinal := quotient.mk

localized "prefix (name := cardinal.mk) `#` := cardinal.mk" in cardinal

instance can_lift_cardinal_Type : can_lift cardinal.{u} (Type u) mk (λ _, true) :=

⟨λ c _, quot.induction_on c $ λ α, ⟨α, rfl⟩⟩

lemma induction_on {p : cardinal → Prop} (c : cardinal) (h : ∀ α, p (#α)) : p c :=

quotient.induction_on c h

lemma induction_on₂ {p : cardinal → cardinal → Prop} (c₁ : cardinal) (c₂ : cardinal)

(h : ∀ α β, p (#α) (#β)) : p c₁ c₂ :=

quotient.induction_on₂ c₁ c₂ h

lemma induction_on₃ {p : cardinal → cardinal → cardinal → Prop} (c₁ : cardinal) (c₂ : cardinal)

(c₃ : cardinal) (h : ∀ α β γ, p (#α) (#β) (#γ)) : p c₁ c₂ c₃ :=

quotient.induction_on₃ c₁ c₂ c₃ h

protected lemma eq : #α = #β ↔ nonempty (α ≃ β) := quotient.eq

@[simp] theorem mk_def (α : Type u) : @eq cardinal ⟦α⟧ (#α) := rfl

@[simp] theorem mk_out (c : cardinal) : #(c.out) = c := quotient.out_eq _

def out_mk_equiv {α : Type v} : (#α).out ≃ α :=

nonempty.some $ cardinal.eq.mp (by simp)

lemma mk_congr (e : α ≃ β) : # α = # β := quot.sound ⟨e⟩

alias mk_congr ← _root_.equiv.cardinal_eq

def map (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) :

cardinal.{u} → cardinal.{v} :=

quotient.map f (λ α β ⟨e⟩, ⟨hf α β e⟩)

@[simp] lemma map_mk (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) (α : Type u) :

map f hf (#α) = #(f α) := rfl

def map₂ (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :

cardinal.{u} → cardinal.{v} → cardinal.{w} :=

quotient.map₂ f $ λ α β ⟨e₁⟩ γ δ ⟨e₂⟩, ⟨hf α β γ δ e₁ e₂⟩

def lift (c : cardinal.{v}) : cardinal.{max v u} :=

map ulift (λ α β e, equiv.ulift.trans $ e.trans equiv.ulift.symm) c

@[simp] theorem mk_ulift (α) : #(ulift.{v u} α) = lift.{v} (#α) := rfl

@[simp] theorem lift_umax : lift.{(max u v) u} = lift.{v u} :=

funext $ λ a, induction_on a $ λ α, (equiv.ulift.trans equiv.ulift.symm).cardinal_eq

@[simp] theorem lift_umax' : lift.{(max v u) u} = lift.{v u} := lift_umax

@[simp] theorem lift_id' (a : cardinal.{max u v}) : lift.{u} a = a :=

induction_on a $ λ α, mk_congr equiv.ulift

@[simp] theorem lift_id (a : cardinal) : lift.{u u} a = a := lift_id'.{u u} a

@[simp] theorem lift_uzero (a : cardinal.{u}) : lift.{0} a = a := lift_id'.{0 u} a

@[simp] theorem lift_lift (a : cardinal) :

lift.{w} (lift.{v} a) = lift.{max v w} a :=

induction_on a $ λ α,

(equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm).cardinal_eq

instance : has_le cardinal.{u} :=

⟨λ q₁ q₂, quotient.lift_on₂ q₁ q₂ (λ α β, nonempty $ α ↪ β) $

λ α β γ δ ⟨e₁⟩ ⟨e₂⟩, propext ⟨λ ⟨e⟩, ⟨e.congr e₁ e₂⟩, λ ⟨e⟩, ⟨e.congr e₁.symm e₂.symm⟩⟩⟩

instance : partial_order cardinal.{u} :=

{ le := (≤),

le_refl := by rintros ⟨α⟩; exact ⟨embedding.refl _⟩,

le_trans := by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.trans e₂⟩,

le_antisymm := by { rintros ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩, exact quotient.sound (e₁.antisymm e₂) }, }

instance : linear_order cardinal.{u} :=

{ le_total := by { rintros ⟨α⟩ ⟨β⟩, apply embedding.total },

decidable_le := classical.dec_rel _,

..cardinal.partial_order.{u}, }

theorem le_def (α β : Type u) : #α ≤ #β ↔ nonempty (α ↪ β) :=

iff.rfl

theorem mk_le_of_injective {α β : Type u} {f : α → β} (hf : injective f) : #α ≤ #β :=

⟨⟨f, hf⟩⟩

theorem _root_.function.embedding.cardinal_le {α β : Type u} (f : α ↪ β) : #α ≤ #β := ⟨f⟩

theorem mk_le_of_surjective {α β : Type u} {f : α → β} (hf : surjective f) : #β ≤ #α :=

⟨embedding.of_surjective f hf⟩

theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} :

c ≤ #α ↔ ∃ p : set α, #p = c :=

⟨induction_on c $ λ β ⟨⟨f, hf⟩⟩,

⟨set.range f, (equiv.of_injective f hf).cardinal_eq.symm⟩,

λ ⟨p, e⟩, e ▸ ⟨⟨subtype.val, λ a b, subtype.eq⟩⟩⟩

theorem mk_subtype_le {α : Type u} (p : α → Prop) : #(subtype p) ≤ #α :=

⟨embedding.subtype p⟩

theorem mk_set_le (s : set α) : #s ≤ #α :=

mk_subtype_le s

theorem out_embedding {c c' : cardinal} : c ≤ c' ↔ nonempty (c.out ↪ c'.out) :=

by { transitivity _, rw [←quotient.out_eq c, ←quotient.out_eq c'], refl }

theorem lift_mk_le {α : Type u} {β : Type v} :

lift.{max v w} (#α) ≤ lift.{max u w} (#β) ↔ nonempty (α ↪ β) :=

⟨λ ⟨f⟩, ⟨embedding.congr equiv.ulift equiv.ulift f⟩,

λ ⟨f⟩, ⟨embedding.congr equiv.ulift.symm equiv.ulift.symm f⟩⟩

theorem lift_mk_le' {α : Type u} {β : Type v} :

lift.{v} (#α) ≤ lift.{u} (#β) ↔ nonempty (α ↪ β) :=

lift_mk_le.{u v 0}

theorem lift_mk_eq {α : Type u} {β : Type v} :

lift.{max v w} (#α) = lift.{max u w} (#β) ↔ nonempty (α ≃ β) :=

quotient.eq.trans

⟨λ ⟨f⟩, ⟨equiv.ulift.symm.trans $ f.trans equiv.ulift⟩,

λ ⟨f⟩, ⟨equiv.ulift.trans $ f.trans equiv.ulift.symm⟩⟩

theorem lift_mk_eq' {α : Type u} {β : Type v} :

lift.{v} (#α) = lift.{u} (#β) ↔ nonempty (α ≃ β) :=

lift_mk_eq.{u v 0}

@[simp] theorem lift_le {a b : cardinal} : lift a ≤ lift b ↔ a ≤ b :=

induction_on₂ a b $ λ α β, by { rw ← lift_umax, exact lift_mk_le }

@[simps { fully_applied := ff }] def lift_order_embedding : cardinal.{v} ↪o cardinal.{max v u} :=

order_embedding.of_map_le_iff lift (λ _ _, lift_le)

theorem lift_injective : injective lift.{u v} := lift_order_embedding.injective

@[simp] theorem lift_inj {a b : cardinal} : lift a = lift b ↔ a = b :=

lift_injective.eq_iff

@[simp] theorem lift_lt {a b : cardinal} : lift a < lift b ↔ a < b :=

lift_order_embedding.lt_iff_lt

theorem lift_strict_mono : strict_mono lift :=

λ a b, lift_lt.2

theorem lift_monotone : monotone lift :=

lift_strict_mono.monotone

instance : has_zero cardinal.{u} := ⟨#pempty⟩

instance : inhabited cardinal.{u} := ⟨0⟩

lemma mk_eq_zero (α : Type u) [is_empty α] : #α = 0 :=

(equiv.equiv_pempty α).cardinal_eq

@[simp] theorem lift_zero : lift 0 = 0 := mk_congr (equiv.equiv_pempty _)

@[simp] theorem lift_eq_zero {a : cardinal.{v}} : lift.{u} a = 0 ↔ a = 0 :=

lift_injective.eq_iff' lift_zero

lemma mk_eq_zero_iff {α : Type u} : #α = 0 ↔ is_empty α :=

⟨λ e, let ⟨h⟩ := quotient.exact e in h.is_empty, @mk_eq_zero α⟩

theorem mk_ne_zero_iff {α : Type u} : #α ≠ 0 ↔ nonempty α :=

(not_iff_not.2 mk_eq_zero_iff).trans not_is_empty_iff

@[simp] lemma mk_ne_zero (α : Type u) [nonempty α] : #α ≠ 0 := mk_ne_zero_iff.2 ‹_›

instance : has_one cardinal.{u} := ⟨#punit⟩

instance : nontrivial cardinal.{u} := ⟨⟨1, 0, mk_ne_zero _⟩⟩

lemma mk_eq_one (α : Type u) [unique α] : #α = 1 :=

(equiv.equiv_punit α).cardinal_eq

theorem le_one_iff_subsingleton {α : Type u} : #α ≤ 1 ↔ subsingleton α :=

⟨λ ⟨f⟩, ⟨λ a b, f.injective (subsingleton.elim _ _)⟩,

λ ⟨h⟩, ⟨⟨λ a, punit.star, λ a b _, h _ _⟩⟩⟩

@[simp] lemma mk_le_one_iff_set_subsingleton {s : set α} : #s ≤ 1 ↔ s.subsingleton :=

le_one_iff_subsingleton.trans s.subsingleton_coe

alias mk_le_one_iff_set_subsingleton ↔ _ _root_.set.subsingleton.cardinal_mk_le_one

instance : has_add cardinal.{u} := ⟨map₂ sum $ λ α β γ δ, equiv.sum_congr⟩

theorem add_def (α β : Type u) : #α + #β = #(α ⊕ β) := rfl

instance : has_nat_cast cardinal.{u} := ⟨nat.unary_cast⟩

@[simp] lemma mk_sum (α : Type u) (β : Type v) :

#(α ⊕ β) = lift.{v u} (#α) + lift.{u v} (#β) :=

mk_congr ((equiv.ulift).symm.sum_congr (equiv.ulift).symm)

@[simp] theorem mk_option {α : Type u} : #(option α) = #α + 1 :=

(equiv.option_equiv_sum_punit α).cardinal_eq

@[simp] lemma mk_psum (α : Type u) (β : Type v) : #(psum α β) = lift.{v} (#α) + lift.{u} (#β) :=

(mk_congr (equiv.psum_equiv_sum α β)).trans (mk_sum α β)

@[simp] lemma mk_fintype (α : Type u) [fintype α] : #α = fintype.card α :=

refine fintype.induction_empty_option _ _ _ α,

{ introsI α β h e hα, letI := fintype.of_equiv β e.symm,

rwa [mk_congr e, fintype.card_congr e] at hα },

{ refl },

{ introsI α h hα, simp [hα], refl }

instance : has_mul cardinal.{u} := ⟨map₂ prod $ λ α β γ δ, equiv.prod_congr⟩

theorem mul_def (α β : Type u) : #α * #β = #(α × β) := rfl

@[simp] lemma mk_prod (α : Type u) (β : Type v) :

#(α × β) = lift.{v u} (#α) * lift.{u v} (#β) :=

mk_congr (equiv.ulift.symm.prod_congr (equiv.ulift).symm)

private theorem mul_comm' (a b : cardinal.{u}) : a * b = b * a :=

induction_on₂ a b $ λ α β, mk_congr $ equiv.prod_comm α β

instance : has_pow cardinal.{u} cardinal.{u} :=

⟨map₂ (λ α β, β → α) (λ α β γ δ e₁ e₂, e₂.arrow_congr e₁)⟩

local infixr (name := cardinal.pow) ^ := @has_pow.pow cardinal cardinal cardinal.has_pow

local infixr (name := cardinal.pow.nat) ` ^ℕ `:80 := @has_pow.pow cardinal ℕ monoid.has_pow

theorem power_def (α β) : #α ^ #β = #(β → α) := rfl

theorem mk_arrow (α : Type u) (β : Type v) : #(α → β) = lift.{u} (#β) ^ lift.{v} (#α) :=

mk_congr (equiv.ulift.symm.arrow_congr equiv.ulift.symm)

@[simp] theorem lift_power (a b) : lift (a ^ b) = lift a ^ lift b :=

induction_on₂ a b $ λ α β,

mk_congr $ equiv.ulift.trans (equiv.ulift.arrow_congr equiv.ulift).symm

@[simp] theorem power_zero {a : cardinal} : a ^ 0 = 1 :=

induction_on a $ λ α, mk_congr $ equiv.pempty_arrow_equiv_punit α

@[simp] theorem power_one {a : cardinal} : a ^ 1 = a :=

induction_on a $ λ α, mk_congr $ equiv.punit_arrow_equiv α

theorem power_add {a b c : cardinal} : a ^ (b + c) = a ^ b * a ^ c :=

induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.sum_arrow_equiv_prod_arrow β γ α

instance : comm_semiring cardinal.{u} :=

{ zero := 0,

one := 1,

add := (+),

mul := (*),

zero_add := λ a, induction_on a $ λ α, mk_congr $ equiv.empty_sum pempty α,

add_zero := λ a, induction_on a $ λ α, mk_congr $ equiv.sum_empty α pempty,

add_assoc := λ a b c, induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.sum_assoc α β γ,

add_comm := λ a b, induction_on₂ a b $ λ α β, mk_congr $ equiv.sum_comm α β,

zero_mul := λ a, induction_on a $ λ α, mk_congr $ equiv.pempty_prod α,

mul_zero := λ a, induction_on a $ λ α, mk_congr $ equiv.prod_pempty α,

one_mul := λ a, induction_on a $ λ α, mk_congr $ equiv.punit_prod α,

mul_one := λ a, induction_on a $ λ α, mk_congr $ equiv.prod_punit α,

mul_assoc := λ a b c, induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.prod_assoc α β γ,

mul_comm := mul_comm',

left_distrib := λ a b c, induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.prod_sum_distrib α β γ,

right_distrib := λ a b c, induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.sum_prod_distrib α β γ,

npow := λ n c, c ^ n,

npow_zero' := @power_zero,

npow_succ' := λ n c, show c ^ (n + 1) = c * c ^ n, by rw [power_add, power_one, mul_comm'] }

theorem power_bit0 (a b : cardinal) : a ^ (bit0 b) = a ^ b * a ^ b :=

power_add

theorem power_bit1 (a b : cardinal) : a ^ (bit1 b) = a ^ b * a ^ b * a :=

by rw [bit1, ←power_bit0, power_add, power_one]

@[simp] theorem one_power {a : cardinal} : 1 ^ a = 1 :=

induction_on a $ λ α, (equiv.arrow_punit_equiv_punit α).cardinal_eq

@[simp] theorem mk_bool : #bool = 2 := by simp

@[simp] theorem mk_Prop : #(Prop) = 2 := by simp

@[simp] theorem zero_power {a : cardinal} : a ≠ 0 → 0 ^ a = 0 :=

induction_on a $ λ α heq, mk_eq_zero_iff.2 $ is_empty_pi.2 $

let ⟨a⟩ := mk_ne_zero_iff.1 heq in ⟨a, pempty.is_empty⟩

theorem power_ne_zero {a : cardinal} (b) : a ≠ 0 → a ^ b ≠ 0 :=

induction_on₂ a b $ λ α β h,

let ⟨a⟩ := mk_ne_zero_iff.1 h in mk_ne_zero_iff.2 ⟨λ _, a⟩

theorem mul_power {a b c : cardinal} : (a * b) ^ c = a ^ c * b ^ c :=

induction_on₃ a b c $ λ α β γ, mk_congr $ equiv.arrow_prod_equiv_prod_arrow α β γ

theorem power_mul {a b c : cardinal} : a ^ (b * c) = (a ^ b) ^ c :=

by { rw [mul_comm b c], exact induction_on₃ a b c (λ α β γ, mk_congr $ equiv.curry γ β α) }

@[simp] lemma pow_cast_right (a : cardinal.{u}) (n : ℕ) : (a ^ (↑n : cardinal.{u})) = a ^ℕ n :=

rfl

@[simp] theorem lift_one : lift 1 = 1 :=

mk_congr $ equiv.ulift.trans equiv.punit_equiv_punit

@[simp] theorem lift_add (a b) : lift (a + b) = lift a + lift b :=

induction_on₂ a b $ λ α β,

mk_congr $ equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm

@[simp] theorem lift_mul (a b) : lift (a * b) = lift a * lift b :=

induction_on₂ a b $ λ α β,

mk_congr $ equiv.ulift.trans (equiv.prod_congr equiv.ulift equiv.ulift).symm

@[simp] theorem lift_bit0 (a : cardinal) : lift (bit0 a) = bit0 (lift a) :=

lift_add a a

@[simp] theorem lift_bit1 (a : cardinal) : lift (bit1 a) = bit1 (lift a) :=

by simp [bit1]

theorem lift_two : lift.{u v} 2 = 2 := by simp

@[simp] theorem mk_set {α : Type u} : #(set α) = 2 ^ #α := by simp [set, mk_arrow]

@[simp] theorem mk_powerset {α : Type u} (s : set α) : #↥(𝒫 s) = 2 ^ #↥s :=

(mk_congr (equiv.set.powerset s)).trans mk_set

theorem lift_two_power (a) : lift (2 ^ a) = 2 ^ lift a := by simp

section order_properties

open sum

protected theorem zero_le : ∀ a : cardinal, 0 ≤ a :=

by rintro ⟨α⟩; exact ⟨embedding.of_is_empty⟩

private theorem add_le_add' : ∀ {a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=

by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.sum_map e₂⟩

instance add_covariant_class : covariant_class cardinal cardinal (+) (≤) :=

⟨λ a b c, add_le_add' le_rfl⟩

instance add_swap_covariant_class : covariant_class cardinal cardinal (swap (+)) (≤) :=

⟨λ a b c h, add_le_add' h le_rfl⟩

instance : canonically_ordered_comm_semiring cardinal.{u} :=

{ bot := 0,

bot_le := cardinal.zero_le,

add_le_add_left := λ a b, add_le_add_left,

exists_add_of_le := λ a b, induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,

have (α ⊕ ((range f)ᶜ : set β)) ≃ β, from

(equiv.sum_congr (equiv.of_injective f hf) (equiv.refl _)).trans $

(equiv.set.sum_compl (range f)),

⟨#↥(range f)ᶜ, mk_congr this.symm⟩,

le_self_add := λ a b, (add_zero a).ge.trans $ add_le_add_left (cardinal.zero_le _) _,

eq_zero_or_eq_zero_of_mul_eq_zero := λ a b, induction_on₂ a b $ λ α β,

by simpa only [mul_def, mk_eq_zero_iff, is_empty_prod] using id,

..cardinal.comm_semiring, ..cardinal.partial_order }

instance : canonically_linear_ordered_add_monoid cardinal.{u} :=

{ ..cardinal.canonically_ordered_comm_semiring,

..cardinal.linear_order }

instance : canonically_ordered_add_monoid cardinal.{u} :=

{ ..cardinal.canonically_ordered_comm_semiring }

instance : linear_ordered_comm_monoid_with_zero cardinal.{u} :=

{ mul_le_mul_left := @mul_le_mul_left' _ _ _ _,

zero_le_one := zero_le _,

..cardinal.comm_semiring,

..cardinal.linear_order }

instance : comm_monoid_with_zero cardinal.{u} :=

{ ..cardinal.canonically_ordered_comm_semiring }

lemma zero_power_le (c : cardinal.{u}) : (0 : cardinal.{u}) ^ c ≤ 1 :=

by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }

theorem power_le_power_left : ∀ {a b c : cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=

by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩; exact

let ⟨a⟩ := mk_ne_zero_iff.1 hα in

⟨@embedding.arrow_congr_left _ _ _ ⟨a⟩ e⟩

theorem self_le_power (a : cardinal) {b : cardinal} (hb : 1 ≤ b) : a ≤ a ^ b :=

rcases eq_or_ne a 0 with rfl|ha,

{ exact zero_le _ },

{ convert power_le_power_left ha hb, exact power_one.symm }

theorem cantor (a : cardinal.{u}) : a < 2 ^ a :=

induction a using cardinal.induction_on with α,

rw [← mk_set],

refine ⟨⟨⟨singleton, λ a b, singleton_eq_singleton_iff.1⟩⟩, _⟩,

rintro ⟨⟨f, hf⟩⟩,

exact cantor_injective f hf

instance : no_max_order cardinal.{u} :=

{ exists_gt := λ a, ⟨_, cantor a⟩ }

instance : distrib_lattice cardinal.{u} := by apply_instance

theorem one_lt_iff_nontrivial {α : Type u} : 1 < #α ↔ nontrivial α :=

by rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, not_not]

theorem power_le_max_power_one {a b c : cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1 :=

by_cases ha : a = 0,

simp [ha, zero_power_le],

exact (power_le_power_left ha h).trans (le_max_left _ _)

theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=

induction_on₃ a b c $ λ α β γ ⟨e⟩, ⟨embedding.arrow_congr_right e⟩

theorem power_pos {a : cardinal} (b) (ha : 0 < a) : 0 < a ^ b := (power_ne_zero _ ha.ne').bot_lt

end order_properties

protected theorem lt_wf : @well_founded cardinal.{u} (<) :=

⟨λ a, classical.by_contradiction $ λ h, begin

let ι := {c : cardinal // ¬ acc (<) c},

let f : ι → cardinal := subtype.val,

haveI hι : nonempty ι := ⟨⟨_, h⟩⟩,

obtain ⟨⟨c : cardinal, hc : ¬acc (<) c⟩, ⟨h_1 : Π j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=

embedding.min_injective (λ i, (f i).out),

apply hc (acc.intro _ (λ j h', classical.by_contradiction (λ hj, h'.2 _))),

have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩,

simpa only [f, mk_out] using this

end⟩

instance : has_well_founded cardinal.{u} := ⟨(<), cardinal.lt_wf⟩

instance wo : @is_well_order cardinal.{u} (<) := { }

instance : conditionally_complete_linear_order_bot cardinal :=

is_well_order.conditionally_complete_linear_order_bot _

@[simp] theorem Inf_empty : Inf (∅ : set cardinal.{u}) = 0 :=

dif_neg not_nonempty_empty

instance : succ_order cardinal :=

succ_order.of_succ_le_iff (λ c, Inf {c' | c < c'})

(λ a b, ⟨lt_of_lt_of_le $ Inf_mem $ exists_gt a, cInf_le'⟩)

theorem succ_def (c : cardinal) : succ c = Inf {c' | c < c'} := rfl

lemma succ_pos : ∀ c : cardinal, 0 < succ c := bot_lt_succ

lemma succ_ne_zero (c : cardinal) : succ c ≠ 0 := (succ_pos _).ne'

theorem add_one_le_succ (c : cardinal.{u}) : c + 1 ≤ succ c :=

refine (le_cInf_iff'' (exists_gt c)).2 (λ b hlt, _),

rcases ⟨b, c⟩ with ⟨⟨β⟩, ⟨γ⟩⟩,

cases le_of_lt hlt with f,

have : ¬ surjective f := λ hn, (not_le_of_lt hlt) (mk_le_of_surjective hn),

simp only [surjective, not_forall] at this,

rcases this with ⟨b, hb⟩,

calc #γ + 1 = #(option γ) : mk_option.symm

... ≤ #β : (f.option_elim b hb).cardinal_le

def is_limit (c : cardinal) : Prop := c ≠ 0 ∧ is_succ_limit c

protected theorem is_limit.ne_zero {c} (h : is_limit c) : c ≠ 0 := h.1

protected theorem is_limit.is_succ_limit {c} (h : is_limit c) : is_succ_limit c := h.2

theorem is_limit.succ_lt {x c} (h : is_limit c) : x < c → succ x < c := h.is_succ_limit.succ_lt

theorem is_succ_limit_zero : is_succ_limit (0 : cardinal) := is_succ_limit_bot

def sum {ι} (f : ι → cardinal) : cardinal := mk Σ i, (f i).out

theorem le_sum {ι} (f : ι → cardinal) (i) : f i ≤ sum f :=

by rw ← quotient.out_eq (f i); exact

⟨⟨λ a, ⟨i, a⟩, λ a b h, eq_of_heq $ by injection h⟩⟩

@[simp] theorem mk_sigma {ι} (f : ι → Type*) : #(Σ i, f i) = sum (λ i, #(f i)) :=

mk_congr $ equiv.sigma_congr_right $ λ i, out_mk_equiv.symm

@[simp] theorem sum_const (ι : Type u) (a : cardinal.{v}) :

sum (λ i : ι, a) = lift.{v} (#ι) * lift.{u} a :=

induction_on a $ λ α, mk_congr $

calc (Σ i : ι, quotient.out (#α)) ≃ ι × quotient.out (#α) : equiv.sigma_equiv_prod _ _

... ≃ ulift ι × ulift α : equiv.ulift.symm.prod_congr (out_mk_equiv.trans equiv.ulift.symm)

theorem sum_const' (ι : Type u) (a : cardinal.{u}) : sum (λ _:ι, a) = #ι * a := by simp

@[simp] theorem sum_add_distrib {ι} (f g : ι → cardinal) :

sum (f + g) = sum f + sum g :=

by simpa only [mk_sigma, mk_sum, mk_out, lift_id] using

mk_congr (equiv.sigma_sum_distrib (quotient.out ∘ f) (quotient.out ∘ g))

@[simp] theorem sum_add_distrib' {ι} (f g : ι → cardinal) :

cardinal.sum (λ i, f i + g i) = sum f + sum g :=

sum_add_distrib f g

@[simp] theorem lift_sum {ι : Type u} (f : ι → cardinal.{v}) :

cardinal.lift.{w} (cardinal.sum f) = cardinal.sum (λ i, cardinal.lift.{w} (f i)) :=

equiv.cardinal_eq $ equiv.ulift.trans $ equiv.sigma_congr_right $ λ a, nonempty.some $

by rw [←lift_mk_eq, mk_out, mk_out, lift_lift]

theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=

⟨(embedding.refl _).sigma_map $ λ i, classical.choice $

by have := H i; rwa [← quot.out_eq (f i), ← quot.out_eq (g i)] at this⟩

lemma mk_le_mk_mul_of_mk_preimage_le {c : cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' {b}) ≤ c) :

#α ≤ #β * c :=

by simpa only [←mk_congr (@equiv.sigma_fiber_equiv α β f), mk_sigma, ←sum_const']

using sum_le_sum _ _ hf

lemma lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : cardinal}

(f : α → β) (hf : ∀ b : β, lift.{v} #(f ⁻¹' {b}) ≤ c) :

lift.{v} #α ≤ lift.{u} #β * c :=

mk_le_mk_mul_of_mk_preimage_le (λ x : ulift.{v} α, ulift.up.{u} (f x.1)) $ ulift.forall.2 $ λ b,

(mk_congr $ (equiv.ulift.image _).trans (equiv.trans

(by { rw [equiv.image_eq_preimage], simp [set.preimage] }) equiv.ulift.symm)).trans_le (hf b)

theorem bdd_above_range {ι : Type u} (f : ι → cardinal.{max u v}) : bdd_above (set.range f) :=

⟨_, by { rintros a ⟨i, rfl⟩, exact le_sum f i }⟩

instance (a : cardinal.{u}) : small.{u} (set.Iic a) :=

rw ←mk_out a,

apply @small_of_surjective (set a.out) (Iic (#a.out)) _ (λ x, ⟨#x, mk_set_le x⟩),

rintro ⟨x, hx⟩,

simpa using le_mk_iff_exists_set.1 hx

instance (a : cardinal.{u}) : small.{u} (set.Iio a) :=

small_subset Iio_subset_Iic_self

theorem bdd_above_iff_small {s : set cardinal.{u}} : bdd_above s ↔ small.{u} s :=

⟨λ ⟨a, ha⟩, @small_subset _ (Iic a) s (λ x h, ha h) _, begin

rintro ⟨ι, ⟨e⟩⟩,

suffices : range (λ x : ι, (e.symm x).1) = s,

{ rw ←this,

apply bdd_above_range.{u u} },

ext x,

refine ⟨_, λ hx, ⟨e ⟨x, hx⟩, _⟩⟩,

{ rintro ⟨a, rfl⟩,

exact (e.symm a).prop },

{ simp_rw [subtype.val_eq_coe, equiv.symm_apply_apply], refl }

end⟩

theorem bdd_above_of_small (s : set cardinal.{u}) [h : small.{u} s] : bdd_above s :=

bdd_above_iff_small.2 h

theorem bdd_above_image (f : cardinal.{u} → cardinal.{max u v}) {s : set cardinal.{u}}

(hs : bdd_above s) : bdd_above (f '' s) :=

by { rw bdd_above_iff_small at hs ⊢, exactI small_lift _ }

theorem bdd_above_range_comp {ι : Type u} {f : ι → cardinal.{v}} (hf : bdd_above (range f))

(g : cardinal.{v} → cardinal.{max v w}) : bdd_above (range (g ∘ f)) :=

by { rw range_comp, exact bdd_above_image g hf }

theorem supr_le_sum {ι} (f : ι → cardinal) : supr f ≤ sum f :=

csupr_le' $ le_sum _

theorem sum_le_supr_lift {ι : Type u} (f : ι → cardinal.{max u v}) :

sum f ≤ (#ι).lift * supr f :=

rw [←(supr f).lift_id, ←lift_umax, lift_umax.{(max u v) u}, ←sum_const],

exact sum_le_sum _ _ (le_csupr $ bdd_above_range.{u v} f)

theorem sum_le_supr {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ #ι * supr f :=

by { rw ←lift_id (#ι), exact sum_le_supr_lift f }

theorem sum_nat_eq_add_sum_succ (f : ℕ → cardinal.{u}) :

cardinal.sum f = f 0 + cardinal.sum (λ i, f (i + 1)) :=

refine (equiv.sigma_nat_succ (λ i, quotient.out (f i))).cardinal_eq.trans _,

simp only [mk_sum, mk_out, lift_id, mk_sigma],

@[simp] protected theorem supr_of_empty {ι} (f : ι → cardinal) [is_empty ι] : supr f = 0 :=

csupr_of_empty f

@[simp] lemma lift_mk_shrink (α : Type u) [small.{v} α] :

cardinal.lift.{max u w} (# (shrink.{v} α)) = cardinal.lift.{max v w} (# α) :=

lift_mk_eq.2 ⟨(equiv_shrink α).symm⟩

@[simp] lemma lift_mk_shrink' (α : Type u) [small.{v} α] :

cardinal.lift.{u} (# (shrink.{v} α)) = cardinal.lift.{v} (# α) :=

lift_mk_shrink.{u v 0} α

@[simp] lemma lift_mk_shrink'' (α : Type (max u v)) [small.{v} α] :

cardinal.lift.{u} (# (shrink.{v} α)) = # α :=

by rw [← lift_umax', lift_mk_shrink.{(max u v) v 0} α, ← lift_umax, lift_id]

def prod {ι : Type u} (f : ι → cardinal) : cardinal := #(Π i, (f i).out)

@[simp] theorem mk_pi {ι : Type u} (α : ι → Type v) : #(Π i, α i) = prod (λ i, #(α i)) :=

mk_congr $ equiv.Pi_congr_right $ λ i, out_mk_equiv.symm

@[simp] theorem prod_const (ι : Type u) (a : cardinal.{v}) :

prod (λ i : ι, a) = lift.{u} a ^ lift.{v} (#ι) :=

induction_on a $ λ α, mk_congr $ equiv.Pi_congr equiv.ulift.symm $

λ i, out_mk_equiv.trans equiv.ulift.symm

theorem prod_const' (ι : Type u) (a : cardinal.{u}) : prod (λ _:ι, a) = a ^ #ι :=

induction_on a $ λ α, (mk_pi _).symm

theorem prod_le_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=

⟨embedding.Pi_congr_right $ λ i, classical.choice $

by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩

@[simp] theorem prod_eq_zero {ι} (f : ι → cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0 :=

by { lift f to ι → Type u using λ _, trivial, simp only [mk_eq_zero_iff, ← mk_pi, is_empty_pi] }

theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=

by simp [prod_eq_zero]

@[simp] theorem lift_prod {ι : Type u} (c : ι → cardinal.{v}) :

lift.{w} (prod c) = prod (λ i, lift.{w} (c i)) :=

lift c to ι → Type v using λ _, trivial,

simp only [← mk_pi, ← mk_ulift],

exact mk_congr (equiv.ulift.trans $ equiv.Pi_congr_right $ λ i, equiv.ulift.symm)

lemma prod_eq_of_fintype {α : Type u} [fintype α] (f : α → cardinal.{v}) :

prod f = cardinal.lift.{u} (∏ i, f i) :=

revert f,

refine fintype.induction_empty_option _ _ _ α,

{ introsI α β hβ e h f,

letI := fintype.of_equiv β e.symm,

rw [←e.prod_comp f, ←h],

exact mk_congr (e.Pi_congr_left _).symm },

{ intro f,

rw [fintype.univ_pempty, finset.prod_empty, lift_one, cardinal.prod, mk_eq_one] },

{ intros α hα h f,

rw [cardinal.prod, mk_congr equiv.pi_option_equiv_prod, mk_prod, lift_umax', mk_out,

←cardinal.prod, lift_prod, fintype.prod_option, lift_mul, ←h (λ a, f (some a))],

simp only [lift_id] },

@[simp] theorem lift_Inf (s : set cardinal) : lift (Inf s) = Inf (lift '' s) :=

rcases eq_empty_or_nonempty s with rfl | hs,

{ simp },

{ exact lift_monotone.map_Inf hs }

@[simp] theorem lift_infi {ι} (f : ι → cardinal) : lift (infi f) = ⨅ i, lift (f i) :=

by { unfold infi, convert lift_Inf (range f), rw range_comp }

theorem lift_down {a : cardinal.{u}} {b : cardinal.{max u v}} :

b ≤ lift a → ∃ a', lift a' = b :=

induction_on₂ a b $ λ α β,

by rw [← lift_id (#β), ← lift_umax, ← lift_umax.{u v}, lift_mk_le]; exact

λ ⟨f⟩, ⟨#(set.range f), eq.symm $ lift_mk_eq.2

⟨embedding.equiv_of_surjective

(embedding.cod_restrict _ f set.mem_range_self)

$ λ ⟨a, ⟨b, e⟩⟩, ⟨b, subtype.eq e⟩⟩⟩

theorem le_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :

b ≤ lift a ↔ ∃ a', lift a' = b ∧ a' ≤ a :=

⟨λ h, let ⟨a', e⟩ := lift_down h in ⟨a', e, lift_le.1 $ e.symm ▸ h⟩,

λ ⟨a', e, h⟩, e ▸ lift_le.2 h⟩

theorem lt_lift_iff {a : cardinal.{u}} {b : cardinal.{max u v}} :

b < lift a ↔ ∃ a', lift a' = b ∧ a' < a :=

⟨λ h, let ⟨a', e⟩ := lift_down h.le in ⟨a', e, lift_lt.1 $ e.symm ▸ h⟩,

λ ⟨a', e, h⟩, e ▸ lift_lt.2 h⟩

@[simp] theorem lift_succ (a) : lift (succ a) = succ (lift a) :=

le_antisymm

(le_of_not_gt $ λ h, begin

rcases lt_lift_iff.1 h with ⟨b, e, h⟩,

rw [lt_succ_iff, ← lift_le, e] at h,

exact h.not_lt (lt_succ _)

end)

(succ_le_of_lt $ lift_lt.2 $ lt_succ a)

@[simp] theorem lift_umax_eq {a : cardinal.{u}} {b : cardinal.{v}} :

lift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b :=

by rw [←lift_lift, ←lift_lift, lift_inj]

@[simp] theorem lift_min {a b : cardinal} : lift (min a b) = min (lift a) (lift b) :=

lift_monotone.map_min

@[simp] theorem lift_max {a b : cardinal} : lift (max a b) = max (lift a) (lift b) :=

lift_monotone.map_max

lemma lift_Sup {s : set cardinal} (hs : bdd_above s) : lift.{u} (Sup s) = Sup (lift.{u} '' s) :=

apply ((le_cSup_iff' (bdd_above_image _ hs)).2 (λ c hc, _)).antisymm (cSup_le' _),

{ by_contra h,

obtain ⟨d, rfl⟩ := cardinal.lift_down (not_le.1 h).le,

simp_rw lift_le at h hc,

rw cSup_le_iff' hs at h,

exact h (λ a ha, lift_le.1 $ hc (mem_image_of_mem _ ha)) },

{ rintros i ⟨j, hj, rfl⟩,

exact lift_le.2 (le_cSup hs hj) },

lemma lift_supr {ι : Type v} {f : ι → cardinal.{w}} (hf : bdd_above (range f)) :

lift.{u} (supr f) = ⨆ i, lift.{u} (f i) :=

by rw [supr, supr, lift_Sup hf, ←range_comp]

lemma lift_supr_le {ι : Type v} {f : ι → cardinal.{w}} {t : cardinal} (hf : bdd_above (range f))

(w : ∀ i, lift.{u} (f i) ≤ t) : lift.{u} (supr f) ≤ t :=

by { rw lift_supr hf, exact csupr_le' w }

@[simp] lemma lift_supr_le_iff {ι : Type v} {f : ι → cardinal.{w}} (hf : bdd_above (range f))

{t : cardinal} : lift.{u} (supr f) ≤ t ↔ ∀ i, lift.{u} (f i) ≤ t :=

by { rw lift_supr hf, exact csupr_le_iff' (bdd_above_range_comp hf _) }

universes v' w'

lemma lift_supr_le_lift_supr

{ι : Type v} {ι' : Type v'} {f : ι → cardinal.{w}} {f' : ι' → cardinal.{w'}}

(hf : bdd_above (range f)) (hf' : bdd_above (range f'))

{g : ι → ι'} (h : ∀ i, lift.{w'} (f i) ≤ lift.{w} (f' (g i))) :

lift.{w'} (supr f) ≤ lift.{w} (supr f') :=

rw [lift_supr hf, lift_supr hf'],

exact csupr_mono' (bdd_above_range_comp hf' _) (λ i, ⟨_, h i⟩)

lemma lift_supr_le_lift_supr'

{ι : Type v} {ι' : Type v'} {f : ι → cardinal.{v}} {f' : ι' → cardinal.{v'}}

(hf : bdd_above (range f)) (hf' : bdd_above (range f'))

(g : ι → ι') (h : ∀ i, lift.{v'} (f i) ≤ lift.{v} (f' (g i))) :

lift.{v'} (supr f) ≤ lift.{v} (supr f') :=

lift_supr_le_lift_supr hf hf' h

def aleph_0 : cardinal.{u} := lift (#ℕ)

localized "notation (name := cardinal.aleph_0) `ℵ₀` := cardinal.aleph_0" in cardinal

lemma mk_nat : #ℕ = ℵ₀ := (lift_id _).symm

theorem aleph_0_ne_zero : ℵ₀ ≠ 0 := mk_ne_zero _

theorem aleph_0_pos : 0 < ℵ₀ :=

pos_iff_ne_zero.2 aleph_0_ne_zero

@[simp] theorem lift_aleph_0 : lift ℵ₀ = ℵ₀ := lift_lift _

@[simp] theorem aleph_0_le_lift {c : cardinal.{u}} : ℵ₀ ≤ lift.{v} c ↔ ℵ₀ ≤ c :=

by rw [←lift_aleph_0, lift_le]

@[simp] theorem lift_le_aleph_0 {c : cardinal.{u}} : lift.{v} c ≤ ℵ₀ ↔ c ≤ ℵ₀ :=

by rw [←lift_aleph_0, lift_le]

@[simp] theorem aleph_0_lt_lift {c : cardinal.{u}} : ℵ₀ < lift.{v} c ↔ ℵ₀ < c :=

by rw [←lift_aleph_0, lift_lt]

@[simp] theorem lift_lt_aleph_0 {c : cardinal.{u}} : lift.{v} c < ℵ₀ ↔ c < ℵ₀ :=

by rw [←lift_aleph_0, lift_lt]

@[simp] theorem mk_fin (n : ℕ) : #(fin n) = n := by simp

@[simp] theorem lift_nat_cast (n : ℕ) : lift.{u} (n : cardinal.{v}) = n :=

by induction n; simp *

@[simp] lemma lift_eq_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{v} a = n ↔ a = n :=

lift_injective.eq_iff' (lift_nat_cast n)

@[simp] lemma nat_eq_lift_iff {n : ℕ} {a : cardinal.{u}} :

(n : cardinal) = lift.{v} a ↔ (n : cardinal) = a :=

by rw [←lift_nat_cast.{v} n, lift_inj]

@[simp] lemma lift_le_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{v} a ≤ n ↔ a ≤ n :=

by simp only [←lift_nat_cast, lift_le]

@[simp] lemma nat_le_lift_iff {n : ℕ} {a : cardinal.{u}} :

(n : cardinal) ≤ lift.{v} a ↔ (n : cardinal) ≤ a :=

by simp only [←lift_nat_cast, lift_le]

@[simp] lemma lift_lt_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{v} a < n ↔ a < n :=

by simp only [←lift_nat_cast, lift_lt]

@[simp] lemma nat_lt_lift_iff {n : ℕ} {a : cardinal.{u}} :

(n : cardinal) < lift.{v} a ↔ (n : cardinal) < a :=

by simp only [←lift_nat_cast, lift_lt]

theorem lift_mk_fin (n : ℕ) : lift (#(fin n)) = n := by simp

lemma mk_coe_finset {α : Type u} {s : finset α} : #s = ↑(finset.card s) := by simp

lemma mk_finset_of_fintype [fintype α] : #(finset α) = 2 ^ℕ fintype.card α := by simp

@[simp] lemma mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [fintype α] [has_zero β] :

#(α →₀ β) = lift.{u} (#β) ^ℕ fintype.card α :=

by simpa using (@finsupp.equiv_fun_on_finite α β _ _).cardinal_eq

lemma mk_finsupp_of_fintype (α β : Type u) [fintype α] [has_zero β] :

#(α →₀ β) = (#β) ^ℕ fintype.card α :=

by simp

theorem card_le_of_finset {α} (s : finset α) : (s.card : cardinal) ≤ #α :=

@mk_coe_finset _ s ▸ mk_set_le _

@[simp, norm_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=

by induction n; simp [pow_succ', power_add, *]

@[simp, norm_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=

by rw [← lift_mk_fin, ← lift_mk_fin, lift_le, le_def, function.embedding.nonempty_iff_card_le,

fintype.card_fin, fintype.card_fin]

@[simp, norm_cast] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=

by simp [lt_iff_le_not_le, ←not_le]

instance : char_zero cardinal := ⟨strict_mono.injective $ λ m n, nat_cast_lt.2⟩

theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n := nat.cast_inj

lemma nat_cast_injective : injective (coe : ℕ → cardinal) :=

nat.cast_injective

@[simp, norm_cast, priority 900] theorem nat_succ (n : ℕ) : (n.succ : cardinal) = succ n :=

(add_one_le_succ _).antisymm (succ_le_of_lt $ nat_cast_lt.2 $ nat.lt_succ_self _)

@[simp] theorem succ_zero : succ (0 : cardinal) = 1 := by norm_cast

theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : finset α, s.card ≤ n) : # α ≤ n :=

refine le_of_lt_succ (lt_of_not_ge $ λ hn, _),

rw [←cardinal.nat_succ, ←lift_mk_fin n.succ] at hn,

cases hn with f,

refine (H $ finset.univ.map f).not_lt _,

rw [finset.card_map, ←fintype.card, fintype.card_ulift, fintype.card_fin],

exact n.lt_succ_self

theorem cantor' (a) {b : cardinal} (hb : 1 < b) : a < b ^ a :=

rw [←succ_le_iff, (by norm_cast : succ (1 : cardinal) = 2)] at hb,

exact (cantor a).trans_le (power_le_power_right hb)

theorem one_le_iff_pos {c : cardinal} : 1 ≤ c ↔ 0 < c :=

by rw [←succ_zero, succ_le_iff]

theorem one_le_iff_ne_zero {c : cardinal} : 1 ≤ c ↔ c ≠ 0 :=

by rw [one_le_iff_pos, pos_iff_ne_zero]

theorem nat_lt_aleph_0 (n : ℕ) : (n : cardinal.{u}) < ℵ₀ :=