[GOAL]
α✝ β : Type u
α : Type v
⊢ #(Quotient.out #α) = #α
[PROOFSTEP]
simp
[GOAL]
α β : Type u
⊢ ∀ (a : Cardinal.{u}), a ≤ a
[PROOFSTEP]
rintro ⟨α⟩
[GOAL]
case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ Quot.mk Setoid.r α ≤ Quot.mk Setoid.r α
[PROOFSTEP]
exact ⟨Embedding.refl _⟩
[GOAL]
α β : Type u
⊢ ∀ (a b c : Cardinal.{u}), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩
[GOAL]
case mk.mk.mk.intro.intro
α✝ β✝ : Type u
a✝ : Cardinal.{u}
α : Type u
b✝ : Cardinal.{u}
β : Type u
c✝ : Cardinal.{u}
γ : Type u
e₁ : α ↪ β
e₂ : β ↪ γ
⊢ Quot.mk Setoid.r α ≤ Quot.mk Setoid.r γ
[PROOFSTEP]
exact ⟨e₁.trans e₂⟩
[GOAL]
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩
[GOAL]
case mk.mk.intro.intro
α✝ β✝ : Type u
a✝ : Cardinal.{u}
α : Type u
b✝ : Cardinal.{u}
β : Type u
e₁ : α ↪ β
e₂ : β ↪ α
⊢ Quot.mk Setoid.r α = Quot.mk Setoid.r β
[PROOFSTEP]
exact Quotient.sound (e₁.antisymm e₂)
[GOAL]
α β : Type u
src✝ : PartialOrder Cardinal.{u} := partialOrder
⊢ ∀ (a b : Cardinal.{u}), a ≤ b ∨ b ≤ a
[PROOFSTEP]
rintro ⟨α⟩ ⟨β⟩
[GOAL]
case mk.mk
α✝ β✝ : Type u
src✝ : PartialOrder Cardinal.{u} := partialOrder
a✝ : Cardinal.{u}
α : Type u
b✝ : Cardinal.{u}
β : Type u
⊢ Quot.mk Setoid.r α ≤ Quot.mk Setoid.r β ∨ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α
[PROOFSTEP]
apply Embedding.total
[GOAL]
α β : Type u
s : Set α
⊢ #↑(ULift.down ⁻¹' s) = lift #↑s
[PROOFSTEP]
rw [← mk_uLift, Cardinal.eq]
[GOAL]
α β : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift ↑s)
[PROOFSTEP]
constructor
[GOAL]
case val
α β : Type u
s : Set α
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift ↑s
[PROOFSTEP]
let f : ULift.down ⁻¹' s → ULift s := fun x ↦ ULift.up (restrictPreimage s ULift.down x)
[GOAL]
case val
α β : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift ↑s := fun x => { down := restrictPreimage s ULift.down x }
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift ↑s
[PROOFSTEP]
have : Function.Bijective f := ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))
[GOAL]
case val
α β : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift ↑s := fun x => { down := restrictPreimage s ULift.down x }
this : Bijective f
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift ↑s
[PROOFSTEP]
exact Equiv.ofBijective f this
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
⊢ c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')
[PROOFSTEP]
trans
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
⊢ c ≤ c' ↔ ?m.14684
[PROOFSTEP]
rw [← Quotient.out_eq c, ← Quotient.out_eq c']
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
⊢ Quotient.mk isEquivalent (Quotient.out c) ≤ Quotient.mk isEquivalent (Quotient.out c') ↔
    Nonempty (Quotient.out c ↪ Quotient.out c')
[PROOFSTEP]
rw [mk'_def, mk'_def, le_def]
[GOAL]
α✝ β✝ : Type u
a b : Cardinal.{v}
α β : Type v
⊢ lift #α ≤ lift #β ↔ #α ≤ #β
[PROOFSTEP]
rw [← lift_umax]
[GOAL]
α✝ β✝ : Type u
a b : Cardinal.{v}
α β : Type v
⊢ lift #α ≤ lift #β ↔ #α ≤ #β
[PROOFSTEP]
exact lift_mk_le.{u}
[GOAL]
α✝ β α : Type u
⊢ #(Option α) = #α + 1
[PROOFSTEP]
rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]
[GOAL]
α✝ β α : Type u
h : Fintype α
⊢ Fintype.card α = Fintype.card (ULift (Fin (Fintype.card α)))
[PROOFSTEP]
simp
[GOAL]
α β : Type u
n : ℕ
⊢ ↑(n + 1) = ↑n + 1
[PROOFSTEP]
change #(ULift.{u} (Fin (n + 1))) = #(ULift.{u} (Fin n)) + 1
[GOAL]
α β : Type u
n : ℕ
⊢ #(ULift (Fin (n + 1))) = #(ULift (Fin n)) + 1
[PROOFSTEP]
rw [← mk_option, mk_fintype, mk_fintype]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑(Fintype.card (ULift (Fin (n + 1)))) = ↑(Fintype.card (Option (ULift (Fin n))))
[PROOFSTEP]
simp only [Fintype.card_ulift, Fintype.card_fin, Fintype.card_option]
[GOAL]
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ ↑(n + 1) = c * c ^ ↑n
[PROOFSTEP]
rw [Cardinal.cast_succ, power_add, power_one, mul_comm']
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
⊢ a ^ bit1 b = a ^ b * a ^ b * a
[PROOFSTEP]
rw [bit1, ← power_bit0, power_add, power_one]
[GOAL]
α β : Type u
⊢ #Bool = 2
[PROOFSTEP]
simp
[GOAL]
α β : Type u
⊢ #Prop = 2
[PROOFSTEP]
simp
[GOAL]
α β : Type u
a b c : Cardinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
rw [mul_comm b c]
[GOAL]
α β : Type u
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c
[PROOFSTEP]
exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α
[GOAL]
α β : Type u
a : Cardinal.{u_1}
⊢ lift (bit1 a) = bit1 (lift a)
[PROOFSTEP]
simp [bit1]
[GOAL]
α β : Type u
⊢ lift 2 = 2
[PROOFSTEP]
simp [← one_add_one_eq_two]
[GOAL]
α✝ β α : Type u
⊢ #(Set α) = 2 ^ #α
[PROOFSTEP]
simp [← one_add_one_eq_two, Set, mk_arrow]
[GOAL]
α β : Type u
a : Cardinal.{u_1}
⊢ lift (2 ^ a) = 2 ^ lift a
[PROOFSTEP]
simp [← one_add_one_eq_two]
[GOAL]
α β : Type u
⊢ ∀ (a : Cardinal.{u_1}), 0 ≤ a
[PROOFSTEP]
rintro ⟨α⟩
[GOAL]
case mk
α✝ β : Type u
a✝ : Cardinal.{u_1}
α : Type u_1
⊢ 0 ≤ Quot.mk Setoid.r α
[PROOFSTEP]
exact ⟨Embedding.ofIsEmpty⟩
[GOAL]
α β : Type u
⊢ ∀ {a b c d : Cardinal.{u_1}}, a ≤ b → c ≤ d → a + c ≤ b + d
[PROOFSTEP]
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩
[GOAL]
case mk.mk.mk.mk.intro.intro
α✝ β✝ : Type u
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk Setoid.r α + Quot.mk Setoid.r γ ≤ Quot.mk Setoid.r β + Quot.mk Setoid.r δ
[PROOFSTEP]
exact
  ⟨e₁.sumMap e₂⟩
    -- #align cardinal.add_le_add' Cardinal.add_le_add'
[GOAL]
α✝ β✝ : Type u
src✝¹ : CommSemiring Cardinal.{u} := commSemiring
src✝ : PartialOrder Cardinal.{u} := partialOrder
a b : Cardinal.{u}
α β : Type u
⊢ #α * #β = 0 → #α = 0 ∨ #β = 0
[PROOFSTEP]
simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ 0 ^ c ≤ 1
[PROOFSTEP]
by_cases h : c = 0
[GOAL]
case pos
α β : Type u
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1
[PROOFSTEP]
rw [h, power_zero]
[GOAL]
case neg
α β : Type u
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1
[PROOFSTEP]
rw [zero_power h]
[GOAL]
case neg
α β : Type u
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1
[PROOFSTEP]
apply zero_le
[GOAL]
α β : Type u
⊢ ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c
[PROOFSTEP]
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩
[GOAL]
case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
[PROOFSTEP]
let ⟨a⟩ := mk_ne_zero_iff.1 hα
[GOAL]
case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
[PROOFSTEP]
exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ a ≤ a ^ b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α β : Type u
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
α β : Type u
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
[PROOFSTEP]
convert power_le_power_left ha hb
[GOAL]
case h.e'_3
α β : Type u
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1
[PROOFSTEP]
exact power_one.symm
[GOAL]
α β : Type u
a : Cardinal.{u}
⊢ a < 2 ^ a
[PROOFSTEP]
induction' a using Cardinal.inductionOn with α
[GOAL]
case h
α✝ β α : Type u
⊢ #α < 2 ^ #α
[PROOFSTEP]
rw [← mk_set]
[GOAL]
case h
α✝ β α : Type u
⊢ #α < #(Set α)
[PROOFSTEP]
refine' ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, _⟩
[GOAL]
case h
α✝ β α : Type u
⊢ ¬Quotient.liftOn₂ (#(Set α)) (#α) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
[PROOFSTEP]
rintro ⟨⟨f, hf⟩⟩
[GOAL]
case h.intro.mk
α✝ β α : Type u
f : Set α → α
hf : Injective f
⊢ False
[PROOFSTEP]
exact cantor_injective f hf
[GOAL]
α✝ β α : Type u
⊢ 1 < #α ↔ Nontrivial α
[PROOFSTEP]
rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]
[GOAL]
α β : Type u
a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^ b ≤ max (a ^ c) 1
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α β : Type u
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1
[PROOFSTEP]
simp [ha, zero_power_le]
[GOAL]
case neg
α β : Type u
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
[PROOFSTEP]
exact (power_le_power_left ha h).trans (le_max_left _ _)
[GOAL]
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
⊢ False
[PROOFSTEP]
let ι := { c : Cardinal // ¬Acc (· < ·) c }
[GOAL]
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (?u.61092 + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
⊢ False
[PROOFSTEP]
let f : ι → Cardinal := Subtype.val
[GOAL]
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (?u.61092 + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal.{?u.61092} := Subtype.val
⊢ False
[PROOFSTEP]
haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
[GOAL]
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
⊢ False
[PROOFSTEP]
obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
  Embedding.min_injective fun i => (f i).out
[GOAL]
case intro.mk.intro
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
⊢ False
[PROOFSTEP]
refine hc (Acc.intro _ fun j h' => byContradiction fun hj => h'.2 ?_)
[GOAL]
case intro.mk.intro
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
[PROOFSTEP]
have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
[GOAL]
case intro.mk.intro
α β : Type u
a : Cardinal.{u}
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
this : #(Quotient.out (f { val := c, property := hc })) ≤ #(Quotient.out (f { val := j, property := hj }))
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
[PROOFSTEP]
simpa only [mk_out] using this
[GOAL]
α β : Type u
a✝ b✝ : Cardinal.{?u.64039}
⊢ (fun c => sInf {c' | c < c'}) a✝ ≤ b✝ → a✝ < b✝
[PROOFSTEP]
apply lt_of_lt_of_le <| csInf_mem <| exists_gt _
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ c + 1 ≤ succ c
[PROOFSTEP]
have : Set.Nonempty {c' | c < c'} := exists_gt c
[GOAL]
α β : Type u
c : Cardinal.{u}
this : Set.Nonempty {c' | c < c'}
⊢ c + 1 ≤ succ c
[PROOFSTEP]
simp_rw [succ_def, le_csInf_iff'' this, mem_setOf]
[GOAL]
α β : Type u
c : Cardinal.{u}
this : Set.Nonempty {c' | c < c'}
⊢ ∀ (b : Cardinal.{u}), c < b → c + 1 ≤ b
[PROOFSTEP]
intro b hlt
[GOAL]
α β : Type u
c : Cardinal.{u}
this : Set.Nonempty {c' | c < c'}
b : Cardinal.{u}
hlt : c < b
⊢ c + 1 ≤ b
[PROOFSTEP]
rcases b, c with ⟨⟨β⟩, ⟨γ⟩⟩
[GOAL]
case mk.mk
α β✝ : Type u
c b : Cardinal.{u}
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
[PROOFSTEP]
cases' le_of_lt hlt with f
[GOAL]
case mk.mk.intro
α β✝ : Type u
c b : Cardinal.{u}
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
[PROOFSTEP]
have : ¬Surjective f := fun hn => (not_le_of_lt hlt) (mk_le_of_surjective hn)
[GOAL]
case mk.mk.intro
α β✝ : Type u
c b : Cardinal.{u}
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ¬Surjective ↑f
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
[PROOFSTEP]
simp only [Surjective, not_forall] at this 
[GOAL]
case mk.mk.intro
α β✝ : Type u
c b : Cardinal.{u}
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ∃ x, ¬∃ a, ↑f a = x
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
[PROOFSTEP]
rcases this with ⟨b, hb⟩
[GOAL]
case mk.mk.intro.intro
α β✝ : Type u
c b✝ : Cardinal.{u}
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
b : β
hb : ¬∃ a, ↑f a = b
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
[PROOFSTEP]
calc
  #γ + 1 = #(Option γ) := mk_option.symm
  _ ≤ #β := (f.optionElim b hb).cardinal_le
[GOAL]
α β : Type u
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
⊢ f i ≤ sum f
[PROOFSTEP]
rw [← Quotient.out_eq (f i)]
[GOAL]
α β : Type u
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
⊢ Quotient.mk isEquivalent (Quotient.out (f i)) ≤ sum f
[PROOFSTEP]
exact ⟨⟨fun a => ⟨i, a⟩, fun a b h => by injection h⟩⟩
[GOAL]
α β : Type u
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
a b : Quotient.out (f i)
h : (fun a => { fst := i, snd := a }) a = (fun a => { fst := i, snd := a }) b
⊢ a = b
[PROOFSTEP]
injection h
[GOAL]
α β ι : Type u
a : Cardinal.{u}
⊢ (sum fun x => a) = #ι * a
[PROOFSTEP]
simp
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ sum (f + g) = sum f + sum g
[PROOFSTEP]
have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g
[PROOFSTEP]
simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this 
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum fun i => f i + g i) = (sum fun i => f i) + sum fun i => g i
⊢ sum (f + g) = sum f + sum g
[PROOFSTEP]
exact this
[GOAL]
α β ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out ((fun i => lift (f i)) a))
[PROOFSTEP]
rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g (↑(Embedding.refl ι) i)))
[PROOFSTEP]
have := H i
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g (↑(Embedding.refl ι) i)))
[PROOFSTEP]
rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this 
[GOAL]
α β : Type u
c : Cardinal.{u}
f : α → β
hf : ∀ (b : β), #↑(f ⁻¹' {b}) ≤ c
⊢ #α ≤ #β * c
[PROOFSTEP]
simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using sum_le_sum _ _ hf
[GOAL]
α✝ β✝ α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(↑Equiv.ulift '' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
[PROOFSTEP]
rw [Equiv.image_eq_preimage]
  /- Porting note: Need to insert the following `have` b/c bad fun coercion
                     behaviour for Equivs -/
[GOAL]
α✝ β✝ α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
[PROOFSTEP]
have : FunLike.coe (Equiv.symm (Equiv.ulift (α := α))) = ULift.up (α := α) := rfl
[GOAL]
α✝ β✝ α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift #↑(f ⁻¹' {b}) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
[PROOFSTEP]
rw [this]
[GOAL]
α✝ β✝ α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift #↑(f ⁻¹' {b}) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
[PROOFSTEP]
simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
[GOAL]
α✝ β✝ α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift #↑(f ⁻¹' {b}) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ { x // f x = b } ≃ { x // f x = b }
[PROOFSTEP]
exact Equiv.refl _
[GOAL]
α β ι : Type u
f : ι → Cardinal.{max u v}
⊢ ?m.81660 f ∈ upperBounds (range f)
[PROOFSTEP]
rintro a
  ⟨i, rfl⟩
      -- Porting note: Added universe reference below
[GOAL]
case intro
α β ι : Type u
f : ι → Cardinal.{max u v}
i : ι
⊢ f i ≤ ?m.81660 f
[PROOFSTEP]
exact le_sum.{v, u} f i
[GOAL]
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic a)
[PROOFSTEP]
rw [← mk_out a]
[GOAL]
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic #(Quotient.out a))
[PROOFSTEP]
apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩
[GOAL]
α β : Type u
a : Cardinal.{u}
⊢ Surjective fun x => { val := #↑x, property := (_ : #↑x ≤ #(Quotient.out a)) }
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
α β : Type u
a x : Cardinal.{u}
hx : x ∈ Iic #(Quotient.out a)
⊢ ∃ a_1, (fun x => { val := #↑x, property := (_ : #↑x ≤ #(Quotient.out a)) }) a_1 = { val := x, property := hx }
[PROOFSTEP]
simpa using le_mk_iff_exists_set.1 hx
[GOAL]
α β : Type u
s : Set Cardinal.{u}
⊢ Small.{u, u + 1} ↑s → BddAbove s
[PROOFSTEP]
rintro ⟨ι, ⟨e⟩⟩
[GOAL]
case mk.intro.intro
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s
[PROOFSTEP]
suffices (range fun x : ι => (e.symm x).1) = s by
  rw [← this]
  apply bddAbove_range.{u, u}
[GOAL]
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
this : (range fun x => ↑(↑e.symm x)) = s
⊢ BddAbove s
[PROOFSTEP]
rw [← this]
[GOAL]
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
this : (range fun x => ↑(↑e.symm x)) = s
⊢ BddAbove (range fun x => ↑(↑e.symm x))
[PROOFSTEP]
apply bddAbove_range.{u, u}
[GOAL]
case mk.intro.intro
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ (range fun x => ↑(↑e.symm x)) = s
[PROOFSTEP]
ext x
[GOAL]
case mk.intro.intro.h
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
x : Cardinal.{u}
⊢ (x ∈ range fun x => ↑(↑e.symm x)) ↔ x ∈ s
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨e ⟨x, hx⟩, _⟩⟩
[GOAL]
case mk.intro.intro.h.refine'_1
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
x : Cardinal.{u}
⊢ (x ∈ range fun x => ↑(↑e.symm x)) → x ∈ s
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case mk.intro.intro.h.refine'_1.intro
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : ι
⊢ (fun x => ↑(↑e.symm x)) a ∈ s
[PROOFSTEP]
exact (e.symm a).2
[GOAL]
case mk.intro.intro.h.refine'_2
α β : Type u
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
x : Cardinal.{u}
hx : x ∈ s
⊢ (fun x => ↑(↑e.symm x)) (↑e { val := x, property := hx }) = x
[PROOFSTEP]
simp_rw [Equiv.symm_apply_apply]
[GOAL]
α β : Type u
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)
[PROOFSTEP]
rw [bddAbove_iff_small] at hs ⊢
  -- Porting note: added universes below
[GOAL]
α β : Type u
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)
[PROOFSTEP]
exact small_lift.{_, v, _} _
[GOAL]
α β ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))
[PROOFSTEP]
rw [range_comp]
[GOAL]
α β ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)
[PROOFSTEP]
exact bddAbove_image.{v, w} g hf
[GOAL]
α β ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift #ι * iSup f
[PROOFSTEP]
rw [← (iSup f).lift_id, ← lift_umax, lift_umax.{max u v, u}, ← sum_const]
[GOAL]
α β ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ sum fun x => iSup f
[PROOFSTEP]
exact sum_le_sum _ _ (le_ciSup <| bddAbove_range.{u, v} f)
[GOAL]
α β ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * iSup f
[PROOFSTEP]
rw [← lift_id #ι]
[GOAL]
α β ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ lift #ι * iSup f
[PROOFSTEP]
exact sum_le_iSup_lift f
[GOAL]
α β : Type u
f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun i => f (i + 1)
[PROOFSTEP]
refine' (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans _
[GOAL]
α β : Type u
f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)
[PROOFSTEP]
simp only [mk_sum, mk_out, lift_id, mk_sigma]
[GOAL]
α✝ β : Type u
α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift #(Shrink α) = #α
[PROOFSTEP]
rw [← lift_umax', lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
[PROOFSTEP]
have := H i
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
[PROOFSTEP]
rwa [← mk_out (f i), ← mk_out (g i)] at this 
[GOAL]
α β : Type u
ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0
[PROOFSTEP]
lift f to ι → Type u using fun _ => trivial
[GOAL]
case intro
α β : Type u
ι : Type u_1
f : ι → Type u
⊢ (prod fun i => #(f i)) = 0 ↔ ∃ i, (fun i => #(f i)) i = 0
[PROOFSTEP]
simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]
[GOAL]
α β : Type u
ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
[PROOFSTEP]
simp [prod_eq_zero]
[GOAL]
α β ι : Type u
c : ι → Cardinal.{v}
⊢ lift (prod c) = prod fun i => lift (c i)
[PROOFSTEP]
lift c to ι → Type v using fun _ => trivial
[GOAL]
case intro
α β ι : Type u
c : ι → Type v
⊢ lift (prod fun i => #(c i)) = prod fun i => lift ((fun i => #(c i)) i)
[PROOFSTEP]
simp only [← mk_pi, ← mk_uLift]
[GOAL]
case intro
α β ι : Type u
c : ι → Type v
⊢ #(ULift ((i : ι) → c i)) = #((i : ι) → ULift (c i))
[PROOFSTEP]
exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)
[GOAL]
α✝ β α : Type u
h : Fintype α
f : α → Cardinal.{v}
⊢ prod f = lift (∏ i : α, f i)
[PROOFSTEP]
revert f
[GOAL]
α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
[PROOFSTEP]
refine' Fintype.induction_empty_option _ _ _ α (h_fintype := h)
[GOAL]
case refine'_1
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)) → ∀ (f : β → Cardinal.{v}), prod f = lift (∏ i : β, f i)
[PROOFSTEP]
intro α β hβ e h f
[GOAL]
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
f : β → Cardinal.{v}
⊢ prod f = lift (∏ i : β, f i)
[PROOFSTEP]
letI := Fintype.ofEquiv β e.symm
[GOAL]
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift (∏ i : β, f i)
[PROOFSTEP]
rw [← e.prod_comp f, ← h]
[GOAL]
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i => f (↑e i)
[PROOFSTEP]
exact mk_congr (e.piCongrLeft _).symm
[GOAL]
case refine'_2
α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty → Cardinal.{v}), prod f = lift (∏ i : PEmpty, f i)
[PROOFSTEP]
intro f
[GOAL]
case refine'_2
α✝ β α : Type u
h : Fintype α
f : PEmpty → Cardinal.{v}
⊢ prod f = lift (∏ i : PEmpty, f i)
[PROOFSTEP]
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
[GOAL]
case refine'_3
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift (∏ i : Option α, f i)
[PROOFSTEP]
intro α hα h f
[GOAL]
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ prod f = lift (∏ i : Option α, f i)
[PROOFSTEP]
rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax'.{v, u}, mk_out, ← Cardinal.prod, lift_prod,
  Fintype.prod_option, lift_mul, ← h fun a => f (some a)]
