feat: When Nat.card is zero (#8202)

and lemmas about injectivity/surjectivity of `PLift.map`/`ULift.map`.

Mathlib/Control/ULift.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Jannis Limperg
 -/
-
 import Mathlib.Mathport.Rename
 
 #align_import control.ulift from "leanprover-community/mathlib"@"99e8971dc62f1f7ecf693d75e75fbbabd55849de"
@@ -13,8 +12,7 @@ import Mathlib.Mathport.Rename
 
 In this file we define `Monad` and `IsLawfulMonad` instances on `PLift` and `ULift`. -/
 
-
-universe u v
+universe u v u' v'
 
 namespace PLift
 
@@ -90,16 +88,14 @@ end PLift
 
 namespace ULift
 
-variable {α : Type u} {β : Type v}
+variable {α : Type u} {β : Type v} {f : α → β}
 
 /-- Functorial action. -/
-protected def map (f : α → β) (a : ULift α) : ULift β :=
-  ULift.up.{u} (f a.down)
+protected def map (f : α → β) (a : ULift.{u'} α) : ULift.{v'} β := ULift.up.{v'} (f a.down)
 #align ulift.map ULift.map
 
 @[simp]
-theorem map_up (f : α → β) (a : α) : (ULift.up.{u} a).map f = ULift.up.{u} (f a) :=
-  rfl
+theorem map_up (f : α → β) (a : α) : (ULift.up.{u'} a).map f = ULift.up.{v'} (f a) := rfl
 #align ulift.map_up ULift.map_up
 
 /-- Embedding of pure values. -/

Mathlib/Data/Nat/Totient.lean

@@ -70,7 +70,9 @@ theorem totient_lt (n : ℕ) (hn : 1 < n) : φ n < n :=
 theorem totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
   | 0 => by decide
   | 1 => by simp [totient]
-  | n + 2 => fun _ => card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 (by simp), coprime_one_right _⟩⟩
+  | n + 2 => fun _ =>
+  -- Must qualify `Finset.card_pos` because of leanprover/lean4#2849
+    Finset.card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 (by simp), coprime_one_right _⟩⟩
 #align nat.totient_pos Nat.totient_pos
 
 theorem filter_coprime_Ico_eq_totient (a n : ℕ) :

Mathlib/Data/ULift.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Control.ULift
 import Mathlib.Logic.Equiv.Basic
 
 #align_import data.ulift from "leanprover-community/mathlib"@"41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3"
@@ -15,13 +16,13 @@ In this file we provide `Subsingleton`, `Unique`, `DecidableEq`, and `isEmpty` i
 `PLift.exists`.
 -/
 
-universe u v
+universe u v u' v'
 
 open Function
 
 namespace PLift
 
-variable {α : Sort u} {β : Sort v}
+variable {α : Sort u} {β : Sort v} {f : α → β}
 
 instance [Subsingleton α] : Subsingleton (PLift α) :=
   Equiv.plift.subsingleton
@@ -73,11 +74,20 @@ theorem «exists» {p : PLift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (PLi
   up_surjective.exists
 #align plift.exists PLift.exists
 
+@[simp] lemma map_injective : Injective (PLift.map f) ↔ Injective f :=
+  (Injective.of_comp_iff' _ down_bijective).trans $ up_injective.of_comp_iff _
+
+@[simp] lemma map_surjective : Surjective (PLift.map f) ↔ Surjective f :=
+  (down_surjective.of_comp_iff _).trans $ Surjective.of_comp_iff' up_bijective _
+
+@[simp] lemma map_bijective : Bijective (PLift.map f) ↔ Bijective f :=
+  (down_bijective.of_comp_iff _).trans $ Bijective.of_comp_iff' up_bijective _
+
 end PLift
 
 namespace ULift
 
-variable {α : Type u} {β : Type v}
+variable {α : Type u} {β : Type v} {f : α → β}
 
 instance [Subsingleton α] : Subsingleton (ULift α) :=
   Equiv.ulift.subsingleton
@@ -129,6 +139,16 @@ theorem «exists» {p : ULift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (ULi
   up_surjective.exists
 #align ulift.exists ULift.exists
 
+@[simp] lemma map_injective : Injective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Injective f :=
+  (Injective.of_comp_iff' _ down_bijective).trans $ up_injective.of_comp_iff _
+
+@[simp] lemma map_surjective :
+    Surjective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Surjective f :=
+  (down_surjective.of_comp_iff _).trans $ Surjective.of_comp_iff' up_bijective _
+
+@[simp] lemma map_bijective : Bijective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Bijective f :=
+  (down_bijective.of_comp_iff _).trans $ Bijective.of_comp_iff' up_bijective _
+
 @[ext]
 theorem ext (x y : ULift α) (h : x.down = y.down) : x = y :=
   congrArg up h

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -375,7 +375,8 @@ theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) :
   have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
   apply card_orderOf_eq_totient_aux₁ hn hd
   by_contra h0
-  simp only [not_lt, _root_.le_zero_iff, card_eq_zero] at h0
+  -- Must qualify `Finset.card_eq_zero` because of leanprover/lean4#2849
+  simp only [not_lt, _root_.le_zero_iff, Finset.card_eq_zero] at h0
   apply lt_irrefl c
   calc
     c = ∑ m in c.divisors, (univ.filter fun a : α => orderOf a = m).card := by

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -1615,6 +1615,9 @@ theorem infinite_iff {α : Type u} : Infinite α ↔ ℵ₀ ≤ #α := by
   rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]
 #align cardinal.infinite_iff Cardinal.infinite_iff
 
+lemma aleph0_le_mk_iff : ℵ₀ ≤ #α ↔ Infinite α := infinite_iff.symm
+lemma mk_lt_aleph0_iff : #α < ℵ₀ ↔ Finite α := by simp [← not_le, aleph0_le_mk_iff]
+
 @[simp]
 theorem aleph0_le_mk (α : Type u) [Infinite α] : ℵ₀ ≤ #α :=
   infinite_iff.1 ‹_›
@@ -1692,6 +1695,8 @@ theorem ofNat_add_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n)
 theorem aleph0_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ + no_index (OfNat.ofNat n) = ℵ₀ :=
   aleph0_add_nat n
 
+variable {c : Cardinal}
+
 /-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
   to 0. -/
 def toNat : ZeroHom Cardinal ℕ where
@@ -1703,6 +1708,15 @@ def toNat : ZeroHom Cardinal ℕ where
       Nat.cast_zero]
 #align cardinal.to_nat Cardinal.toNat
 
+@[simp]
+lemma toNat_eq_zero : toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c := by
+  simp only [toNat, ZeroHom.coe_mk, dite_eq_right_iff, or_iff_not_imp_right, not_le]
+  refine' forall_congr' fun h => _
+  rw [←@Nat.cast_eq_zero Cardinal, ← Classical.choose_spec (p := fun n : ℕ ↦ c = n)]
+
+lemma toNat_ne_zero : toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀ := by simp [not_or]
+@[simp] lemma toNat_pos : 0 < toNat c ↔ c ≠ 0 ∧ c < ℵ₀ := pos_iff_ne_zero.trans toNat_ne_zero
+
 theorem toNat_apply_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) :
     toNat c = Classical.choose (lt_aleph0.1 h) :=
   dif_pos h

Mathlib/SetTheory/Cardinal/Finite.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
+import Mathlib.Data.ULift
 import Mathlib.Data.ZMod.Defs
 import Mathlib.SetTheory.Cardinal.Basic
 
@@ -21,13 +22,11 @@ import Mathlib.SetTheory.Cardinal.Basic
 
 set_option autoImplicit true
 
-
-open Cardinal
+open Cardinal Function
+open scoped BigOperators
 
 noncomputable section
 
-open BigOperators
-
 variable {α β : Type*}
 
 namespace Nat
@@ -43,19 +42,37 @@ theorem card_eq_fintype_card [Fintype α] : Nat.card α = Fintype.card α :=
   mk_toNat_eq_card
 #align nat.card_eq_fintype_card Nat.card_eq_fintype_card
 
-@[simp]
-theorem card_eq_zero_of_infinite [Infinite α] : Nat.card α = 0 :=
-  mk_toNat_of_infinite
+lemma card_eq_zero_of_isEmpty [IsEmpty α] : Nat.card α = 0 := by simp [Nat.card]
+@[simp] lemma card_eq_zero_of_infinite [Infinite α] : Nat.card α = 0 := mk_toNat_of_infinite
 #align nat.card_eq_zero_of_infinite Nat.card_eq_zero_of_infinite
 
-theorem finite_of_card_ne_zero (h : Nat.card α ≠ 0) : Finite α :=
-  not_infinite_iff_finite.mp <| h ∘ @Nat.card_eq_zero_of_infinite α
+lemma card_eq_zero : Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α := by
+  simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]
+
+lemma card_ne_zero : Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α := by simp [card_eq_zero, not_or]
+
+lemma card_pos_iff : 0 < Nat.card α ↔ Nonempty α ∧ Finite α := by
+  simp [Nat.card, mk_eq_zero_iff, mk_lt_aleph0_iff]
+
+@[simp] lemma card_pos [Nonempty α] [Finite α] : 0 < Nat.card α := card_pos_iff.2 ⟨‹_›, ‹_›⟩
+
+theorem finite_of_card_ne_zero (h : Nat.card α ≠ 0) : Finite α := (card_ne_zero.1 h).2
 #align nat.finite_of_card_ne_zero Nat.finite_of_card_ne_zero
 
 theorem card_congr (f : α ≃ β) : Nat.card α = Nat.card β :=
   Cardinal.toNat_congr f
 #align nat.card_congr Nat.card_congr
 
+lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
+    (hf : Injective f) : Nat.card α ≤ Nat.card β := by
+  simpa using toNat_le_of_le_of_lt_aleph0 (by simp [lt_aleph0_of_finite]) $
+    mk_le_of_injective (α := ULift.{max u v} α) (β := ULift.{max u v} β) $ ULift.map_injective.2 hf
+
+lemma card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β)
+    (hf : Surjective f) : Nat.card β ≤ Nat.card α := by
+  simpa using toNat_le_of_le_of_lt_aleph0 (by simp [lt_aleph0_of_finite]) $ mk_le_of_surjective
+    (α := ULift.{max u v} α) (β := ULift.{max u v} β) $ ULift.map_surjective.2 hf
+
 theorem card_eq_of_bijective (f : α → β) (hf : Function.Bijective f) : Nat.card α = Nat.card β :=
   card_congr (Equiv.ofBijective f hf)
 #align nat.card_eq_of_bijective Nat.card_eq_of_bijective
@@ -172,6 +189,9 @@ theorem card_pLift (α : Type*) : card (PLift α) = card α :=
   card_congr Equiv.plift
 #align part_enat.card_plift PartENat.card_pLift
 
+lemma card_mono {s t : Set α} (ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t :=
+  toNat_le_of_le_of_lt_aleph0 ht.lt_aleph0 <| mk_le_mk_of_subset h
+
 theorem card_image_of_injOn {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h : Set.InjOn f s) :
     card (f '' s) = card s :=
   card_congr (Equiv.Set.imageOfInjOn f s h).symm