[Merged by Bors] - feat(SetTheory/Cardinal): helpers for Konig's theorem on bipartite graphs

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -464,6 +464,10 @@ theorem add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < ℵ₀)
   rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
   exact ⟨by grw [h.1], mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩
 
+lemma add_lt_add_iff_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < ℵ₀) :
+  α + γ < β + γ ↔ α < β := by
+  constructor <;> contrapose! <;> simp [add_le_add_iff_of_lt_aleph0 γ₀]
+
 @[simp]
 theorem add_nat_le_add_nat_iff {α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β :=
   add_le_add_iff_of_lt_aleph0 (nat_lt_aleph0 n)
@@ -472,6 +476,36 @@ theorem add_nat_le_add_nat_iff {α β : Cardinal} (n : ℕ) : α + n ≤ β + n
 theorem add_one_le_add_one_iff {α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β :=
   add_le_add_iff_of_lt_aleph0 one_lt_aleph0
 
+lemma add_lt_add_of_lt_of_lt {κ₁ κ₂ μ₁ μ₂ : Cardinal}
+    (hκ : κ₁ < κ₂) (hμ : μ₁ < μ₂) : κ₁ + μ₁ < κ₂ + μ₂ := by
+  rcases le_or_gt ℵ₀ (κ₂ + μ₂) with hinf | hfin
+  · refine add_lt_of_lt hinf ?_ ?_ <;> apply lt_of_lt_of_le <;> solve | assumption | simp
+  · have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀ := add_lt_aleph0_iff.1 hfin
+    apply lt_of_le_of_lt
+    · exact (add_le_add_iff_of_lt_aleph0 (lt_trans hμ hfin_.right)).mpr <| le_of_lt hκ
+    · simpa [add_comm] using (add_lt_add_iff_of_lt_aleph0 hfin_.left).mpr hμ
+
+lemma mul_lt_mul_of_nat {n : ℕ} {κ μ : Cardinal} {hneq0 : n ≠ 0} (hlt : κ < μ) : n * κ < n * μ := by
+  cases n with
+  | zero => contradiction
+  | succ m =>
+    push_cast
+    rw [add_mul, one_mul, add_mul, one_mul]
+    cases m with
+    | zero => simpa
+    | succ k =>
+      have : ↑(k + 1) * κ < ↑(k + 1) * μ := mul_lt_mul_of_nat (hneq0 := Nat.succ_ne_zero k) hlt
+      exact Cardinal.add_lt_add_of_lt_of_lt this hlt
+
+
+lemma mul_left_cancel_of_nat {n : ℕ} {κ μ : Cardinal} {hneq0 : n ≠ 0} (h : n * κ = n * μ) :
+  κ = μ := by
+  contrapose! h
+  rcases lt_or_gt_of_ne h with hlt | hlt <;>
+  have := ne_of_lt <| mul_lt_mul_of_nat (hneq0 := hneq0) hlt <;>
+  symm_saturate <;>
+  assumption
+
 end aleph
 
 /-! ### Properties about `power` -/

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -833,6 +833,17 @@ theorem mk_subtype_mono {p q : α → Prop} (h : ∀ x, p x → q x) :
     #{ x // p x } ≤ #{ x // q x } :=
   ⟨embeddingOfSubset _ _ h⟩
 
+lemma card_ssubset' {A B : Set α} {hfin : #B < ℵ₀} (hlt : A < B) : #A < #B := by
+  have : #A ≤ #B := mk_subtype_mono hlt.1
+  have : Fintype A := ((lt_aleph0_iff_fintype).1 <| hfin.trans_le' this).some
+  have : Fintype B := ((lt_aleph0_iff_fintype).1 hfin).some
+  simpa using Finset.card_lt_card <| Set.toFinset_ssubset_toFinset.mpr hlt
+
+lemma card_ssubset {A B : Set α} {hfin : #A < ℵ₀} (hlt : A < B) : #A < #B := by
+  rcases lt_or_ge #B ℵ₀ with hfin | hinf
+  · exact card_ssubset' (hfin := hfin) hlt
+  · exact lt_of_lt_of_le hfin hinf
+
 theorem le_mk_diff_add_mk (S T : Set α) : #S ≤ #(S \ T : Set α) + #T :=
   (mk_le_mk_of_subset <| subset_diff_union _ _).trans <| mk_union_le _ _