[GOAL]
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ (lift (f none) * prod fun i => lift (f (some i))) = lift (f none) * prod fun a => f (some a)
[PROOFSTEP]
simp only [lift_id]
[GOAL]
α β : Type u
s : Set Cardinal.{v}
⊢ lift (sInf s) = sInf (lift '' s)
[PROOFSTEP]
rcases eq_empty_or_nonempty s with (rfl | hs)
[GOAL]
case inl
α β : Type u
⊢ lift (sInf ∅) = sInf (lift '' ∅)
[PROOFSTEP]
simp
[GOAL]
case inr
α β : Type u
s : Set Cardinal.{v}
hs : Set.Nonempty s
⊢ lift (sInf s) = sInf (lift '' s)
[PROOFSTEP]
exact lift_monotone.map_csInf hs
[GOAL]
α β : Type u
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift (iInf f) = ⨅ (i : ι), lift (f i)
[PROOFSTEP]
unfold iInf
[GOAL]
α β : Type u
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift (sInf (range f)) = sInf (range fun i => lift (f i))
[PROOFSTEP]
convert lift_sInf (range f)
[GOAL]
case h.e'_3.h.e'_3
α β : Type u
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i => lift (f i)) = lift '' range f
[PROOFSTEP]
simp_rw [← comp_apply (f := lift), range_comp]
[GOAL]
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
⊢ #β ≤ lift #α → ∃ a', lift a' = #β
[PROOFSTEP]
rw [← lift_id #β, ← lift_umax, ← lift_umax.{u, v}, lift_mk_le.{v}]
[GOAL]
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
⊢ Nonempty (β ↪ α) → ∃ a', lift a' = lift #β
[PROOFSTEP]
exact fun ⟨f⟩ =>
  ⟨#(Set.range f),
    Eq.symm <|
      lift_mk_eq.{_, _, v}.2
        ⟨Function.Embedding.equivOfSurjective (Embedding.codRestrict _ f Set.mem_range_self) fun ⟨a, ⟨b, e⟩⟩ =>
            ⟨b, Subtype.eq e⟩⟩⟩
[GOAL]
α β : Type u
a : Cardinal.{u}
h : lift (succ a) > succ (lift a)
⊢ False
[PROOFSTEP]
rcases lt_lift_iff.1 h with ⟨b, e, h⟩
[GOAL]
case intro.intro
α β : Type u
a : Cardinal.{u}
h✝ : lift (succ a) > succ (lift a)
b : Cardinal.{u}
e : lift b = succ (lift a)
h : b < succ a
⊢ False
[PROOFSTEP]
rw [lt_succ_iff, ← lift_le, e] at h 
[GOAL]
case intro.intro
α β : Type u
a : Cardinal.{u}
h✝ : lift (succ a) > succ (lift a)
b : Cardinal.{u}
e : lift b = succ (lift a)
h : succ (lift a) ≤ lift a
⊢ False
[PROOFSTEP]
exact h.not_lt (lt_succ _)
[GOAL]
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift a = lift b ↔ lift a = lift b
[PROOFSTEP]
rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]
[GOAL]
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift (sSup s) = sSup (lift '' s)
[PROOFSTEP]
apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
[GOAL]
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ (c : Cardinal.{max u_1 u}), c ∈ upperBounds (lift '' s) → lift (sSup s) ≤ c
[PROOFSTEP]
intro c hc
[GOAL]
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift '' s)
⊢ lift (sSup s) ≤ c
[PROOFSTEP]
by_contra h
[GOAL]
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ c
⊢ False
[PROOFSTEP]
obtain ⟨d, rfl⟩ := Cardinal.lift_down (not_le.1 h).le
[GOAL]
case intro
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift d ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ lift d
⊢ False
[PROOFSTEP]
simp_rw [lift_le] at h hc 
[GOAL]
case intro
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift d ∈ upperBounds (lift '' s)
h : ¬sSup s ≤ d
⊢ False
[PROOFSTEP]
rw [csSup_le_iff' hs] at h 
[GOAL]
case intro
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift d ∈ upperBounds (lift '' s)
h : ¬∀ (x : Cardinal.{u_1}), x ∈ s → x ≤ d
⊢ False
[PROOFSTEP]
exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)
[GOAL]
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift (sSup s) ∈ upperBounds (lift '' s)
[PROOFSTEP]
rintro i ⟨j, hj, rfl⟩
[GOAL]
case intro.intro
α β : Type u
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift j ≤ lift (sSup s)
[PROOFSTEP]
exact lift_le.2 (le_csSup hs hj)
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift (iSup f) = ⨆ (i : ι), lift (f i)
[PROOFSTEP]
rw [iSup, iSup, lift_sSup hf, ← range_comp]
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift ∘ f)) = sSup (range fun i => lift (f i))
[PROOFSTEP]
simp [Function.comp]
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift (f i) ≤ t
⊢ lift (iSup f) ≤ t
[PROOFSTEP]
rw [lift_iSup hf]
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift (f i) ≤ t
⊢ ⨆ (i : ι), lift (f i) ≤ t
[PROOFSTEP]
exact ciSup_le' w
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift (iSup f) ≤ t ↔ ∀ (i : ι), lift (f i) ≤ t
[PROOFSTEP]
rw [lift_iSup hf]
[GOAL]
α β : Type u
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ (i : ι), lift (f i) ≤ t ↔ ∀ (i : ι), lift (f i) ≤ t
[PROOFSTEP]
exact ciSup_le_iff' (bddAbove_range_comp.{_, _, u} hf _)
[GOAL]
α β : Type u
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift (f i) ≤ lift (f' (g i))
⊢ lift (iSup f) ≤ lift (iSup f')
[PROOFSTEP]
rw [lift_iSup hf, lift_iSup hf']
[GOAL]
α β : Type u
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift (f i) ≤ lift (f' (g i))
⊢ ⨆ (i : ι), lift (f i) ≤ ⨆ (i : ι'), lift (f' i)
[PROOFSTEP]
exact ciSup_mono' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ lift c ↔ ℵ₀ ≤ c
[PROOFSTEP]
rw [← lift_aleph0.{u, v}, lift_le]
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ lift c ≤ ℵ₀ ↔ c ≤ ℵ₀
[PROOFSTEP]
rw [← lift_aleph0.{u, v}, lift_le]
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ ℵ₀ < lift c ↔ ℵ₀ < c
[PROOFSTEP]
rw [← lift_aleph0.{u, v}, lift_lt]
[GOAL]
α β : Type u
c : Cardinal.{u}
⊢ lift c < ℵ₀ ↔ c < ℵ₀
[PROOFSTEP]
rw [← lift_aleph0.{u, v}, lift_lt]
[GOAL]
α β : Type u
n : ℕ
⊢ #(Fin n) = ↑n
[PROOFSTEP]
simp
[GOAL]
α β : Type u
n : ℕ
⊢ lift ↑n = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α β : Type u
⊢ lift ↑Nat.zero = ↑Nat.zero
[PROOFSTEP]
simp [*]
[GOAL]
case succ
α β : Type u
n✝ : ℕ
n_ih✝ : lift ↑n✝ = ↑n✝
⊢ lift ↑(Nat.succ n✝) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*]
[GOAL]
α β : Type u
n : ℕ
a : Cardinal.{u}
⊢ ↑n = lift a ↔ ↑n = a
[PROOFSTEP]
rw [← lift_natCast.{v, u} n, lift_inj]
[GOAL]
α β : Type u
a : Cardinal.{u}
n : ℕ
⊢ lift a ≤ ↑n ↔ a ≤ ↑n
[PROOFSTEP]
rw [← lift_natCast.{v, u}, lift_le]
[GOAL]
α β : Type u
n : ℕ
a : Cardinal.{u}
⊢ ↑n ≤ lift a ↔ ↑n ≤ a
[PROOFSTEP]
rw [← lift_natCast.{v, u}, lift_le]
[GOAL]
α β : Type u
a : Cardinal.{u}
n : ℕ
⊢ lift a < ↑n ↔ a < ↑n
[PROOFSTEP]
rw [← lift_natCast.{v, u}, lift_lt]
[GOAL]
α β : Type u
n : ℕ
a : Cardinal.{u}
⊢ ↑n < lift a ↔ ↑n < a
[PROOFSTEP]
rw [← lift_natCast.{v, u}, lift_lt]
[GOAL]
α✝ β α : Type u
s : Finset α
⊢ #{ x // x ∈ s } = ↑(Finset.card s)
[PROOFSTEP]
simp
[GOAL]
α β : Type u
inst✝ : Fintype α
⊢ #(Finset α) = 2 ^ Fintype.card α
[PROOFSTEP]
simp [Pow.pow]
[GOAL]
α✝ β✝ α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = lift #β ^ Fintype.card α
[PROOFSTEP]
simpa using (@Finsupp.equivFunOnFinite α β _ _).cardinal_eq
[GOAL]
α✝ β✝ α β : Type u
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = #β ^ Fintype.card α
[PROOFSTEP]
simp
[GOAL]
α β : Type u
m n : ℕ
⊢ ↑(m ^ n) = ↑m ^ ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α β : Type u
m : ℕ
⊢ ↑(m ^ Nat.zero) = ↑m ^ ↑Nat.zero
[PROOFSTEP]
simp [pow_succ', power_add, *, Pow.pow]
[GOAL]
case succ
α β : Type u
m n✝ : ℕ
n_ih✝ : ↑(m ^ n✝) = ↑m ^ ↑n✝
⊢ ↑(m ^ Nat.succ n✝) = ↑m ^ ↑(Nat.succ n✝)
[PROOFSTEP]
simp [pow_succ', power_add, *, Pow.pow]
[GOAL]
α β : Type u
m n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ n
[PROOFSTEP]
rw [← lift_mk_fin, ← lift_mk_fin, lift_le, le_def, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
  Fintype.card_fin]
[GOAL]
α β : Type u
m n : ℕ
⊢ ↑m < ↑n ↔ m < n
[PROOFSTEP]
rw [lt_iff_le_not_le, ← not_le]
[GOAL]
α β : Type u
m n : ℕ
⊢ ↑m ≤ ↑n ∧ ¬↑n ≤ ↑m ↔ ¬n ≤ m
[PROOFSTEP]
simp only [natCast_le, not_le, and_iff_right_iff_imp]
[GOAL]
α β : Type u
m n : ℕ
⊢ m < n → m ≤ n
[PROOFSTEP]
exact fun h ↦ le_of_lt h
[GOAL]
α β : Type u
n : ℕ
⊢ ↑(Nat.succ n) = succ ↑n
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑n + 1 = succ ↑n
[PROOFSTEP]
refine (add_one_le_succ _).antisymm (succ_le_of_lt ?_)
[GOAL]
α β : Type u
n : ℕ
⊢ ↑n < ↑n + 1
[PROOFSTEP]
rw [← Nat.cast_succ]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑n < ↑(Nat.succ n)
[PROOFSTEP]
exact natCast_lt.2 (Nat.lt_succ_self _)
[GOAL]
α β : Type u
⊢ succ 0 = 1
[PROOFSTEP]
norm_cast
[GOAL]
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
⊢ #α ≤ ↑n
[PROOFSTEP]
refine' le_of_lt_succ (lt_of_not_ge fun hn => _)
[GOAL]
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : #α ≥ succ ↑n
⊢ False
[PROOFSTEP]
rw [← Cardinal.nat_succ, ← lift_mk_fin n.succ] at hn 
[GOAL]
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : #α ≥ lift #(Fin (Nat.succ n))
⊢ False
[PROOFSTEP]
cases' hn with f
[GOAL]
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ False
[PROOFSTEP]
refine' (H <| Finset.univ.map f).not_lt _
[GOAL]
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Finset.card (Finset.map f Finset.univ)
[PROOFSTEP]
rw [Finset.card_map, ← Fintype.card, Fintype.card_ulift, Fintype.card_fin]
[GOAL]
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Nat.succ n
[PROOFSTEP]
exact n.lt_succ_self
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a
[PROOFSTEP]
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb 
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
hb✝ : 1 < b
hb : succ 1 ≤ b
⊢ succ 1 = 2
[PROOFSTEP]
norm_cast
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
hb✝ : 1 < b
hb : 2 ≤ b
⊢ a < b ^ a
[PROOFSTEP]
exact (cantor a).trans_le (power_le_power_right hb)
[GOAL]
α β : Type u
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c
[PROOFSTEP]
rw [← succ_zero, succ_le_iff]
[GOAL]
α β : Type u
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ c ≠ 0
[PROOFSTEP]
rw [one_le_iff_pos, pos_iff_ne_zero]
[GOAL]
α β : Type u
n : ℕ
⊢ succ ↑n ≤ ℵ₀
[PROOFSTEP]
rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
[GOAL]
α β : Type u
n : ℕ
⊢ Nonempty (Fin (Nat.succ n) ↪ ℕ)
[PROOFSTEP]
exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩
[GOAL]
α β : Type u
⊢ 1 < ℵ₀
[PROOFSTEP]
simpa using nat_lt_aleph0 1
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ n, c = ↑n
[PROOFSTEP]
rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩
[GOAL]
case intro.intro
α β : Type u
c : Cardinal.{0}
h' : c < #ℕ
h : lift c < ℵ₀
⊢ ∃ n, lift c = ↑n
[PROOFSTEP]
rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
[GOAL]
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : #↑S < #ℕ
h : lift #↑S < ℵ₀
⊢ ∃ n, lift #↑S = ↑n
[PROOFSTEP]
suffices S.Finite by
  lift S to Finset ℕ using this
  simp
[GOAL]
α β : Type u
S : Set ℕ
h' : #↑S < #ℕ
h : lift #↑S < ℵ₀
this : Set.Finite S
⊢ ∃ n, lift #↑S = ↑n
[PROOFSTEP]
lift S to Finset ℕ using this
[GOAL]
case intro
α β : Type u
S : Finset ℕ
h' : #↑↑S < #ℕ
h : lift #↑↑S < ℵ₀
⊢ ∃ n, lift #↑↑S = ↑n
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : #↑S < #ℕ
h : lift #↑S < ℵ₀
⊢ Set.Finite S
[PROOFSTEP]
contrapose! h'
[GOAL]
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift #↑S < ℵ₀
h' : ¬Set.Finite S
⊢ #ℕ ≤ #↑S
[PROOFSTEP]
haveI := Infinite.to_subtype h'
[GOAL]
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift #↑S < ℵ₀
h' : ¬Set.Finite S
this : Infinite ↑S
⊢ #ℕ ≤ #↑S
[PROOFSTEP]
exact ⟨Infinite.natEmbedding S⟩
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False
[PROOFSTEP]
rcases lt_aleph0.1 hn with ⟨n, rfl⟩
[GOAL]
case intro
α β : Type u
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False
[PROOFSTEP]
exact (Nat.lt_succ_self _).not_le (natCast_le.1 (h (n + 1)))
[GOAL]
α β : Type u
a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀
[PROOFSTEP]
rcases lt_aleph0.1 ha with ⟨n, rfl⟩
[GOAL]
case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀
[PROOFSTEP]
rw [← nat_succ]
[GOAL]
case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(Nat.succ n) < ℵ₀
[PROOFSTEP]
apply nat_lt_aleph0
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : IsLimit c
⊢ ℵ₀ ≤ c
[PROOFSTEP]
by_contra' h'
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : IsLimit c
h' : c < ℵ₀
⊢ False
[PROOFSTEP]
rcases lt_aleph0.1 h' with ⟨_ | n, rfl⟩
[GOAL]
case intro.zero
α β : Type u
h : IsLimit ↑Nat.zero
h' : ↑Nat.zero < ℵ₀
⊢ False
[PROOFSTEP]
exact h.ne_zero.irrefl
[GOAL]
case intro.succ
α β : Type u
n : ℕ
h : IsLimit ↑(Nat.succ n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
[PROOFSTEP]
rw [nat_succ] at h 
[GOAL]
case intro.succ
α β : Type u
n : ℕ
h : IsLimit (succ ↑n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
[PROOFSTEP]
exact not_isSuccLimit_succ _ h.isSuccLimit
[GOAL]
α β : Type u
x : Cardinal.{u_1}
⊢ x ∈ range Nat.cast ↔ x ∈ Iio ℵ₀
[PROOFSTEP]
simp only [mem_Iio, mem_range, eq_comm, lt_aleph0]
[GOAL]
α✝ β α : Type u
n : ℕ
⊢ #α = ↑n ↔ Nonempty (α ≃ Fin n)
[PROOFSTEP]
rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']
[GOAL]
α✝ β α : Type u
⊢ #α < ℵ₀ ↔ Finite α
[PROOFSTEP]
simp only [lt_aleph0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]
[GOAL]
α β : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α
[PROOFSTEP]
rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']
[GOAL]
α β : Type u
s : Set α
⊢ #↑s ≤ ℵ₀ ↔ Set.Countable s
[PROOFSTEP]
rw [mk_le_aleph0_iff, countable_coe_iff]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m + ↑n < ℵ₀
[PROOFSTEP]
rw [← Nat.cast_add]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀
[PROOFSTEP]
apply nat_lt_aleph0
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b
[PROOFSTEP]
simp only [← not_lt, add_lt_aleph0_iff, not_and_or]
[GOAL]
α β : Type u
n : ℕ
a : Cardinal.{u_1}
⊢ n • a < ℵ₀ ↔ n = 0 ∨ a < ℵ₀
[PROOFSTEP]
cases n with
| zero => simpa using nat_lt_aleph0 0
| succ n =>
  simp only [Nat.succ_ne_zero, false_or_iff]
  induction' n with n ih
  · simp
  rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]
[GOAL]
α β : Type u
n : ℕ
a : Cardinal.{u_1}
⊢ n • a < ℵ₀ ↔ n = 0 ∨ a < ℵ₀
[PROOFSTEP]
cases n with
| zero => simpa using nat_lt_aleph0 0
| succ n =>
  simp only [Nat.succ_ne_zero, false_or_iff]
  induction' n with n ih
  · simp
  rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]
[GOAL]
case zero
α β : Type u
a : Cardinal.{u_1}
⊢ Nat.zero • a < ℵ₀ ↔ Nat.zero = 0 ∨ a < ℵ₀
[PROOFSTEP]

| zero => simpa using nat_lt_aleph0 0
[GOAL]
case zero
α β : Type u
a : Cardinal.{u_1}
⊢ Nat.zero • a < ℵ₀ ↔ Nat.zero = 0 ∨ a < ℵ₀
[PROOFSTEP]
simpa using nat_lt_aleph0 0
[GOAL]
case succ
α β : Type u
a : Cardinal.{u_1}
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ Nat.succ n = 0 ∨ a < ℵ₀
[PROOFSTEP]

| succ n =>
  simp only [Nat.succ_ne_zero, false_or_iff]
  induction' n with n ih
  · simp
  rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]
[GOAL]
case succ
α β : Type u
a : Cardinal.{u_1}
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ Nat.succ n = 0 ∨ a < ℵ₀
[PROOFSTEP]
simp only [Nat.succ_ne_zero, false_or_iff]
[GOAL]
case succ
α β : Type u
a : Cardinal.{u_1}
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
[PROOFSTEP]
induction' n with n ih
[GOAL]
case succ.zero
α β : Type u
a : Cardinal.{u_1}
⊢ Nat.succ Nat.zero • a < ℵ₀ ↔ a < ℵ₀
[PROOFSTEP]
simp
[GOAL]
case succ.succ
α β : Type u
a : Cardinal.{u_1}
n : ℕ
ih : Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
⊢ Nat.succ (Nat.succ n) • a < ℵ₀ ↔ a < ℵ₀
[PROOFSTEP]
rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m * ↑n < ℵ₀
[PROOFSTEP]
rw [← Nat.cast_mul]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀
[PROOFSTEP]
apply nat_lt_aleph0
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case neg
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
right
[GOAL]
case neg.h
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
exact Or.inl hb
[GOAL]
case neg
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
right
[GOAL]
case neg.h
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
rw [← Ne, ← one_le_iff_ne_zero] at ha hb 
[GOAL]
case neg.h
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
constructor
[GOAL]
case neg.h.left
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀
[PROOFSTEP]
rw [← mul_one a]
[GOAL]
case neg.h.left
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀
[PROOFSTEP]
refine' (mul_le_mul' le_rfl hb).trans_lt h
[GOAL]
case neg.h.right
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
[PROOFSTEP]
rw [← one_mul b]
[GOAL]
case neg.h.right
α β : Type u
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀
[PROOFSTEP]
refine' (mul_le_mul' ha le_rfl).trans_lt h
[GOAL]
case refine'_2
α β : Type u
a b : Cardinal.{u_1}
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
[PROOFSTEP]
rintro (rfl | rfl | ⟨ha, hb⟩)
[GOAL]
case refine'_2.inl
α β : Type u
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀
[PROOFSTEP]
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]
[GOAL]
case refine'_2.inr.inl
α β : Type u
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀
[PROOFSTEP]
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]
[GOAL]
case refine'_2.inr.inr.intro
α β : Type u
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀
[PROOFSTEP]
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
[PROOFSTEP]
let h := (@mul_lt_aleph0_iff a b).not
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := Iff.not mul_lt_aleph0_iff
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
[PROOFSTEP]
rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h 
[GOAL]
α β : Type u
a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
[PROOFSTEP]
have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a
[GOAL]
α β : Type u
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
[PROOFSTEP]
simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]
[GOAL]
α β : Type u
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
[PROOFSTEP]
simp only [and_comm, or_comm]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀
[PROOFSTEP]
simp [mul_lt_aleph0_iff, ha, hb]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ ↑n < ℵ₀
[PROOFSTEP]
rw [← natCast_pow]
[GOAL]
α β : Type u
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀
[PROOFSTEP]
apply nat_lt_aleph0
[GOAL]
α✝ β α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α
[PROOFSTEP]
rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]
[GOAL]
α✝ β α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)
[PROOFSTEP]
cases' Quotient.exact h with f
[GOAL]
case intro
α✝ β α : Type u
h : #α = ℵ₀
f : α ≃ ULift ℕ
⊢ Nonempty (Denumerable α)
[PROOFSTEP]
exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩
[GOAL]
α β : Type u
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑n
[PROOFSTEP]
rwa [← Nat.cast_one, natCast_le, Nat.one_le_iff_ne_zero]
[GOAL]
α β : Type u
n : ℕ
hn : n ≠ 0
⊢ ℵ₀ * ↑n = ℵ₀
[PROOFSTEP]
rw [mul_comm, nat_mul_aleph0 hn]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑n + ℵ₀ = ℵ₀
[PROOFSTEP]
rw [add_comm, aleph0_add_nat]
[GOAL]
α β : Type u
⊢ (fun c => if h : c < ℵ₀ then choose (_ : ∃ n, c = ↑n) else 0) 0 = 0
[PROOFSTEP]
have h : 0 < ℵ₀ := nat_lt_aleph0 0
[GOAL]
α β : Type u
h : 0 < ℵ₀
⊢ (fun c => if h : c < ℵ₀ then choose (_ : ∃ n, c = ↑n) else 0) 0 = 0
[PROOFSTEP]
dsimp only
[GOAL]
α β : Type u
h : 0 < ℵ₀
⊢ (if h : 0 < ℵ₀ then choose (_ : ∃ n, 0 = ↑n) else 0) = 0
[PROOFSTEP]
rw [dif_pos h, ← Cardinal.natCast_inj, ← Classical.choose_spec (lt_aleph0.1 h), Nat.cast_zero]
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ↑(↑toNat c) = c
[PROOFSTEP]
rw [toNat_apply_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]
[GOAL]
α β : Type u
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ↑(↑toNat c) = 0
[PROOFSTEP]
rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]
[GOAL]
α β : Type u
c d : Cardinal.{u_1}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ ↑toNat c = ↑toNat d ↔ c = d
[PROOFSTEP]
rw [← natCast_inj, cast_toNat_of_lt_aleph0 hc, cast_toNat_of_lt_aleph0 hd]
[GOAL]
α β : Type u
c d : Cardinal.{u_1}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ ↑toNat c ≤ ↑toNat d ↔ c ≤ d
[PROOFSTEP]
rw [← natCast_le, cast_toNat_of_lt_aleph0 hc, cast_toNat_of_lt_aleph0 hd]
[GOAL]
α β : Type u
c d : Cardinal.{u_1}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ ↑toNat c < ↑toNat d ↔ c < d
[PROOFSTEP]
rw [← natCast_lt, cast_toNat_of_lt_aleph0 hc, cast_toNat_of_lt_aleph0 hd]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑toNat ↑n = n
[PROOFSTEP]
rw [toNat_apply_of_lt_aleph0 (nat_lt_aleph0 n), ← natCast_inj]
[GOAL]
α β : Type u
n : ℕ
⊢ ↑(choose (_ : ∃ n_1, ↑n = ↑n_1)) = ↑n
[PROOFSTEP]
exact (Classical.choose_spec (lt_aleph0.1 (nat_lt_aleph0 n))).symm
[GOAL]
α β : Type u
inst✝ : Fintype α
⊢ ↑toNat #α = Fintype.card α
[PROOFSTEP]
simp
[GOAL]
α β : Type u
⊢ ↑toNat 0 = 0
[PROOFSTEP]
rw [← toNat_cast 0, Nat.cast_zero]
[GOAL]
α β : Type u
⊢ ↑toNat 1 = 1
[PROOFSTEP]
rw [← toNat_cast 1, Nat.cast_one]
[GOAL]
α β : Type u
c : Cardinal.{u_1}
⊢ ↑toNat c = 1 ↔ c = 1
[PROOFSTEP]
rw [toNat_eq_iff one_ne_zero, Nat.cast_one]
[GOAL]
α β : Type u
c : Cardinal.{v}
⊢ ↑toNat (lift c) = ↑toNat c
[PROOFSTEP]
apply natCast_injective
[GOAL]
case a
α β : Type u
c : Cardinal.{v}
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
[PROOFSTEP]
cases' lt_or_ge c ℵ₀ with hc hc
[GOAL]
case a.inl
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
[PROOFSTEP]
rw [cast_toNat_of_lt_aleph0, ← lift_natCast.{u, v}, cast_toNat_of_lt_aleph0 hc]
[GOAL]
case a.inl
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ lift c < ℵ₀
[PROOFSTEP]
rwa [lift_lt_aleph0]
[GOAL]
case a.inr
α β : Type u
c : Cardinal.{v}
hc : c ≥ ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
[PROOFSTEP]
rw [cast_toNat_of_aleph0_le, ← lift_natCast.{u, v}, cast_toNat_of_aleph0_le hc, lift_zero]
[GOAL]
case a.inr
α β : Type u
c : Cardinal.{v}
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ lift c
[PROOFSTEP]
rwa [aleph0_le_lift]
[GOAL]
α β✝ : Type u
β : Type v
e : α ≃ β
⊢ ↑toNat #α = ↑toNat #β
[PROOFSTEP]
rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]
[GOAL]
α β : Type u
x y : Cardinal.{u_1}
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx1)
[GOAL]
case inl
α β : Type u
y : Cardinal.{u_1}
⊢ ↑toNat (0 * y) = ↑toNat 0 * ↑toNat y
[PROOFSTEP]
rw [zero_mul, zero_toNat, zero_mul]
[GOAL]
case inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy1)
[GOAL]
case inr.inl
α β : Type u
x : Cardinal.{u_1}
hx1 : x ≠ 0
⊢ ↑toNat (x * 0) = ↑toNat x * ↑toNat 0
[PROOFSTEP]
rw [mul_zero, zero_toNat, mul_zero]
[GOAL]
case inr.inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
cases' lt_or_le x ℵ₀ with hx2 hx2
[GOAL]
case inr.inr.inl
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
cases' lt_or_le y ℵ₀ with hy2 hy2
[GOAL]
case inr.inr.inl.inl
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : y < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
lift x to ℕ using hx2
[GOAL]
case inr.inr.inl.inl.intro
α β : Type u
y : Cardinal.{u_1}
hy1 : y ≠ 0
hy2 : y < ℵ₀
x : ℕ
hx1 : ↑x ≠ 0
⊢ ↑toNat (↑x * y) = ↑toNat ↑x * ↑toNat y
[PROOFSTEP]
lift y to ℕ using hy2
[GOAL]
case inr.inr.inl.inl.intro.intro
α β : Type u
x : ℕ
hx1 : ↑x ≠ 0
y : ℕ
hy1 : ↑y ≠ 0
⊢ ↑toNat (↑x * ↑y) = ↑toNat ↑x * ↑toNat ↑y
[PROOFSTEP]
rw [← Nat.cast_mul, toNat_cast, toNat_cast, toNat_cast]
[GOAL]
case inr.inr.inl.inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
rw [toNat_apply_of_aleph0_le hy2, mul_zero, toNat_apply_of_aleph0_le]
[GOAL]
case inr.inr.inl.inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ℵ₀ ≤ x * y
[PROOFSTEP]
exact aleph0_le_mul_iff'.2 (Or.inl ⟨hx1, hy2⟩)
[GOAL]
case inr.inr.inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
[PROOFSTEP]
rw [toNat_apply_of_aleph0_le hx2, zero_mul, toNat_apply_of_aleph0_le]
[GOAL]
case inr.inr.inr
α β : Type u
x y : Cardinal.{u_1}
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ℵ₀ ≤ x * y
[PROOFSTEP]
exact aleph0_le_mul_iff'.2 (Or.inr ⟨hx2, hy1⟩)
[GOAL]
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ↑toNat (lift a + lift b) = ↑toNat a + ↑toNat b
[PROOFSTEP]
apply Cardinal.natCast_injective
[GOAL]
case a
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
[PROOFSTEP]
replace ha : lift.{v, u} a < ℵ₀ := by rwa [lift_lt_aleph0]
[GOAL]
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ lift a < ℵ₀
[PROOFSTEP]
rwa [lift_lt_aleph0]
[GOAL]
case a
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
hb : b < ℵ₀
ha : lift a < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
[PROOFSTEP]
replace hb : lift.{u, v} b < ℵ₀ := by rwa [lift_lt_aleph0]
[GOAL]
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
hb : b < ℵ₀
ha : lift a < ℵ₀
⊢ lift b < ℵ₀
[PROOFSTEP]
rwa [lift_lt_aleph0]
[GOAL]
case a
α β : Type u
a : Cardinal.{u}
b : Cardinal.{v}
ha : lift a < ℵ₀
hb : lift b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
[PROOFSTEP]
rw [Nat.cast_add, ← toNat_lift.{v, u} a, ← toNat_lift.{u, v} b, cast_toNat_of_lt_aleph0 ha, cast_toNat_of_lt_aleph0 hb,
  cast_toNat_of_lt_aleph0 (add_lt_aleph0 ha hb)]
[GOAL]
α β : Type u
⊢ (fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤) 0 = 0
[PROOFSTEP]
simp [if_pos (zero_lt_one.trans one_lt_aleph0)]
[GOAL]
α β : Type u
x y : Cardinal.{?u.569475}
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (x + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        x +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
by_cases hx : x < ℵ₀
[GOAL]
case pos
α β : Type u
x y : Cardinal.{?u.580039}
hx : x < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (x + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        x +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
obtain ⟨x0, rfl⟩ := lt_aleph0.1 hx
[GOAL]
case pos.intro
α β : Type u
y : Cardinal.{?u.580039}
x0 : ℕ
hx : ↑x0 < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (↑x0 + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        ↑x0 +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
by_cases hy : y < ℵ₀
[GOAL]
case pos
α β : Type u
y : Cardinal.{?u.580319}
x0 : ℕ
hx : ↑x0 < ℵ₀
hy : y < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (↑x0 + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        ↑x0 +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
obtain ⟨y0, rfl⟩ := lt_aleph0.1 hy
[GOAL]
case pos.intro
α β : Type u
x0 : ℕ
hx : ↑x0 < ℵ₀
y0 : ℕ
hy : ↑y0 < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (↑x0 + ↑y0) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        ↑x0 +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        ↑y0
[PROOFSTEP]
simp only [add_lt_aleph0 hx hy, hx, hy, toNat_cast, if_true]
[GOAL]
case pos.intro
α β : Type u
x0 : ℕ
hx : ↑x0 < ℵ₀
y0 : ℕ
hy : ↑y0 < ℵ₀
⊢ ↑(↑toNat (↑x0 + ↑y0)) = ↑x0 + ↑y0
[PROOFSTEP]
rw [← Nat.cast_add, toNat_cast, Nat.cast_add]
[GOAL]
case neg
α β : Type u
y : Cardinal.{?u.581337}
x0 : ℕ
hx : ↑x0 < ℵ₀
hy : ¬y < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (↑x0 + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        ↑x0 +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
simp_rw [if_neg hy, PartENat.add_top]
[GOAL]
case neg
α β : Type u
y : Cardinal.{?u.581337}
x0 : ℕ
hx : ↑x0 < ℵ₀
hy : ¬y < ℵ₀
⊢ (if ↑x0 + y < ℵ₀ then ↑(↑toNat (↑x0 + y)) else ⊤) = ⊤
[PROOFSTEP]
contrapose! hy
[GOAL]
case neg
α β : Type u
y : Cardinal.{?u.581337}
x0 : ℕ
hx : ↑x0 < ℵ₀
hy : (if ↑x0 + y < ℵ₀ then ↑(↑toNat (↑x0 + y)) else ⊤) ≠ ⊤
⊢ y < ℵ₀
[PROOFSTEP]
simp only [ne_eq, ite_eq_right_iff, PartENat.natCast_ne_top, not_forall, exists_prop, and_true] at hy 
[GOAL]
case neg
α β : Type u
y : Cardinal.{?u.581337}
x0 : ℕ
hx : ↑x0 < ℵ₀
hy : ↑x0 + y < ℵ₀
⊢ y < ℵ₀
[PROOFSTEP]
exact le_add_self.trans_lt hy
[GOAL]
case neg
α β : Type u
x y : Cardinal.{?u.581337}
hx : ¬x < ℵ₀
⊢ ZeroHom.toFun
      { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
        map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
      (x + y) =
    ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        x +
      ZeroHom.toFun
        { toFun := fun c => if c < ℵ₀ then ↑(↑toNat c) else ⊤,
          map_zero' := (_ : (if 0 < ℵ₀ then ↑(↑toNat 0) else ⊤) = 0) }
        y
[PROOFSTEP]
simp_rw [if_neg hx, PartENat.top_add]
[GOAL]
case neg
α β : Type u
x y : Cardinal.{?u.581337}
hx : ¬x < ℵ₀
⊢ (if x + y < ℵ₀ then ↑(↑toNat (x + y)) else ⊤) = ⊤
[PROOFSTEP]
contrapose! hx
[GOAL]
case neg
α β : Type u
x y : Cardinal.{?u.581337}
hx : (if x + y < ℵ₀ then ↑(↑toNat (x + y)) else ⊤) ≠ ⊤
⊢ x < ℵ₀
[PROOFSTEP]
simp only [ne_eq, ite_eq_right_iff, PartENat.natCast_ne_top, not_forall, exists_prop, and_true] at hx 
[GOAL]
case neg
α β : Type u
x y : Cardinal.{?u.581337}
hx : x + y < ℵ₀
⊢ x < ℵ₀
[PROOFSTEP]
exact le_self_add.trans_lt hx
[GOAL]
α β : Type u
n : ℕ
⊢ ↑toPartENat ↑n = ↑n
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 (nat_lt_aleph0 n), toNat_cast]
[GOAL]
α β : Type u
c : Cardinal.{u_1}
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc => simp only [toPartENat_apply_of_lt_aleph0 hc, PartENat.natCast_ne_top, false_iff, not_le, hc]
| inr hc => simp only [toPartENat_apply_of_aleph0_le hc, eq_self_iff_true, true_iff]; exact hc
[GOAL]
α β : Type u
c : Cardinal.{u_1}
x✝ : c < ℵ₀ ∨ c ≥ ℵ₀
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc => simp only [toPartENat_apply_of_lt_aleph0 hc, PartENat.natCast_ne_top, false_iff, not_le, hc]
| inr hc => simp only [toPartENat_apply_of_aleph0_le hc, eq_self_iff_true, true_iff]; exact hc
[GOAL]
case inl
α β : Type u
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]

| inl hc => simp only [toPartENat_apply_of_lt_aleph0 hc, PartENat.natCast_ne_top, false_iff, not_le, hc]
[GOAL]
case inl
α β : Type u
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]
simp only [toPartENat_apply_of_lt_aleph0 hc, PartENat.natCast_ne_top, false_iff, not_le, hc]
[GOAL]
case inr
α β : Type u
c : Cardinal.{u_1}
hc : c ≥ ℵ₀
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]

| inr hc => simp only [toPartENat_apply_of_aleph0_le hc, eq_self_iff_true, true_iff]; exact hc
[GOAL]
case inr
α β : Type u
c : Cardinal.{u_1}
hc : c ≥ ℵ₀
⊢ ↑toPartENat c = ⊤ ↔ ℵ₀ ≤ c
[PROOFSTEP]
simp only [toPartENat_apply_of_aleph0_le hc, eq_self_iff_true, true_iff]
[GOAL]
case inr
α β : Type u
c : Cardinal.{u_1}
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ c
[PROOFSTEP]
exact hc
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_iff_le_of_lt_aleph0 hc hc'
  | inr hc' =>
    simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
    exact le_trans h hc'
| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0, le_antisymm h hc]
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
x✝ : c < ℵ₀ ∨ c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_iff_le_of_lt_aleph0 hc hc'
  | inr hc' =>
    simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
    exact le_trans h hc'
| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0, le_antisymm h hc]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_iff_le_of_lt_aleph0 hc hc'
  | inr hc' =>
    simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
    exact le_trans h hc'
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c' ℵ₀ with
| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
| inr hc' =>
  simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
  exact le_trans h hc'
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
x✝ : c' < ℵ₀ ∨ c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c' ℵ₀ with
| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
| inr hc' =>
  simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
  exact le_trans h hc'
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑toNat c ≤ ↑toNat c' ↔ c ≤ c'
[PROOFSTEP]
exact toNat_le_iff_le_of_lt_aleph0 hc hc'
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inr hc' =>
  simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
  exact le_trans h hc'
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
simp only [toPartENat_apply_of_aleph0_le hc', le_top, true_iff]
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ c ≤ c'
[PROOFSTEP]
exact le_trans h hc'
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0, le_antisymm h hc]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_aleph0_le hc]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
hc : c ≥ ℵ₀
⊢ ⊤ ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0, le_antisymm h hc]
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0]
  rw [← not_iff_not, not_le, not_le]
  simp only [hc', lt_of_lt_of_le hc' hc]
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
x✝ : c < ℵ₀ ∨ c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0]
  rw [← not_iff_not, not_le, not_le]
  simp only [hc', lt_of_lt_of_le hc' hc]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_iff_le_of_lt_aleph0 hc hc'
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c < ℵ₀
⊢ ↑toNat c ≤ ↑toNat c' ↔ c ≤ c'
[PROOFSTEP]
exact toNat_le_iff_le_of_lt_aleph0 hc hc'
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]

| inr hc =>
  rw [toPartENat_apply_of_aleph0_le hc]
  simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0]
  rw [← not_iff_not, not_le, not_le]
  simp only [hc', lt_of_lt_of_le hc' hc]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
rw [toPartENat_apply_of_aleph0_le hc]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c ≥ ℵ₀
⊢ ⊤ ≤ ↑toPartENat c' ↔ c ≤ c'
[PROOFSTEP]
simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ c' ↔ c ≤ c'
[PROOFSTEP]
rw [← not_iff_not, not_le, not_le]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
hc : c ≥ ℵ₀
⊢ c' < ℵ₀ ↔ c' < c
[PROOFSTEP]
simp only [hc', lt_of_lt_of_le hc' hc]
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
hc : c ≤ ℵ₀
hc' : c' ≤ ℵ₀
⊢ ↑toPartENat c = ↑toPartENat c' ↔ c = c'
[PROOFSTEP]
rw [le_antisymm_iff, le_antisymm_iff, toPartENat_le_iff_of_le_aleph0 hc, toPartENat_le_iff_of_le_aleph0 hc']
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_of_le_of_lt_aleph0 hc' h
  | inr hc' =>
    rw [toPartENat_apply_of_aleph0_le hc']
    exact le_top
| inr hc => rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le (le_trans hc h)]
[GOAL]
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
x✝ : c < ℵ₀ ∨ c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]
cases lt_or_ge c ℵ₀ with
| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_of_le_of_lt_aleph0 hc' h
  | inr hc' =>
    rw [toPartENat_apply_of_aleph0_le hc']
    exact le_top
| inr hc => rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le (le_trans hc h)]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]

| inl hc =>
  rw [toPartENat_apply_of_lt_aleph0 hc]
  cases lt_or_ge c' ℵ₀ with
  | inl hc' =>
    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
    exact toNat_le_of_le_of_lt_aleph0 hc' h
  | inr hc' =>
    rw [toPartENat_apply_of_aleph0_le hc']
    exact le_top
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc]
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]
cases lt_or_ge c' ℵ₀ with
| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_of_le_of_lt_aleph0 hc' h
| inr hc' =>
  rw [toPartENat_apply_of_aleph0_le hc']
  exact le_top
[GOAL]
case inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
x✝ : c' < ℵ₀ ∨ c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]
cases lt_or_ge c' ℵ₀ with
| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_of_le_of_lt_aleph0 hc' h
| inr hc' =>
  rw [toPartENat_apply_of_aleph0_le hc']
  exact le_top
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]

| inl hc' =>
  rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
  exact toNat_le_of_le_of_lt_aleph0 hc' h
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
[GOAL]
case inl.inl
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' < ℵ₀
⊢ ↑toNat c ≤ ↑toNat c'
[PROOFSTEP]
exact toNat_le_of_le_of_lt_aleph0 hc' h
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]

| inr hc' =>
  rw [toPartENat_apply_of_aleph0_le hc']
  exact le_top
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ↑toPartENat c'
[PROOFSTEP]
rw [toPartENat_apply_of_aleph0_le hc']
[GOAL]
case inl.inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c < ℵ₀
hc' : c' ≥ ℵ₀
⊢ ↑(↑toNat c) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]

| inr hc => rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le (le_trans hc h)]
[GOAL]
case inr
α β : Type u
c c' : Cardinal.{u_1}
h : c ≤ c'
hc : c ≥ ℵ₀
⊢ ↑toPartENat c ≤ ↑toPartENat c'
[PROOFSTEP]
rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le (le_trans hc h)]
[GOAL]
α β : Type u
c : Cardinal.{v}
⊢ ↑toPartENat (lift c) = ↑toPartENat c
[PROOFSTEP]
cases' lt_or_ge c ℵ₀ with hc hc
[GOAL]
case inl
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ ↑toPartENat (lift c) = ↑toPartENat c
[PROOFSTEP]
rw [toPartENat_apply_of_lt_aleph0 hc, Cardinal.toPartENat_apply_of_lt_aleph0 _]
[GOAL]
case inl
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
α β : Type u c : Cardinal.{v} hc : c < ℵ₀ ⊢ lift c < ℵ₀
[PROOFSTEP]
simp only [toNat_lift]
[GOAL]
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ lift c < ℵ₀
[PROOFSTEP]
rw [lift_lt_aleph0]
[GOAL]
α β : Type u
c : Cardinal.{v}
hc : c < ℵ₀
⊢ c < ℵ₀
[PROOFSTEP]
exact hc
[GOAL]
case inr
α β : Type u
c : Cardinal.{v}
hc : c ≥ ℵ₀
⊢ ↑toPartENat (lift c) = ↑toPartENat c
[PROOFSTEP]
rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le _]
[GOAL]
α β : Type u
c : Cardinal.{v}
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ lift c
[PROOFSTEP]
rw [aleph0_le_lift]
[GOAL]
α β : Type u
c : Cardinal.{v}
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ c
[PROOFSTEP]
exact hc
[GOAL]
α β✝ : Type u
β : Type v
e : α ≃ β
⊢ ↑toPartENat #α = ↑toPartENat #β
[PROOFSTEP]
rw [← toPartENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toPartENat_lift]
[GOAL]
α β : Type u
inst✝ : Fintype α
⊢ ↑toPartENat #α = ↑(Fintype.card α)
[PROOFSTEP]
simp
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ False
[PROOFSTEP]
have : Inhabited (∀ i : ι, (g i).out) :=
  by
  refine' ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 _⟩
  rw [mk_out]
  exact (H i).ne_bot
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ Inhabited ((i : ι) → Quotient.out (g i))
[PROOFSTEP]
refine' ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 _⟩
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ #(Quotient.out (g i)) ≠ 0
[PROOFSTEP]
rw [mk_out]
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0
[PROOFSTEP]
exact (H i).ne_bot
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
⊢ False
[PROOFSTEP]
let G := invFun F
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
⊢ False
[PROOFSTEP]
have sG : Surjective G := invFun_surjective F.2
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
⊢ False
[PROOFSTEP]
choose C hc using
  show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
    intro i
    simp only [not_exists.symm, not_forall.symm]
    refine' fun h => (H i).not_le _
    rw [← mk_out (f i), ← mk_out (g i)]
    exact ⟨Embedding.ofSurjective _ h⟩
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
⊢ ∀ (i : ι), ∃ b, ∀ (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ b
[PROOFSTEP]
intro i
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ∃ b, ∀ (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ b
[PROOFSTEP]
simp only [not_exists.symm, not_forall.symm]
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
[PROOFSTEP]
refine' fun h => (H i).not_le _
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ g i ≤ f i
[PROOFSTEP]
rw [← mk_out (f i), ← mk_out (g i)]
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ #(Quotient.out (g i)) ≤ #(Quotient.out (f i))
[PROOFSTEP]
exact ⟨Embedding.ofSurjective _ h⟩
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
⊢ False
[PROOFSTEP]
let ⟨⟨i, a⟩, h⟩ := sG C
[GOAL]
α β : Type u
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
i : ι
a : Quotient.out (f i)
h : G { fst := i, snd := a } = C
⊢ False
[PROOFSTEP]
exact hc i a (congr_fun h _)
[GOAL]
α✝ β α : Type u
n : ℕ
⊢ #(Fin n → α) = #α ^ n
[PROOFSTEP]
simp
[GOAL]
α✝ β α : Type u
⊢ #((n : ℕ) × Vector α n) = sum fun n => #α ^ n
[PROOFSTEP]
simp
[GOAL]
α✝ β α : Type u
s : Set α
⊢ #↑s = 0 ↔ s = ∅
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ β α : Type u
s : Set α
⊢ #↑s = 0 → s = ∅
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ β α : Type u
s : Set α
h : #↑s = 0
⊢ s = ∅
[PROOFSTEP]
rw [mk_eq_zero_iff] at h 
[GOAL]
case mp
α✝ β α : Type u
s : Set α
h : IsEmpty ↑s
⊢ s = ∅
[PROOFSTEP]
exact eq_empty_iff_forall_not_mem.2 fun x hx => h.elim' ⟨x, hx⟩
[GOAL]
case mpr
α✝ β α : Type u
s : Set α
⊢ s = ∅ → #↑s = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α✝ β α : Type u
⊢ #↑∅ = 0
[PROOFSTEP]
exact mk_emptyCollection _
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift #α ≤ lift #β
[PROOFSTEP]
rw [← Cardinal.mk_range_eq_of_injective hf]
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift #↑(range f) ≤ lift #β
[PROOFSTEP]
exact Cardinal.lift_le.2 (Cardinal.mk_set_le _)
[GOAL]
α✝ β α : Type u
A : Set (Set α)
⊢ #↑(⋃₀ A) ≤ #↑A * ⨆ (s : ↑A), #↑↑s
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
α✝ β α : Type u
A : Set (Set α)
⊢ #↑(⋃ (i : ↑A), ↑i) ≤ #↑A * ⨆ (s : ↑A), #↑↑s
[PROOFSTEP]
apply mk_iUnion_le
[GOAL]
α✝ β ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ (x : ι) (_ : x ∈ s), A x) ≤ #↑s * ⨆ (x : ↑s), #↑(A ↑x)
[PROOFSTEP]
rw [biUnion_eq_iUnion]
[GOAL]
α✝ β ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ (x : ↑s), A ↑x) ≤ #↑s * ⨆ (x : ↑s), #↑(A ↑x)
[PROOFSTEP]
apply mk_iUnion_le
[GOAL]
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n ↔ ∃ t, ↑t = s ∧ Finset.card t = n
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ Finset.card t = n
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
h : #↑s = ↑n
⊢ ∃ t, ↑t = s ∧ Finset.card t = n
[PROOFSTEP]
lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ nat_lt_aleph0 n)
[GOAL]
case mp.intro
α✝ β : Type u
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ Finset.card t = n
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ Finset.card t = n) → #↑s = ↑n
[PROOFSTEP]
rintro ⟨t, rfl, rfl⟩
[GOAL]
case mpr.intro.intro
α✝ β : Type u
α : Type u_1
t : Finset α
⊢ #↑↑t = ↑(Finset.card t)
[PROOFSTEP]
exact mk_coe_finset
[GOAL]
α β : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ t, ↑t = univ ∧ Finset.card t = n
[PROOFSTEP]
rw [← mk_univ, mk_set_eq_nat_iff_finset]
[GOAL]
α β : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ h, Fintype.card α = n
[PROOFSTEP]
rw [mk_eq_nat_iff_finset]
[GOAL]
α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) ↔ ∃ h, Fintype.card α = n
[PROOFSTEP]
constructor
[GOAL]
case mp
α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) → ∃ h, Fintype.card α = n
[PROOFSTEP]
rintro ⟨t, ht, hn⟩
[GOAL]
case mp.intro.intro
α β : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : Finset.card t = n
⊢ ∃ h, Fintype.card α = n
[PROOFSTEP]
exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩
[GOAL]
case mpr
α β : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ Finset.card t = n
[PROOFSTEP]
rintro ⟨⟨t, ht⟩, hn⟩
[GOAL]
case mpr.intro.mk
α β : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ Finset.card t = n
[PROOFSTEP]
exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩
[GOAL]
α✝ β α : Type u
s : Set α
a : α
h : ¬a ∈ s
⊢ #↑(insert a s) = #↑s + 1
[PROOFSTEP]
rw [← union_singleton, mk_union_of_disjoint, mk_singleton]
[GOAL]
α✝ β α : Type u
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint s {a}
[PROOFSTEP]
simpa
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
[PROOFSTEP]
refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ Finset.card s ≤ n
[PROOFSTEP]
simpa using (mk_le_mk_of_subset hs).trans H
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
⊢ #↑t ≤ ↑n
[PROOFSTEP]
apply card_le_of (fun s ↦ ?_)
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
s : Finset ↑t
⊢ Finset.card s ≤ n
[PROOFSTEP]
let u : Finset α := s.image Subtype.val
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
⊢ Finset.card s ≤ n
[PROOFSTEP]
have : u.card = s.card := Finset.card_image_of_injOn (injOn_of_injective Subtype.coe_injective _)
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : Finset.card u = Finset.card s
⊢ Finset.card s ≤ n
[PROOFSTEP]
rw [← this]
[GOAL]
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : Finset.card u = Finset.card s
⊢ Finset.card u ≤ n
[PROOFSTEP]
apply H
[GOAL]
case a
α✝ β α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → Finset.card s ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : Finset.card u = Finset.card s
⊢ ↑u ⊆ t
[PROOFSTEP]
simp only [Finset.coe_image, image_subset_iff, Subtype.coe_preimage_self, subset_univ]
[GOAL]
α β : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T) + #↑T = #↑S
[PROOFSTEP]
refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [diff_union_of_subset h]
[GOAL]
α β : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T ∪ T) = #↑S
[PROOFSTEP]
rw [diff_union_of_subset h]
[GOAL]
α β : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T
[PROOFSTEP]
exact disjoint_sdiff_self_left
[GOAL]
α✝ β : Type u
α : Type u_1
P Q : Set α
⊢ #↑(P ∪ Q) ≤ ℵ₀ ↔ #↑P ≤ ℵ₀ ∧ #↑Q ≤ ℵ₀
[PROOFSTEP]
simp only [le_aleph0_iff_subtype_countable, mem_union, setOf_mem_eq, Set.union_def, ← countable_union]
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift #↑(f ⁻¹' s) ≤ lift #↑s
[PROOFSTEP]
rw [lift_mk_le.{0}]
  -- Porting note: Needed to insert `mem_preimage.mp` below
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
[PROOFSTEP]
use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
[GOAL]
case inj'
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x => f ↑x) (_ : ∀ (x : ↑(f ⁻¹' s)), f ↑x ∈ s))
[PROOFSTEP]
apply Subtype.coind_injective
[GOAL]
case inj'.hf
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x => f ↑x
[PROOFSTEP]
exact h.comp Subtype.val_injective
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift #↑s ≤ lift #↑(f ⁻¹' s)
[PROOFSTEP]
rw [lift_mk_le.{0}]
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Nonempty (↑s ↪ ↑(f ⁻¹' s))
[PROOFSTEP]
refine' ⟨⟨_, _⟩⟩
[GOAL]
case refine'_1
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ ↑s → ↑(f ⁻¹' s)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case refine'_1.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
⊢ ↑(f ⁻¹' s)
[PROOFSTEP]
rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
[GOAL]
case refine'_1.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
⊢ ↑(f ⁻¹' s)
[PROOFSTEP]
exact ⟨x, hy⟩
[GOAL]
case refine'_2
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Injective fun a =>
    Subtype.casesOn a fun y hy =>
      Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
        Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy
[PROOFSTEP]
rintro ⟨y, hy⟩ ⟨y', hy'⟩
[GOAL]
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y, property := hy } =
      (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y', property := hy' } →
    { val := y, property := hy } = { val := y', property := hy' }
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy_1 => { val := ↑(subtype_of_exists (_ : y ∈ range f)), property := hy_1 })
        (_ : f ↑(subtype_of_exists (_ : y ∈ range f)) = y) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := y, property := hy } = { val := y', property := hy' }
[PROOFSTEP]
rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
[GOAL]
case refine'_2.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y' : β
hy' : y' ∈ s
x : α
hy : f x ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := f x, property := hy } = { val := y', property := hy' }
[PROOFSTEP]
rcases Classical.subtype_of_exists (h hy') with ⟨x', rfl⟩
[GOAL]
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x', property := (_ : f x' = f x') }, property := hy })
        (_ : f ↑{ val := x', property := (_ : f x' = f x') } = f x') hy' →
    { val := f x, property := hy } = { val := f x', property := hy' }
[PROOFSTEP]
simp
[GOAL]
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ x = x' → f x = f x'
[PROOFSTEP]
intro hxx'
[GOAL]
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
hxx' : x = x'
⊢ f x = f x'
[PROOFSTEP]
rw [hxx']
[GOAL]
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #↑(f ⁻¹' s) ≤ #↑s
[PROOFSTEP]
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
[GOAL]
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift #↑(f ⁻¹' s) ≤ lift #↑s
[PROOFSTEP]
exact mk_preimage_of_injective_lift f s h
[GOAL]
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ #↑(f ⁻¹' s)
[PROOFSTEP]
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
[GOAL]
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift #↑s ≤ lift #↑(f ⁻¹' s)
[PROOFSTEP]
exact mk_preimage_of_subset_range_lift f s h
[GOAL]
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑s
[PROOFSTEP]
convert mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1
[GOAL]
case h.e'_2
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = lift #↑(f ⁻¹' s)
[PROOFSTEP]
rw [lift_id]
[GOAL]
case h.e'_3
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑s = lift #↑s
[PROOFSTEP]
rw [lift_id]
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift #↑t ≤ lift #↑{x | x ∈ s ∧ f x ∈ t}
[PROOFSTEP]
rw [image_eq_range] at h 
[GOAL]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift #↑t ≤ lift #↑{x | x ∈ s ∧ f x ∈ t}
[PROOFSTEP]
convert mk_preimage_of_subset_range_lift _ _ h using 1
[GOAL]
case h.e'_4
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift #↑{x | x ∈ s ∧ f x ∈ t} = lift #↑((fun x => f ↑x) ⁻¹' t)
[PROOFSTEP]
rw [mk_sep]
[GOAL]
case h.e'_4
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift #↑{x | f ↑x ∈ t} = lift #↑((fun x => f ↑x) ⁻¹' t)
[PROOFSTEP]
rfl
[GOAL]
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}
[PROOFSTEP]
rw [image_eq_range] at h 
[GOAL]
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}
[PROOFSTEP]
convert mk_preimage_of_subset_range _ _ h using 1
[GOAL]
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)
[PROOFSTEP]
rw [mk_sep]
[GOAL]
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)
[PROOFSTEP]
rfl
[GOAL]
α✝ β : Type u
c : Cardinal.{u}
α : Type u
s : Set α
⊢ c ≤ #↑s ↔ ∃ p, p ⊆ s ∧ #↑p = c
[PROOFSTEP]
rw [le_mk_iff_exists_set, ← Subtype.exists_set_subtype]
[GOAL]
α✝ β : Type u
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
α✝ β : Type u
c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c
[PROOFSTEP]
intro t
[GOAL]
case h
α✝ β : Type u
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c
[PROOFSTEP]
rw [mk_image_eq]
[GOAL]
case h
α✝ β : Type u
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val
[PROOFSTEP]
apply Subtype.val_injective
[GOAL]
α β : Type u
⊢ 2 ≤ #α ↔ ∃ x y, x ≠ y
[PROOFSTEP]
rw [← Nat.cast_two, nat_succ, succ_le_iff, Nat.cast_one, one_lt_iff_nontrivial, nontrivial_iff]
[GOAL]
α β : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ y, y ≠ x
[PROOFSTEP]
rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]
[GOAL]
α β : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
[GOAL]
α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
constructor
[GOAL]
case mp
α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
rintro ⟨t, ht, x, y, hne, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
exact ⟨x, y, hne, by simpa using ht⟩
[GOAL]
α β : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ
[PROOFSTEP]
simpa using ht
[GOAL]
case mpr
α β : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
[PROOFSTEP]
rintro ⟨x, y, hne, h⟩
[GOAL]
case mpr.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
[PROOFSTEP]
exact ⟨{ x, y }, by simpa using h, x, y, hne, rfl⟩
[GOAL]
α β : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ
[PROOFSTEP]
simpa using h
[GOAL]
α β : Type u
x : α
⊢ #α = 2 ↔ ∃! y, y ≠ x
[PROOFSTEP]
rw [mk_eq_two_iff]
[GOAL]
α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
[PROOFSTEP]
constructor
[GOAL]
case mp
α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x
[PROOFSTEP]
rintro ⟨a, b, hne, h⟩
[GOAL]
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x
[PROOFSTEP]
simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h 
[GOAL]
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x
[PROOFSTEP]
rcases h x with (rfl | rfl)
[GOAL]
case mp.intro.intro.intro.inl
α β : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y, y ≠ x
case mp.intro.intro.intro.inr α β : Type u x a : α hne : a ≠ x h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x ⊢ ∃! y, y ≠ x
[PROOFSTEP]
exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]
[GOAL]
case mpr
α β : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
rintro ⟨y, hne, hy⟩
[GOAL]
case mpr.intro.intro
α β : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y => y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
[PROOFSTEP]
exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩
[GOAL]
α✝ β : Type u
α : Type u_1
l : List α
h : ↑(List.length l) < #α
⊢ ∃ z, ¬z ∈ l
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ β : Type u
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α ≤ ↑(List.length l)
[PROOFSTEP]
calc
  #α = #(Set.univ : Set α) := mk_univ.symm
  _ ≤ #l.toFinset := (mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x))
  _ = l.toFinset.card := Cardinal.mk_coe_finset
  _ ≤ l.length := Cardinal.natCast_le.mpr (List.toFinset_card_le l)
[GOAL]
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
have : ↑(3 : ℕ) ≤ #α
[GOAL]
case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ↑3 ≤ #α
α✝ β : Type u α : Type u_1 h : 3 ≤ #α x y : α this : ↑3 ≤ #α ⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
simpa using h
[GOAL]
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
have : ↑(2 : ℕ) < #α
[GOAL]
case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑2 < #α
α✝ β : Type u α : Type u_1 h : 3 ≤ #α x y : α this✝ : ↑3 ≤ #α this : ↑2 < #α ⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
rwa [← succ_le_iff, ← Cardinal.nat_succ]
[GOAL]
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
this✝ : ↑3 ≤ #α
this : ↑2 < #α
⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
have := exists_not_mem_of_length_lt [x, y] this
[GOAL]
α✝ β : Type u
α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, ¬z ∈ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y
[PROOFSTEP]
simpa [not_or] using this
[GOAL]
α β : Type u
b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b
[PROOFSTEP]
refine le_ciSup (f := fun y : Iio b => a ^ y) ?_ ⟨c, h⟩
[GOAL]
α β : Type u
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (range fun y => a ^ ↑y)
[PROOFSTEP]
rw [← image_eq_range]
[GOAL]
α β : Type u
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
[PROOFSTEP]
exact bddAbove_image.{u, u} _ bddAbove_Iio
[GOAL]
α β : Type u
a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ (x : Cardinal.{u}), x < b → a ^ x ≤ c
[PROOFSTEP]
rw [powerlt, ciSup_le_iff']
[GOAL]
α β : Type u
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ (x : Cardinal.{u}), x < b → a ^ x ≤ c
[PROOFSTEP]
simp
[GOAL]
case h
α β : Type u
a b c : Cardinal.{u}
⊢ BddAbove (range fun c => a ^ ↑c)
[PROOFSTEP]
rw [← image_eq_range]
[GOAL]
case h
α β : Type u
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)
[PROOFSTEP]
exact bddAbove_image.{u, u} _ bddAbove_Iio
[GOAL]
α β : Type u
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1
[PROOFSTEP]
apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm
[GOAL]
α β : Type u
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 1 ≤ 0 ^< a
[PROOFSTEP]
rw [← power_zero]
[GOAL]
α β : Type u
a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.860481 ^ 0 ≤ 0 ^< a
α β : Type u a : Cardinal.{u_1} h : a ≠ 0 ⊢ Cardinal.{u_1}
[PROOFSTEP]
exact le_powerlt 0 (pos_iff_ne_zero.2 h)
[GOAL]
α β : Type u
a : Cardinal.{u_1}
⊢ a ^< 0 = 0
[PROOFSTEP]
convert Cardinal.iSup_of_empty _
[GOAL]
case convert_3
α β : Type u
a : Cardinal.{u_1}
⊢ IsEmpty ↑(Iio 0)
[PROOFSTEP]
exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr (Cardinal.zero_le x).not_lt
[GOAL]
α β R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
⊢ lift #R ≤ lift #E
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0
[GOAL]
case intro
α β R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
⊢ lift #R ≤ lift #E
[PROOFSTEP]
have : Injective (fun k ↦ k • x) := smul_left_injective R hx
[GOAL]
case intro
α β R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
this : Injective fun k => k • x
⊢ lift #R ≤ lift #E
[PROOFSTEP]
exact lift_mk_le_lift_mk_of_injective this
