From c803cc9d92f00605db3f0a31d558127f25c84520 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Tue, 21 Jan 2025 12:27:21 -0500
Subject: [PATCH 01/13] initial

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 259 +++++++++++++++++++-----
 1 file changed, 206 insertions(+), 53 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index b12a9f56efadbb..ba375f16c41aaf 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -3,46 +3,118 @@ Copyright (c) 2025 Peter Nelson and Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Peter Nelson, Junyan Xu
 -/
-import Mathlib.Data.Matroid.Restrict
+import Mathlib.Data.Matroid.Closure
+import Mathlib.Data.Matroid.Map
 import Mathlib.SetTheory.Cardinal.Arithmetic
 
 /-!
-# Invariance of cardinality of bases of a finitary matroid
+# Cardinal-valued rank
 
 In a finitary matroid, all bases have the same cardinality.
-In fact, something stronger holds: if `B` and `B'` are bases, then `#(B \ B') = #(B' \ B)`.
-This file provides proofs of these facts,
-as well as variants when each of `B` and `B'` is a `Basis` or `Basis'` of some common set `X`.
+In fact, something stronger holds: if `I` and `J` are both bases for a set `X`,
+then `#I = #J` and, in fact, `#(I \ J) = #(J \ I)`.
+This file introduces a typeclass `CardinalRank` that applies to any matroid
+such that this property holds for all `I`, `J` and `X`.
 
-Some extra assumption like `Finitary` is necessary for these to be true,
+A matroid `M` satisfying this condition has a well-defined cardinality-valued rank function,
+both for the matroid itself and all its minors.
+
+# Main Declarations
+
+* `Matroid.CardinalRank` : a typeclass capturing the idea that a matroid and all its minors
+  have a well-defined cardinal-valued rank function.
+* `Matroid.cardRank M` is the rank of a matroid `M`, as a `Cardinal`.
+* `Matroid.cardRk M X` is the rank of a set `X` in a matroid `M`, as a `Cardinal`.
+* `cardinalRank_of_finitary` is the instance showing that `Finitary` matroids are `CardinalRank`.
+* `cardRk_inter_add_cardRk_union_le` : cardinal rank is submodular.
+
+# Notes
+
+It is not the case that all matroids are `CardinalRank`,
 since the equicardinality of bases in general matroids is independent of ZFC
 (see the docstring of `Data.Matroid.Basic`).
-Lemmas like `Matroid.Base.cardinalMk_diff_comm_of_finitary`
-become true for all matroids if they are weakened by replacing `Cardinal.mk`
+Lemmas like `Matroid.Base.cardinalMk_diff_comm` become true for all matroids
+only if they are weakened by replacing `Cardinal.mk`
 with the cruder `ℕ∞`-valued `encard`; see, for example, `Matroid.Base.encard_diff_comm`.
 
-TODO
+# TODO
 
 * Higg's theorem that, if the generalized continuum hypothesis holds,
   all bases of any matroid are equicardinal.
-* API for a `Cardinal`-valued rank function.
 -/
 
-variable {α : Type*} {M : Matroid α} {I J B B' X : Set α} [M.Finitary]
+variable {α : Type*} {M : Matroid α} {I J B B' X Y : Set α}
+
+universe u
 
 open Cardinal Set
 
 namespace Matroid
 
-theorem Base.cardinalMk_diff_comm_of_finitary (hB : M.Base B) (hB' : M.Base B') :
-    #(B \ B' : Set α) = #(B' \ B : Set α) := by
-  wlog hge : #(B' \ B : Set α) ≤ #(B \ B' : Set α) with aux
-  · exact (aux hB' hB (not_le.1 hge).le).symm
+section Basic
+
+/-- A class stating that cardinality-valued rank is well-defined for a matroid `M` and its minors.
+This holds for `Finitary` matroids.  -/
+@[mk_iff]
+class CardinalRank (M : Matroid α) : Prop where
+  forall_card_base_diff : ∀ ⦃I J X⦄, M.Basis I X → M.Basis J X → #(I \ J : Set α) = #(J \ I : Set α)
+
+variable [CardinalRank M]
+
+theorem Basis.cardinalMk_diff_comm (hIX : M.Basis I X) (hJX : M.Basis J X) :
+    #(I \ J : Set α) = #(J \ I : Set α) :=
+  CardinalRank.forall_card_base_diff hIX hJX
+
+theorem Basis'.cardinalMk_diff_comm (hIX : M.Basis' I X) (hJX : M.Basis' J X) :
+    #(I \ J : Set α) = #(J \ I : Set α) :=
+  hIX.basis_inter_ground.cardinalMk_diff_comm hJX.basis_inter_ground
+
+theorem Base.cardinalMk_diff_comm (hB : M.Base B) (hB' : M.Base B') :
+    #(B \ B' : Set α) = #(B' \ B : Set α) :=
+  hB.basis_ground.cardinalMk_diff_comm hB'.basis_ground
+
+theorem Basis.cardinalMk_eq (hIX : M.Basis I X) (hJX : M.Basis J X) : #I = #J := by
+  rw [← diff_union_inter I J,
+    mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_right),
+    hIX.cardinalMk_diff_comm hJX,
+    ← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),
+    inter_comm, diff_union_inter]
+
+theorem Basis'.cardinalMk_eq (hIX : M.Basis' I X) (hJX : M.Basis' J X) : #I = #J :=
+  hIX.basis_inter_ground.cardinalMk_eq hJX.basis_inter_ground
+
+theorem Base.cardinalMk_eq (hB : M.Base B) (hB' : M.Base B') : #B = #B' :=
+  hB.basis_ground.cardinalMk_eq hB'.basis_ground
+
+theorem Indep.cardinalMk_le_base (hI : M.Indep I) (hB : M.Base B) : #I ≤ #B :=
+  have ⟨_B', hB', hIB'⟩ := hI.exists_base_superset
+  hB'.cardinalMk_eq hB ▸ mk_le_mk_of_subset hIB'
+
+theorem Indep.cardinalMk_le_basis' (hI : M.Indep I) (hJ : M.Basis' J X) (hIX : I ⊆ X) :
+    #I ≤ #J :=
+  have ⟨_J', hJ', hIJ'⟩ := hI.subset_basis'_of_subset hIX
+  hJ'.cardinalMk_eq hJ ▸ mk_le_mk_of_subset hIJ'
+
+theorem Indep.cardinalMk_le_basis (hI : M.Indep I) (hJ : M.Basis J X) (hIX : I ⊆ X) :
+    #I ≤ #J :=
+  hI.cardinalMk_le_basis' hJ.basis' hIX
+
+end Basic
+
+section Instances
+
+/-- `Finitary` matroids have a cardinality-valued rank function. -/
+instance cardinalRank_of_finitary [Finitary M] : CardinalRank M := by
+  suffices aux : ∀ ⦃B B'⦄ ⦃N : Matroid α⦄, Finitary N → N.Base B → N.Base B' →
+      #(B \ B' : Set α) ≤ #(B' \ B : Set α) from
+    ⟨fun I J X hI hJ ↦ (aux (restrict_finitary X) hI.base_restrict hJ.base_restrict).antisymm
+      (aux (restrict_finitary X) hJ.base_restrict hI.base_restrict)⟩
+  intro B B' N hfin hB hB'
   by_cases h : (B' \ B).Finite
   · rw [← cast_ncard h, ← cast_ncard, hB.ncard_diff_comm hB']
-    exact (diff_finite_comm hB' hB).mp h
+    exact (hB'.diff_finite_comm hB).mp h
   rw [← Set.Infinite, ← infinite_coe_iff] at h
-  have (a : α) (ha : a ∈ B' \ B) : ∃ S : Set α, Finite S ∧ S ⊆ B ∧ ¬ M.Indep (insert a S) := by
+  have (a : α) (ha : a ∈ B' \ B) : ∃ S : Set α, Finite S ∧ S ⊆ B ∧ ¬ N.Indep (insert a S) := by
     have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
     contrapose! this
     exact Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.diff.to_subtype <|
@@ -50,7 +122,7 @@ theorem Base.cardinalMk_diff_comm_of_finitary (hB : M.Base B) (hB' : M.Base B')
   choose S S_fin hSB dep using this
   let U := ⋃ a : ↥(B' \ B), S a a.2
   suffices B \ B' ⊆ U by
-    refine hge.antisymm' <| (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
+    refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
       <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
     simp only [sup_le_iff, le_refl, true_and]
     exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp
@@ -63,40 +135,121 @@ theorem Base.cardinalMk_diff_comm_of_finitary (hB : M.Base B) (hB' : M.Base B')
   refine dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)
   exact subset_iUnion_of_subset ⟨a, this⟩ subset_rfl
 
-theorem Base.cardinalMk_eq_of_finitary (hB : M.Base B) (hB' : M.Base B') : #B = #B' := by
-  rw [← diff_union_inter B B',
-    mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_right),
-    hB.cardinalMk_diff_comm_of_finitary hB',
-    ← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),
-    inter_comm, diff_union_inter]
-
-theorem Basis'.cardinalMk_diff_comm_of_finitary (hIX : M.Basis' I X) (hJX : M.Basis' J X) :
-    #(I \ J : Set α) = #(J \ I : Set α) := by
-  rw [← base_restrict_iff'] at hIX hJX
-  rw [hIX.cardinalMk_diff_comm_of_finitary hJX]
-
-theorem Basis.cardinalMk_diff_comm_of_finitary (hIX : M.Basis I X) (hJX : M.Basis J X) :
-    #(I \ J : Set α) = #(J \ I : Set α) :=
-  hIX.basis'.cardinalMk_diff_comm_of_finitary hJX.basis'
-
-theorem Basis'.cardinalMk_eq_of_finitary (hIX : M.Basis' I X) (hJX : M.Basis' J X) : #I = #J := by
-  rw [← base_restrict_iff'] at hIX hJX
-  rw [hIX.cardinalMk_eq_of_finitary hJX]
-
-theorem Basis.cardinalMk_eq_of_finitary (hIX : M.Basis I X) (hJX : M.Basis J X) : #I = #J :=
-  hIX.basis'.cardinalMk_eq_of_finitary hJX.basis'
-
-theorem Indep.cardinalMk_le_base_of_finitary (hI : M.Indep I) (hB : M.Base B) : #I ≤ #B :=
-  have ⟨_B', hB', hIB'⟩ := hI.exists_base_superset
-  hB'.cardinalMk_eq_of_finitary hB ▸ mk_le_mk_of_subset hIB'
-
-theorem Indep.cardinalMk_le_basis'_of_finitary (hI : M.Indep I) (hJ : M.Basis' J X) (hIX : I ⊆ X) :
-    #I ≤ #J :=
-  have ⟨_J', hJ', hIJ'⟩ := hI.subset_basis'_of_subset hIX
-  hJ'.cardinalMk_eq_of_finitary hJ ▸ mk_le_mk_of_subset hIJ'
-
-theorem Indep.cardinalMk_le_basis_of_finitary (hI : M.Indep I) (hJ : M.Basis J X) (hIX : I ⊆ X) :
-    #I ≤ #J :=
-  hI.cardinalMk_le_basis'_of_finitary hJ.basis' hIX
+/-- Restrictions of matroids with cardinal rank functions have cardinal rank functions- -/
+instance cardinalRank_restrict [CardinalRank M] : CardinalRank (M ↾ X) := by
+  refine ⟨fun I J Y hI hJ ↦ ?_⟩
+  rw [basis_restrict_iff'] at hI hJ
+  exact hI.1.cardinalMk_diff_comm hJ.1
+
+instance cardinalRank_map {α β : Type u} {f : α → β} (M : Matroid α) [CardinalRank M]
+    (hf : InjOn f M.E) : CardinalRank (M.map f hf) := by
+  refine ⟨fun I J X hI hJ ↦ ?_⟩
+  obtain ⟨I, X, hIX, rfl, rfl⟩ := map_basis_iff'.1 hI
+  obtain ⟨J, X', hJX, rfl, h'⟩ := map_basis_iff'.1 hJ
+  obtain rfl : X = X' := by
+    rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
+  have hcard := hIX.cardinalMk_diff_comm hJX
+  rwa [← mk_image_eq_of_injOn _ _ (hf.mono (diff_subset.trans hIX.indep.subset_ground)),
+    ← mk_image_eq_of_injOn _ _ (hf.mono (diff_subset.trans hJX.indep.subset_ground)),
+    (hf.mono hIX.indep.subset_ground).image_diff,
+    (hf.mono hJX.indep.subset_ground).image_diff, inter_comm,
+    hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
+    diff_inter_self_eq_diff, diff_self_inter] at hcard
+
+end Instances
+
+section Rank
+
+/-- The rank (size of a base) of a matroid `M` as a `Cardinal`. -/
+def cardRank (M : Matroid α) := #(M.exists_base.choose)
+
+/-- The rank (size of a basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
+def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
+
+variable [CardinalRank M]
+
+theorem Base.cardRank_eq_cardinalMk (hB : M.Base B) : M.cardRank = #B :=
+  M.exists_base.choose_spec.cardinalMk_eq hB
+
+theorem Basis'.cardRk_eq_cardinalMk (hIX : M.Basis' I X) : M.cardRk X = #I :=
+  (M ↾ X).exists_base.choose_spec.cardinalMk_eq (base_restrict_iff'.2 hIX)
+
+theorem Basis.cardRk_eq_cardinalMk (hIX : M.Basis I X) : M.cardRk X = #I:=
+  hIX.basis'.cardRk_eq_cardinalMk
+
+@[simp] theorem cardRank_restrict (M : Matroid α) [CardinalRank M] :
+    (M ↾ X).cardRank = M.cardRk X := rfl
+
+@[simp] theorem cardRk_ground (M : Matroid α) [CardinalRank M] : M.cardRk M.E = M.cardRank := by
+  rw [cardRk, restrict_ground_eq_self]
+
+theorem cardRk_mono (M : Matroid α) [CardinalRank M] : Monotone M.cardRk := by
+  intro X Y (hXY : X ⊆ Y)
+  obtain ⟨I, hI⟩ := M.exists_basis' X
+  obtain ⟨J, hJ⟩ := M.exists_basis' Y
+  rw [hI.cardRk_eq_cardinalMk, hJ.cardRk_eq_cardinalMk]
+  exact hI.indep.cardinalMk_le_basis' hJ (hI.subset.trans hXY)
+
+theorem cardRk_le_of_subset (M : Matroid α) [CardinalRank M] (hXY : X ⊆ Y) :
+    M.cardRk X ≤ M.cardRk Y :=
+  M.cardRk_mono hXY
+
+theorem cardRk_le_cardinalMk (M : Matroid α) [CardinalRank M] (X : Set α) : M.cardRk X ≤ #X := by
+  obtain ⟨I, hI⟩ := M.exists_basis' X
+  rw [hI.cardRk_eq_cardinalMk]
+  exact mk_le_mk_of_subset hI.subset
+
+theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : M.cardRk I = #I :=
+  hI.basis_self.cardRk_eq_cardinalMk
+
+@[simp] theorem cardRk_closure (M : Matroid α) [CardinalRank M] (X : Set α) :
+    M.cardRk (M.closure X) = M.cardRk X := by
+  obtain ⟨I, hI⟩ := M.exists_basis' X
+  rw [hI.basis_closure_right.cardRk_eq_cardinalMk, hI.cardRk_eq_cardinalMk]
+
+theorem cardRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cardRk X = M.cardRk Y := by
+  rw [← cardRk_closure, hXY, cardRk_closure]
+
+@[simp] theorem cardRk_union_closure_right_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
+    M.cardRk (X ∪ M.closure Y) = M.cardRk (X ∪ Y) :=
+  M.cardRk_closure_congr (M.closure_union_closure_right_eq _ _)
+
+@[simp] theorem cardRk_union_closure_left_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
+    M.cardRk (M.closure X ∪ Y) = M.cardRk (X ∪ Y) :=
+  M.cardRk_closure_congr (M.closure_union_closure_left_eq _ _)
+
+@[simp] theorem cardRk_insert_closure_eq (M : Matroid α) [CardinalRank M] (e : α) (X : Set α) :
+    M.cardRk (insert e (M.closure X)) = M.cardRk (insert e X) := by
+  rw [← union_singleton, cardRk_union_closure_left_eq, union_singleton]
+
+theorem cardRk_union_closure_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
+    M.cardRk (M.closure X ∪ M.closure Y) = M.cardRk (X ∪ Y) := by
+  simp
+
+@[simp] theorem cardRk_inter_ground (M : Matroid α) [CardinalRank M] (X : Set α) :
+    M.cardRk (X ∩ M.E) = M.cardRk X := by
+  rw [← cardRk_closure, closure_inter_ground, cardRk_closure]
+
+@[simp] theorem cardRk_map_eq {α β : Type u} {f : α → β} {X : Set α} (M : Matroid α)
+    [CardinalRank M] (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
+    (M.map f hf).cardRk (f '' X) = M.cardRk X := by
+  obtain ⟨I, hI⟩ := M.exists_basis X
+  rw [hI.cardRk_eq_cardinalMk, (hI.map hf).cardRk_eq_cardinalMk,
+    mk_image_eq_of_injOn _ _ (hf.mono hI.indep.subset_ground)]
+
+/-- The `Cardinal` rank function is submodular. -/
+theorem cardRk_inter_add_cardRk_union_le (M : Matroid α) [CardinalRank M] (X Y : Set α) :
+    M.cardRk (X ∩ Y) + M.cardRk (X ∪ Y) ≤ M.cardRk X + M.cardRk Y := by
+  obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
+  obtain ⟨IX, hIX, hIX'⟩ :=
+    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)
+  obtain ⟨IY, hIY, hIY'⟩ :=
+    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
+  rw [← cardRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
+    cardRk_union_closure_eq, hIi.cardRk_eq_cardinalMk, hIX.cardRk_eq_cardinalMk,
+    hIY.cardRk_eq_cardinalMk, ← mk_union_add_mk_inter, add_comm]
+  exact add_le_add (M.cardRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))
+
+end Rank
 
 end Matroid

From 460a555b18a49a5eb7fe21e8aa26163b7c407cdf Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Tue, 21 Jan 2025 12:36:59 -0500
Subject: [PATCH 02/13] lint

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index ba375f16c41aaf..89b9a71e21bfe4 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -177,10 +177,9 @@ theorem Basis'.cardRk_eq_cardinalMk (hIX : M.Basis' I X) : M.cardRk X = #I :=
 theorem Basis.cardRk_eq_cardinalMk (hIX : M.Basis I X) : M.cardRk X = #I:=
   hIX.basis'.cardRk_eq_cardinalMk
 
-@[simp] theorem cardRank_restrict (M : Matroid α) [CardinalRank M] :
-    (M ↾ X).cardRank = M.cardRk X := rfl
+@[simp] theorem cardRank_restrict (M : Matroid α) : (M ↾ X).cardRank = M.cardRk X := rfl
 
-@[simp] theorem cardRk_ground (M : Matroid α) [CardinalRank M] : M.cardRk M.E = M.cardRank := by
+@[simp] theorem cardRk_ground (M : Matroid α) : M.cardRk M.E = M.cardRank := by
   rw [cardRk, restrict_ground_eq_self]
 
 theorem cardRk_mono (M : Matroid α) [CardinalRank M] : Monotone M.cardRk := by

From d9d7008cbee0ff11a4767c90a59d9e79b4948df0 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Tue, 21 Jan 2025 21:50:34 -0500
Subject: [PATCH 03/13] typos

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 89b9a71e21bfe4..bfa4d71f14c4df 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -12,12 +12,12 @@ import Mathlib.SetTheory.Cardinal.Arithmetic
 
 In a finitary matroid, all bases have the same cardinality.
 In fact, something stronger holds: if `I` and `J` are both bases for a set `X`,
-then `#I = #J` and, in fact, `#(I \ J) = #(J \ I)`.
+then `#(I \ J) = #(J \ I)` and (consequently) `#I = #J`.
 This file introduces a typeclass `CardinalRank` that applies to any matroid
 such that this property holds for all `I`, `J` and `X`.
 
-A matroid `M` satisfying this condition has a well-defined cardinality-valued rank function,
-both for the matroid itself and all its minors.
+A matroid satisfying this condition has a well-defined cardinality-valued rank function,
+both for itself and all its minors.
 
 # Main Declarations
 
@@ -26,7 +26,7 @@ both for the matroid itself and all its minors.
 * `Matroid.cardRank M` is the rank of a matroid `M`, as a `Cardinal`.
 * `Matroid.cardRk M X` is the rank of a set `X` in a matroid `M`, as a `Cardinal`.
 * `cardinalRank_of_finitary` is the instance showing that `Finitary` matroids are `CardinalRank`.
-* `cardRk_inter_add_cardRk_union_le` : cardinal rank is submodular.
+* `cardRk_inter_add_cardRk_union_le` states that cardinal rank is submodular.
 
 # Notes
 
@@ -35,7 +35,7 @@ since the equicardinality of bases in general matroids is independent of ZFC
 (see the docstring of `Data.Matroid.Basic`).
 Lemmas like `Matroid.Base.cardinalMk_diff_comm` become true for all matroids
 only if they are weakened by replacing `Cardinal.mk`
-with the cruder `ℕ∞`-valued `encard`; see, for example, `Matroid.Base.encard_diff_comm`.
+with the cruder `ℕ∞`-valued `Set.encard`; see, for example, `Matroid.Base.encard_diff_comm`.
 
 # TODO
 
@@ -174,7 +174,7 @@ theorem Base.cardRank_eq_cardinalMk (hB : M.Base B) : M.cardRank = #B :=
 theorem Basis'.cardRk_eq_cardinalMk (hIX : M.Basis' I X) : M.cardRk X = #I :=
   (M ↾ X).exists_base.choose_spec.cardinalMk_eq (base_restrict_iff'.2 hIX)
 
-theorem Basis.cardRk_eq_cardinalMk (hIX : M.Basis I X) : M.cardRk X = #I:=
+theorem Basis.cardRk_eq_cardinalMk (hIX : M.Basis I X) : M.cardRk X = #I :=
   hIX.basis'.cardRk_eq_cardinalMk
 
 @[simp] theorem cardRank_restrict (M : Matroid α) : (M ↾ X).cardRank = M.cardRk X := rfl

From 312f509bb1e8ef3903cdc3200e75c289a34c5692 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Tue, 21 Jan 2025 21:52:15 -0500
Subject: [PATCH 04/13] fix

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index bfa4d71f14c4df..e73c152a15a9b9 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -57,13 +57,14 @@ section Basic
 This holds for `Finitary` matroids.  -/
 @[mk_iff]
 class CardinalRank (M : Matroid α) : Prop where
-  forall_card_base_diff : ∀ ⦃I J X⦄, M.Basis I X → M.Basis J X → #(I \ J : Set α) = #(J \ I : Set α)
+  forall_card_basis_diff :
+    ∀ ⦃I J X⦄, M.Basis I X → M.Basis J X → #(I \ J : Set α) = #(J \ I : Set α)
 
 variable [CardinalRank M]
 
 theorem Basis.cardinalMk_diff_comm (hIX : M.Basis I X) (hJX : M.Basis J X) :
     #(I \ J : Set α) = #(J \ I : Set α) :=
-  CardinalRank.forall_card_base_diff hIX hJX
+  CardinalRank.forall_card_basis_diff hIX hJX
 
 theorem Basis'.cardinalMk_diff_comm (hIX : M.Basis' I X) (hJX : M.Basis' J X) :
     #(I \ J : Set α) = #(J \ I : Set α) :=

From 9083478f39eb528af968cb81ba49590bdaf618eb Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Wed, 22 Jan 2025 20:06:43 -0500
Subject: [PATCH 05/13] Update Mathlib/Data/Matroid/Rank/Cardinal.lean

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index e73c152a15a9b9..7b30593dbd6d3d 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -32,7 +32,7 @@ both for itself and all its minors.
 
 It is not the case that all matroids are `CardinalRank`,
 since the equicardinality of bases in general matroids is independent of ZFC
-(see the docstring of `Data.Matroid.Basic`).
+(see the module docstring of `Mathlib.Data.Matroid.Basic`).
 Lemmas like `Matroid.Base.cardinalMk_diff_comm` become true for all matroids
 only if they are weakened by replacing `Cardinal.mk`
 with the cruder `ℕ∞`-valued `Set.encard`; see, for example, `Matroid.Base.encard_diff_comm`.

From a314525a958f92cc0f7d0ea7dd2411d1d94fc14a Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Thu, 23 Jan 2025 07:04:55 -0500
Subject: [PATCH 06/13] comments

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 40 +++++++++++++------------
 1 file changed, 21 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 7b30593dbd6d3d..d5f45b9ce58efe 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -39,7 +39,7 @@ with the cruder `ℕ∞`-valued `Set.encard`; see, for example, `Matroid.Base.en
 
 # TODO
 
-* Higg's theorem that, if the generalized continuum hypothesis holds,
+* Higgs' theorem that, if the generalized continuum hypothesis holds,
   all bases of any matroid are equicardinal.
 -/
 
@@ -161,22 +161,24 @@ end Instances
 
 section Rank
 
-/-- The rank (size of a base) of a matroid `M` as a `Cardinal`. -/
-def cardRank (M : Matroid α) := #(M.exists_base.choose)
+/-- The rank (size of an arbitrarily chosen base) of a matroid `M` as a `Cardinal`. -/
+noncomputable def cardRank (M : Matroid α) := ⨆ (B : {B : Set α // M.Base B}), #B
 
-/-- The rank (size of a basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
-def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
+/-- The rank (size of an arbitrary basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
+noncomputable def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
 
 variable [CardinalRank M]
 
-theorem Base.cardRank_eq_cardinalMk (hB : M.Base B) : M.cardRank = #B :=
-  M.exists_base.choose_spec.cardinalMk_eq hB
+theorem Base.cardinalMk_eq_cardRank (hB : M.Base B) : #B = M.cardRank := by
+  have : Nonempty {B : Set α // M.Base B} := ⟨M.exists_base.choose, M.exists_base.choose_spec⟩
+  have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
+  simp [cardRank, hrw]
 
-theorem Basis'.cardRk_eq_cardinalMk (hIX : M.Basis' I X) : M.cardRk X = #I :=
-  (M ↾ X).exists_base.choose_spec.cardinalMk_eq (base_restrict_iff'.2 hIX)
+theorem Basis'.cardinalMk_eq_cardRk (hIX : M.Basis' I X) : #I = M.cardRk X := by
+  rw [cardRk, (base_restrict_iff'.2 hIX).cardinalMk_eq_cardRank]
 
-theorem Basis.cardRk_eq_cardinalMk (hIX : M.Basis I X) : M.cardRk X = #I :=
-  hIX.basis'.cardRk_eq_cardinalMk
+theorem Basis.cardinalMk_eq_cardRk (hIX : M.Basis I X) : #I = M.cardRk X :=
+  hIX.basis'.cardinalMk_eq_cardRk
 
 @[simp] theorem cardRank_restrict (M : Matroid α) : (M ↾ X).cardRank = M.cardRk X := rfl
 
@@ -187,7 +189,7 @@ theorem cardRk_mono (M : Matroid α) [CardinalRank M] : Monotone M.cardRk := by
   intro X Y (hXY : X ⊆ Y)
   obtain ⟨I, hI⟩ := M.exists_basis' X
   obtain ⟨J, hJ⟩ := M.exists_basis' Y
-  rw [hI.cardRk_eq_cardinalMk, hJ.cardRk_eq_cardinalMk]
+  rw [← hI.cardinalMk_eq_cardRk, ← hJ.cardinalMk_eq_cardRk]
   exact hI.indep.cardinalMk_le_basis' hJ (hI.subset.trans hXY)
 
 theorem cardRk_le_of_subset (M : Matroid α) [CardinalRank M] (hXY : X ⊆ Y) :
@@ -196,16 +198,16 @@ theorem cardRk_le_of_subset (M : Matroid α) [CardinalRank M] (hXY : X ⊆ Y) :
 
 theorem cardRk_le_cardinalMk (M : Matroid α) [CardinalRank M] (X : Set α) : M.cardRk X ≤ #X := by
   obtain ⟨I, hI⟩ := M.exists_basis' X
-  rw [hI.cardRk_eq_cardinalMk]
+  rw [← hI.cardinalMk_eq_cardRk]
   exact mk_le_mk_of_subset hI.subset
 
-theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : M.cardRk I = #I :=
-  hI.basis_self.cardRk_eq_cardinalMk
+theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cardRk I :=
+  hI.basis_self.cardinalMk_eq_cardRk
 
 @[simp] theorem cardRk_closure (M : Matroid α) [CardinalRank M] (X : Set α) :
     M.cardRk (M.closure X) = M.cardRk X := by
   obtain ⟨I, hI⟩ := M.exists_basis' X
-  rw [hI.basis_closure_right.cardRk_eq_cardinalMk, hI.cardRk_eq_cardinalMk]
+  rw [← hI.basis_closure_right.cardinalMk_eq_cardRk, ← hI.cardinalMk_eq_cardRk]
 
 theorem cardRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cardRk X = M.cardRk Y := by
   rw [← cardRk_closure, hXY, cardRk_closure]
@@ -234,7 +236,7 @@ theorem cardRk_union_closure_eq (M : Matroid α) [CardinalRank M] (X Y : Set α)
     [CardinalRank M] (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
     (M.map f hf).cardRk (f '' X) = M.cardRk X := by
   obtain ⟨I, hI⟩ := M.exists_basis X
-  rw [hI.cardRk_eq_cardinalMk, (hI.map hf).cardRk_eq_cardinalMk,
+  rw [← hI.cardinalMk_eq_cardRk, ← (hI.map hf).cardinalMk_eq_cardRk,
     mk_image_eq_of_injOn _ _ (hf.mono hI.indep.subset_ground)]
 
 /-- The `Cardinal` rank function is submodular. -/
@@ -246,8 +248,8 @@ theorem cardRk_inter_add_cardRk_union_le (M : Matroid α) [CardinalRank M] (X Y
   obtain ⟨IY, hIY, hIY'⟩ :=
     hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
   rw [← cardRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
-    cardRk_union_closure_eq, hIi.cardRk_eq_cardinalMk, hIX.cardRk_eq_cardinalMk,
-    hIY.cardRk_eq_cardinalMk, ← mk_union_add_mk_inter, add_comm]
+    cardRk_union_closure_eq, ← hIi.cardinalMk_eq_cardRk, ← hIX.cardinalMk_eq_cardRk,
+    ← hIY.cardinalMk_eq_cardRk, ← mk_union_add_mk_inter, add_comm]
   exact add_le_add (M.cardRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))
 
 end Rank

From 4a30db293d2ce919a87a83af606009f6ebd767ea Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Thu, 23 Jan 2025 07:14:55 -0500
Subject: [PATCH 07/13] docstring

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index d5f45b9ce58efe..b80756e2f7e8a8 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -161,10 +161,10 @@ end Instances
 
 section Rank
 
-/-- The rank (size of an arbitrarily chosen base) of a matroid `M` as a `Cardinal`. -/
+/-- The rank (size of a largest base) of a matroid `M` as a `Cardinal`. -/
 noncomputable def cardRank (M : Matroid α) := ⨆ (B : {B : Set α // M.Base B}), #B
 
-/-- The rank (size of an arbitrary basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
+/-- The rank (size of a largest basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
 noncomputable def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
 
 variable [CardinalRank M]

From 02de685fcd3fda9e627f61a8f016350f70d24078 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Thu, 23 Jan 2025 09:52:49 -0500
Subject: [PATCH 08/13] remove typeclass assumptions

---
 Mathlib/Data/Matroid/Basic.lean         |   3 +
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 102 ++++++++++++++++--------
 2 files changed, 70 insertions(+), 35 deletions(-)

diff --git a/Mathlib/Data/Matroid/Basic.lean b/Mathlib/Data/Matroid/Basic.lean
index 4c8032518f51d6..2a28738e5a3a1d 100644
--- a/Mathlib/Data/Matroid/Basic.lean
+++ b/Mathlib/Data/Matroid/Basic.lean
@@ -217,6 +217,9 @@ namespace Matroid
 
 variable {α : Type*} {M : Matroid α}
 
+instance (M : Matroid α) : Nonempty {B // M.Base B} :=
+  nonempty_subtype.2 M.exists_base
+
 /-- Typeclass for a matroid having finite ground set. Just a wrapper for `M.E.Finite`-/
 @[mk_iff] protected class Finite (M : Matroid α) : Prop where
   /-- The ground set is finite -/
diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index b80756e2f7e8a8..313ddf52dba920 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -162,47 +162,90 @@ end Instances
 section Rank
 
 /-- The rank (size of a largest base) of a matroid `M` as a `Cardinal`. -/
-noncomputable def cardRank (M : Matroid α) := ⨆ (B : {B : Set α // M.Base B}), #B
+noncomputable def cardRank (M : Matroid α) := ⨆ (B : {B // M.Base B}), #B
 
 /-- The rank (size of a largest basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
 noncomputable def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
 
-variable [CardinalRank M]
+theorem Base.cardinalMk_le_cardRank (hB : M.Base B) : #B ≤ M.cardRank :=
+  le_ciSup (f := fun (B : {B // M.Base B}) ↦ #(B.1)) (bddAbove_range _) ⟨B, hB⟩
 
-theorem Base.cardinalMk_eq_cardRank (hB : M.Base B) : #B = M.cardRank := by
-  have : Nonempty {B : Set α // M.Base B} := ⟨M.exists_base.choose, M.exists_base.choose_spec⟩
-  have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
-  simp [cardRank, hrw]
+theorem Basis'.cardinalMk_le_cardRk (hIX : M.Basis' I X) : #I ≤ M.cardRk X :=
+  (base_restrict_iff'.2 hIX).cardinalMk_le_cardRank
 
-theorem Basis'.cardinalMk_eq_cardRk (hIX : M.Basis' I X) : #I = M.cardRk X := by
-  rw [cardRk, (base_restrict_iff'.2 hIX).cardinalMk_eq_cardRank]
+theorem Basis.cardinalMk_le_cardRk (hIX : M.Basis I X) : #I ≤ M.cardRk X :=
+  hIX.basis'.cardinalMk_le_cardRk
 
-theorem Basis.cardinalMk_eq_cardRk (hIX : M.Basis I X) : #I = M.cardRk X :=
-  hIX.basis'.cardinalMk_eq_cardRk
+theorem cardRank_le_iff {κ : Cardinal} : M.cardRank ≤ κ ↔ ∀ ⦃B⦄, M.Base B → #B ≤ κ :=
+  ⟨fun h _ hB ↦ (hB.cardinalMk_le_cardRank.trans h), fun h ↦ ciSup_le fun ⟨_, hB⟩ ↦ h hB⟩
+
+theorem cardRk_le_iff {κ : Cardinal} : M.cardRk X ≤ κ ↔ ∀ ⦃I⦄, M.Basis' I X → #I ≤ κ := by
+  simp_rw [cardRk, cardRank_le_iff, base_restrict_iff']
 
-@[simp] theorem cardRank_restrict (M : Matroid α) : (M ↾ X).cardRank = M.cardRk X := rfl
+theorem Indep.cardinalMk_le_cardRk_of_subset (hI : M.Indep I) (hIX : I ⊆ X) : #I ≤ M.cardRk X :=
+  let ⟨_, hJ, hIJ⟩ := hI.subset_basis'_of_subset hIX
+  (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cardRk
+
+theorem cardRk_le_cardinalMk (M : Matroid α) (X : Set α) : M.cardRk X ≤ #X :=
+  ciSup_le fun ⟨_, hI⟩ ↦ mk_le_mk_of_subset hI.subset_ground
 
 @[simp] theorem cardRk_ground (M : Matroid α) : M.cardRk M.E = M.cardRank := by
   rw [cardRk, restrict_ground_eq_self]
 
-theorem cardRk_mono (M : Matroid α) [CardinalRank M] : Monotone M.cardRk := by
-  intro X Y (hXY : X ⊆ Y)
-  obtain ⟨I, hI⟩ := M.exists_basis' X
-  obtain ⟨J, hJ⟩ := M.exists_basis' Y
-  rw [← hI.cardinalMk_eq_cardRk, ← hJ.cardinalMk_eq_cardRk]
-  exact hI.indep.cardinalMk_le_basis' hJ (hI.subset.trans hXY)
+@[simp] theorem cardRank_restrict (M : Matroid α) (X : Set α) : (M ↾ X).cardRank = M.cardRk X := rfl
+
+theorem cardRk_mono (M : Matroid α) : Monotone M.cardRk := by
+  simp only [Monotone, le_eq_subset, cardRk_le_iff]
+  intro X Y hXY I hIX
+  obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_basis'_of_subset (hIX.subset.trans hXY)
+  exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cardRk
 
-theorem cardRk_le_of_subset (M : Matroid α) [CardinalRank M] (hXY : X ⊆ Y) :
-    M.cardRk X ≤ M.cardRk Y :=
+theorem cardRk_le_of_subset (M : Matroid α) (hXY : X ⊆ Y) : M.cardRk X ≤ M.cardRk Y :=
   M.cardRk_mono hXY
 
-theorem cardRk_le_cardinalMk (M : Matroid α) [CardinalRank M] (X : Set α) : M.cardRk X ≤ #X := by
-  obtain ⟨I, hI⟩ := M.exists_basis' X
-  rw [← hI.cardinalMk_eq_cardRk]
-  exact mk_le_mk_of_subset hI.subset
+@[simp] theorem cardRk_inter_ground (M : Matroid α) (X : Set α) :
+    M.cardRk (X ∩ M.E) = M.cardRk X :=
+  (M.cardRk_le_of_subset inter_subset_left).antisymm <|
+    cardRk_le_iff.2 fun _ h ↦ h.basis_inter_ground.cardinalMk_le_cardRk
+
+theorem cardRk_restrict_subset (M : Matroid α) (hYX : Y ⊆ X) : (M ↾ X).cardRk Y = M.cardRk Y := by
+  have aux : ∀ ⦃I⦄, M.Basis' I Y ↔ (M ↾ X).Basis' I Y := by
+    simp_rw [basis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
+    exact fun I h ↦ h.subset.trans hYX
+  simp_rw [le_antisymm_iff, cardRk_le_iff]
+  exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cardRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cardRk⟩
+
+theorem cardRk_restrict (M : Matroid α) (X Y : Set α) : (M ↾ X).cardRk Y = M.cardRk (X ∩ Y) := by
+  rw [← cardRk_inter_ground, restrict_ground_eq, cardRk_restrict_subset _ inter_subset_right,
+    inter_comm]
 
 theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cardRk I :=
-  hI.basis_self.cardinalMk_eq_cardRk
+  (M.cardRk_le_cardinalMk I).antisymm' (hI.basis_self.cardinalMk_le_cardRk)
+
+@[simp] theorem cardRk_map_eq {α β : Type u} {f : α → β} {X : Set α} (M : Matroid α)
+    [CardinalRank M] (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
+    (M.map f hf).cardRk (f '' X) = M.cardRk X := by
+  simp_rw [le_antisymm_iff, cardRk_le_iff, basis'_iff_basis hX,
+    basis'_iff_basis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
+  refine ⟨fun I hI ↦ ?_, fun I hI ↦ le_of_eq_of_le ?_ (hI.map hf).cardinalMk_le_cardRk ⟩
+  · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_basis_iff'.1 hI
+    obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
+    rw [mk_image_eq_of_injOn _ _ (hf.mono hIX.indep.subset_ground)]
+    exact hIX.cardinalMk_le_cardRk
+  rw [mk_image_eq_of_injOn _ _ (hf.mono hI.indep.subset_ground)]
+
+variable [CardinalRank M]
+
+theorem Base.cardinalMk_eq_cardRank (hB : M.Base B) : #B = M.cardRank := by
+  have : Nonempty {B : Set α // M.Base B} := ⟨M.exists_base.choose, M.exists_base.choose_spec⟩
+  have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
+  simp [cardRank, hrw]
+
+theorem Basis'.cardinalMk_eq_cardRk (hIX : M.Basis' I X) : #I = M.cardRk X := by
+  rw [cardRk, (base_restrict_iff'.2 hIX).cardinalMk_eq_cardRank]
+
+theorem Basis.cardinalMk_eq_cardRk (hIX : M.Basis I X) : #I = M.cardRk X :=
+  hIX.basis'.cardinalMk_eq_cardRk
 
 @[simp] theorem cardRk_closure (M : Matroid α) [CardinalRank M] (X : Set α) :
     M.cardRk (M.closure X) = M.cardRk X := by
@@ -228,17 +271,6 @@ theorem cardRk_union_closure_eq (M : Matroid α) [CardinalRank M] (X Y : Set α)
     M.cardRk (M.closure X ∪ M.closure Y) = M.cardRk (X ∪ Y) := by
   simp
 
-@[simp] theorem cardRk_inter_ground (M : Matroid α) [CardinalRank M] (X : Set α) :
-    M.cardRk (X ∩ M.E) = M.cardRk X := by
-  rw [← cardRk_closure, closure_inter_ground, cardRk_closure]
-
-@[simp] theorem cardRk_map_eq {α β : Type u} {f : α → β} {X : Set α} (M : Matroid α)
-    [CardinalRank M] (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
-    (M.map f hf).cardRk (f '' X) = M.cardRk X := by
-  obtain ⟨I, hI⟩ := M.exists_basis X
-  rw [← hI.cardinalMk_eq_cardRk, ← (hI.map hf).cardinalMk_eq_cardRk,
-    mk_image_eq_of_injOn _ _ (hf.mono hI.indep.subset_ground)]
-
 /-- The `Cardinal` rank function is submodular. -/
 theorem cardRk_inter_add_cardRk_union_le (M : Matroid α) [CardinalRank M] (X Y : Set α) :
     M.cardRk (X ∩ Y) + M.cardRk (X ∪ Y) ≤ M.cardRk X + M.cardRk Y := by

From b95b4757d29ab2e2ca8f0ee514c5c850d47613ff Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Thu, 23 Jan 2025 11:00:59 -0500
Subject: [PATCH 09/13] fix

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 313ddf52dba920..6212c30de11c57 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -223,7 +223,7 @@ theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cardRk I :=
   (M.cardRk_le_cardinalMk I).antisymm' (hI.basis_self.cardinalMk_le_cardRk)
 
 @[simp] theorem cardRk_map_eq {α β : Type u} {f : α → β} {X : Set α} (M : Matroid α)
-    [CardinalRank M] (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
+    (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
     (M.map f hf).cardRk (f '' X) = M.cardRk X := by
   simp_rw [le_antisymm_iff, cardRk_le_iff, basis'_iff_basis hX,
     basis'_iff_basis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]

From 37b4115e6239b496ed7ed8ba0b5b311908cdc6a0 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Thu, 23 Jan 2025 11:03:40 -0500
Subject: [PATCH 10/13] fix

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 6212c30de11c57..312b2fdcd72815 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -237,7 +237,6 @@ theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cardRk I :=
 variable [CardinalRank M]
 
 theorem Base.cardinalMk_eq_cardRank (hB : M.Base B) : #B = M.cardRank := by
-  have : Nonempty {B : Set α // M.Base B} := ⟨M.exists_base.choose, M.exists_base.choose_spec⟩
   have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
   simp [cardRank, hrw]
 

From dfe549a70e300790a2d4dd93c3081a22f9793618 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Sun, 26 Jan 2025 11:00:25 -0500
Subject: [PATCH 11/13] heterogeneity/naming

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 373 ++++++++++++++----------
 1 file changed, 216 insertions(+), 157 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 312b2fdcd72815..d337d9a50d93be 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -13,7 +13,7 @@ import Mathlib.SetTheory.Cardinal.Arithmetic
 In a finitary matroid, all bases have the same cardinality.
 In fact, something stronger holds: if `I` and `J` are both bases for a set `X`,
 then `#(I \ J) = #(J \ I)` and (consequently) `#I = #J`.
-This file introduces a typeclass `CardinalRank` that applies to any matroid
+This file introduces a typeclass `InvariantCardinalRank` that applies to any matroid
 such that this property holds for all `I`, `J` and `X`.
 
 A matroid satisfying this condition has a well-defined cardinality-valued rank function,
@@ -21,50 +21,173 @@ both for itself and all its minors.
 
 # Main Declarations
 
-* `Matroid.CardinalRank` : a typeclass capturing the idea that a matroid and all its minors
-  have a well-defined cardinal-valued rank function.
-* `Matroid.cardRank M` is the rank of a matroid `M`, as a `Cardinal`.
-* `Matroid.cardRk M X` is the rank of a set `X` in a matroid `M`, as a `Cardinal`.
-* `cardinalRank_of_finitary` is the instance showing that `Finitary` matroids are `CardinalRank`.
-* `cardRk_inter_add_cardRk_union_le` states that cardinal rank is submodular.
+* `Matroid.InvariantCardinalRank` : a typeclass capturing the idea that a matroid and all its minors
+  have a well-behaved cardinal-valued rank function.
+* `Matroid.cRank M` is the supremum of the cardinalities of the bases of matroid `M`.
+* `Matroid.cRk M X` is the supremum of the cardinalities of the bases of a set `X` in a matroid `M`.
+* `invariantCardinalRank_of_finitary` is the instance
+   showing that `Finitary` matroids are `InvariantCardinalRank`.
+* `cRk_inter_add_cRk_union_le` states that cardinal rank is submodular.
 
 # Notes
 
-It is not the case that all matroids are `CardinalRank`,
+It is not the case that all matroids are `InvariantCardinalRank`,
 since the equicardinality of bases in general matroids is independent of ZFC
 (see the module docstring of `Mathlib.Data.Matroid.Basic`).
 Lemmas like `Matroid.Base.cardinalMk_diff_comm` become true for all matroids
 only if they are weakened by replacing `Cardinal.mk`
 with the cruder `ℕ∞`-valued `Set.encard`; see, for example, `Matroid.Base.encard_diff_comm`.
 
+# Implementation Details
+
+Since the functions `cRank` and `cRk` are defined as suprema,
+independently of the `Matroid.InvariantCardinalRank` typeclass,
+they are well-defined for all matroids.
+However, for matroids that do not satisfy `InvariantCardinalRank`, they are badly behaved.
+For instance, in general `cRk` is not submodular,
+and its value may differ on a set `X` and the closure of `X`.
+We state and prove theorems without the instance whenever possible,
+which sometime makes their proofs longer than they would be without the instance.
+
 # TODO
 
-* Higgs' theorem that, if the generalized continuum hypothesis holds,
-  all bases of any matroid are equicardinal.
+* Higgs' theorem : if the generalized continuum hypothesis holds,
+  then every matroid is `InvariantCardinalRank`.
+
 -/
 
-variable {α : Type*} {M : Matroid α} {I J B B' X Y : Set α}
+universe u v
 
-universe u
+variable {α : Type u} {β : Type v} {f : α → β} {M : Matroid α} {I J B B' X Y : Set α}
 
 open Cardinal Set
 
 namespace Matroid
 
-section Basic
+section Rank
+
+variable {κ : Cardinal}
+
+/-- The rank (size of a largest base) of a matroid `M` as a `Cardinal`. -/
+noncomputable def cRank (M : Matroid α) := ⨆ (B : {B // M.Base B}), #B
+
+/-- The rank (size of a largest basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
+noncomputable def cRk (M : Matroid α) (X : Set α) := (M ↾ X).cRank
+
+theorem Base.cardinalMk_le_cRank (hB : M.Base B) : #B ≤ M.cRank :=
+  le_ciSup (f := fun (B : {B // M.Base B}) ↦ #(B.1)) (bddAbove_range _) ⟨B, hB⟩
+
+theorem Basis'.cardinalMk_le_cRk (hIX : M.Basis' I X) : #I ≤ M.cRk X :=
+  (base_restrict_iff'.2 hIX).cardinalMk_le_cRank
+
+theorem Basis.cardinalMk_le_cRk (hIX : M.Basis I X) : #I ≤ M.cRk X :=
+  hIX.basis'.cardinalMk_le_cRk
+
+theorem cRank_le_iff : M.cRank ≤ κ ↔ ∀ ⦃B⦄, M.Base B → #B ≤ κ :=
+  ⟨fun h _ hB ↦ (hB.cardinalMk_le_cRank.trans h), fun h ↦ ciSup_le fun ⟨_, hB⟩ ↦ h hB⟩
+
+theorem cRk_le_iff : M.cRk X ≤ κ ↔ ∀ ⦃I⦄, M.Basis' I X → #I ≤ κ := by
+  simp_rw [cRk, cRank_le_iff, base_restrict_iff']
+
+theorem Indep.cardinalMk_le_cRk_of_subset (hI : M.Indep I) (hIX : I ⊆ X) : #I ≤ M.cRk X :=
+  let ⟨_, hJ, hIJ⟩ := hI.subset_basis'_of_subset hIX
+  (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk
+
+theorem cRk_le_cardinalMk (M : Matroid α) (X : Set α) : M.cRk X ≤ #X :=
+  ciSup_le fun ⟨_, hI⟩ ↦ mk_le_mk_of_subset hI.subset_ground
+
+@[simp] theorem cRk_ground (M : Matroid α) : M.cRk M.E = M.cRank := by
+  rw [cRk, restrict_ground_eq_self]
+
+@[simp] theorem cRank_restrict (M : Matroid α) (X : Set α) : (M ↾ X).cRank = M.cRk X := rfl
+
+theorem cRk_mono (M : Matroid α) : Monotone M.cRk := by
+  simp only [Monotone, le_eq_subset, cRk_le_iff]
+  intro X Y hXY I hIX
+  obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_basis'_of_subset (hIX.subset.trans hXY)
+  exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk
+
+theorem cRk_le_of_subset (M : Matroid α) (hXY : X ⊆ Y) : M.cRk X ≤ M.cRk Y :=
+  M.cRk_mono hXY
+
+@[simp] theorem cRk_inter_ground (M : Matroid α) (X : Set α) : M.cRk (X ∩ M.E) = M.cRk X :=
+  (M.cRk_le_of_subset inter_subset_left).antisymm <| cRk_le_iff.2
+    fun _ h ↦ h.basis_inter_ground.cardinalMk_le_cRk
+
+theorem cRk_restrict_subset (M : Matroid α) (hYX : Y ⊆ X) : (M ↾ X).cRk Y = M.cRk Y := by
+  have aux : ∀ ⦃I⦄, M.Basis' I Y ↔ (M ↾ X).Basis' I Y := by
+    simp_rw [basis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
+    exact fun I h ↦ h.subset.trans hYX
+  simp_rw [le_antisymm_iff, cRk_le_iff]
+  exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩
+
+theorem cRk_restrict (M : Matroid α) (X Y : Set α) : (M ↾ X).cRk Y = M.cRk (X ∩ Y) := by
+  rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
+    inter_comm]
 
-/-- A class stating that cardinality-valued rank is well-defined for a matroid `M` and its minors.
-This holds for `Finitary` matroids.  -/
+theorem Indep.cRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cRk I :=
+  (M.cRk_le_cardinalMk I).antisymm' (hI.basis_self.cardinalMk_le_cRk)
+
+@[simp] theorem cRk_map_image_lift (M : Matroid α) (hf : InjOn f M.E) (X : Set α)
+    (hX : X ⊆ M.E := by aesop_mat) : lift.{u,v} ((M.map f hf).cRk (f '' X)) = lift (M.cRk X) := by
+  nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]
+  nth_rw 2 [lift_iSup (bddAbove_range _)]
+  simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, base_restrict_iff',
+    basis'_iff_basis hX, basis'_iff_basis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
+  refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
+  · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_basis_iff'.1 hI
+    rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]
+    obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
+    exact hIX.cardinalMk_le_cRk
+  rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]
+  exact (hI.map hf).cardinalMk_le_cRk
+
+@[simp] theorem cRk_map_image {β : Type u} {f : α → β} (M : Matroid α) (hf : InjOn f M.E)
+    (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : (M.map f hf).cRk (f '' X) = M.cRk X :=
+  lift_inj.1 <| M.cRk_map_image_lift ..
+
+theorem cRk_map_eq {β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (hf : InjOn f M.E) :
+    (M.map f hf).cRk X = M.cRk (f ⁻¹' X) := by
+  rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
+    cRk_inter_ground]
+
+@[simp] theorem cRk_comap_lift (M : Matroid β) (f : α → β) (X : Set α) :
+    lift.{v,u} ((M.comap f).cRk X) = lift (M.cRk (f '' X)) := by
+  nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]
+  nth_rw 2 [lift_iSup (bddAbove_range _)]
+  simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, base_restrict_iff',
+    comap_basis'_iff, and_imp]
+  refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
+  · rw [← mk_image_eq_of_injOn_lift _ _ hfI, lift_le]
+    exact hI.cardinalMk_le_cRk
+  obtain ⟨I₀, hI₀X, rfl, hfI₀⟩ := show ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀ by
+    obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
+    refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
+    rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]
+  rw [mk_image_eq_of_injOn_lift _ _ hfI₀, lift_le]
+  exact Basis'.cardinalMk_le_cRk <| comap_basis'_iff.2 ⟨hIX, hfI₀, hI₀X⟩
+
+@[simp] theorem cRk_comap {β : Type u} (M : Matroid β) (f : α → β) (X : Set α) :
+    (M.comap f).cRk X = M.cRk (f '' X) :=
+  lift_inj.1 <| M.cRk_comap_lift ..
+
+end Rank
+
+section Invariant
+
+/-- A class stating that cardinality-valued rank is well-defined
+(i.e. all bases are equicardinal) for a matroid `M` and its minors.
+Notably, this holds for `Finitary` matroids; see `Matroid.invarCardinalRank_of_finitary`.  -/
 @[mk_iff]
-class CardinalRank (M : Matroid α) : Prop where
+class InvariantCardinalRank (M : Matroid α) : Prop where
   forall_card_basis_diff :
     ∀ ⦃I J X⦄, M.Basis I X → M.Basis J X → #(I \ J : Set α) = #(J \ I : Set α)
 
-variable [CardinalRank M]
+variable [InvariantCardinalRank M]
 
 theorem Basis.cardinalMk_diff_comm (hIX : M.Basis I X) (hJX : M.Basis J X) :
     #(I \ J : Set α) = #(J \ I : Set α) :=
-  CardinalRank.forall_card_basis_diff hIX hJX
+  InvariantCardinalRank.forall_card_basis_diff hIX hJX
 
 theorem Basis'.cardinalMk_diff_comm (hIX : M.Basis' I X) (hJX : M.Basis' J X) :
     #(I \ J : Set α) = #(J \ I : Set α) :=
@@ -100,12 +223,66 @@ theorem Indep.cardinalMk_le_basis (hI : M.Indep I) (hJ : M.Basis J X) (hIX : I 
     #I ≤ #J :=
   hI.cardinalMk_le_basis' hJ.basis' hIX
 
-end Basic
+theorem Base.cardinalMk_eq_cRank (hB : M.Base B) : #B = M.cRank := by
+  have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
+  simp [cRank, hrw]
+
+/-- Restrictions of matroids with cardinal rank functions have cardinal rank functions- -/
+instance invariantCardinalRank_restrict [InvariantCardinalRank M] :
+    InvariantCardinalRank (M ↾ X) := by
+  refine ⟨fun I J Y hI hJ ↦ ?_⟩
+  rw [basis_restrict_iff'] at hI hJ
+  exact hI.1.cardinalMk_diff_comm hJ.1
+
+theorem Basis'.cardinalMk_eq_cRk (hIX : M.Basis' I X) : #I = M.cRk X := by
+  rw [cRk, (base_restrict_iff'.2 hIX).cardinalMk_eq_cRank]
+
+theorem Basis.cardinalMk_eq_cRk (hIX : M.Basis I X) : #I = M.cRk X :=
+  hIX.basis'.cardinalMk_eq_cRk
+
+@[simp] theorem cRk_closure (M : Matroid α) [InvariantCardinalRank M] (X : Set α) :
+    M.cRk (M.closure X) = M.cRk X := by
+  obtain ⟨I, hI⟩ := M.exists_basis' X
+  rw [← hI.basis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]
+
+theorem cRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cRk X = M.cRk Y := by
+  rw [← cRk_closure, hXY, cRk_closure]
+
+@[simp] theorem cRk_union_closure_right_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
+    M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y) :=
+  M.cRk_closure_congr (M.closure_union_closure_right_eq _ _)
+
+@[simp] theorem cRk_union_closure_left_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
+    M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y) :=
+  M.cRk_closure_congr (M.closure_union_closure_left_eq _ _)
+
+@[simp] theorem cRk_insert_closure_eq (M : Matroid α) [InvariantCardinalRank M] (e : α)
+    (X : Set α) : M.cRk (insert e (M.closure X)) = M.cRk (insert e X) := by
+  rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]
+
+theorem cRk_union_closure_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
+    M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y) := by
+  simp
+
+/-- The `Cardinal` rank function is submodular. -/
+theorem cRk_inter_add_cRk_union_le (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
+    M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y := by
+  obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
+  obtain ⟨IX, hIX, hIX'⟩ :=
+    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)
+  obtain ⟨IY, hIY, hIY'⟩ :=
+    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
+  rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
+    cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
+    ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]
+  exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))
+
+end Invariant
 
 section Instances
 
 /-- `Finitary` matroids have a cardinality-valued rank function. -/
-instance cardinalRank_of_finitary [Finitary M] : CardinalRank M := by
+instance invariantCardinalRank_of_finitary [Finitary M] : InvariantCardinalRank M := by
   suffices aux : ∀ ⦃B B'⦄ ⦃N : Matroid α⦄, Finitary N → N.Base B → N.Base B' →
       #(B \ B' : Set α) ≤ #(B' \ B : Set α) from
     ⟨fun I J X hI hJ ↦ (aux (restrict_finitary X) hI.base_restrict hJ.base_restrict).antisymm
@@ -136,153 +313,35 @@ instance cardinalRank_of_finitary [Finitary M] : CardinalRank M := by
   refine dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)
   exact subset_iUnion_of_subset ⟨a, this⟩ subset_rfl
 
-/-- Restrictions of matroids with cardinal rank functions have cardinal rank functions- -/
-instance cardinalRank_restrict [CardinalRank M] : CardinalRank (M ↾ X) := by
-  refine ⟨fun I J Y hI hJ ↦ ?_⟩
-  rw [basis_restrict_iff'] at hI hJ
-  exact hI.1.cardinalMk_diff_comm hJ.1
-
-instance cardinalRank_map {α β : Type u} {f : α → β} (M : Matroid α) [CardinalRank M]
-    (hf : InjOn f M.E) : CardinalRank (M.map f hf) := by
+instance invariantCardinalRank_map (M : Matroid α) [InvariantCardinalRank M] (hf : InjOn f M.E) :
+    InvariantCardinalRank (M.map f hf) := by
   refine ⟨fun I J X hI hJ ↦ ?_⟩
   obtain ⟨I, X, hIX, rfl, rfl⟩ := map_basis_iff'.1 hI
   obtain ⟨J, X', hJX, rfl, h'⟩ := map_basis_iff'.1 hJ
   obtain rfl : X = X' := by
     rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
   have hcard := hIX.cardinalMk_diff_comm hJX
-  rwa [← mk_image_eq_of_injOn _ _ (hf.mono (diff_subset.trans hIX.indep.subset_ground)),
-    ← mk_image_eq_of_injOn _ _ (hf.mono (diff_subset.trans hJX.indep.subset_ground)),
-    (hf.mono hIX.indep.subset_ground).image_diff,
+  rwa [← lift_inj.{u,v},
+    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.diff _).subset_ground)),
+    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.diff _).subset_ground)),
+    lift_inj, (hf.mono hIX.indep.subset_ground).image_diff,
     (hf.mono hJX.indep.subset_ground).image_diff, inter_comm,
     hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
     diff_inter_self_eq_diff, diff_self_inter] at hcard
 
-end Instances
-
-section Rank
-
-/-- The rank (size of a largest base) of a matroid `M` as a `Cardinal`. -/
-noncomputable def cardRank (M : Matroid α) := ⨆ (B : {B // M.Base B}), #B
-
-/-- The rank (size of a largest basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
-noncomputable def cardRk (M : Matroid α) (X : Set α) := (M ↾ X).cardRank
-
-theorem Base.cardinalMk_le_cardRank (hB : M.Base B) : #B ≤ M.cardRank :=
-  le_ciSup (f := fun (B : {B // M.Base B}) ↦ #(B.1)) (bddAbove_range _) ⟨B, hB⟩
-
-theorem Basis'.cardinalMk_le_cardRk (hIX : M.Basis' I X) : #I ≤ M.cardRk X :=
-  (base_restrict_iff'.2 hIX).cardinalMk_le_cardRank
-
-theorem Basis.cardinalMk_le_cardRk (hIX : M.Basis I X) : #I ≤ M.cardRk X :=
-  hIX.basis'.cardinalMk_le_cardRk
-
-theorem cardRank_le_iff {κ : Cardinal} : M.cardRank ≤ κ ↔ ∀ ⦃B⦄, M.Base B → #B ≤ κ :=
-  ⟨fun h _ hB ↦ (hB.cardinalMk_le_cardRank.trans h), fun h ↦ ciSup_le fun ⟨_, hB⟩ ↦ h hB⟩
-
-theorem cardRk_le_iff {κ : Cardinal} : M.cardRk X ≤ κ ↔ ∀ ⦃I⦄, M.Basis' I X → #I ≤ κ := by
-  simp_rw [cardRk, cardRank_le_iff, base_restrict_iff']
-
-theorem Indep.cardinalMk_le_cardRk_of_subset (hI : M.Indep I) (hIX : I ⊆ X) : #I ≤ M.cardRk X :=
-  let ⟨_, hJ, hIJ⟩ := hI.subset_basis'_of_subset hIX
-  (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cardRk
-
-theorem cardRk_le_cardinalMk (M : Matroid α) (X : Set α) : M.cardRk X ≤ #X :=
-  ciSup_le fun ⟨_, hI⟩ ↦ mk_le_mk_of_subset hI.subset_ground
-
-@[simp] theorem cardRk_ground (M : Matroid α) : M.cardRk M.E = M.cardRank := by
-  rw [cardRk, restrict_ground_eq_self]
-
-@[simp] theorem cardRank_restrict (M : Matroid α) (X : Set α) : (M ↾ X).cardRank = M.cardRk X := rfl
-
-theorem cardRk_mono (M : Matroid α) : Monotone M.cardRk := by
-  simp only [Monotone, le_eq_subset, cardRk_le_iff]
-  intro X Y hXY I hIX
-  obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_basis'_of_subset (hIX.subset.trans hXY)
-  exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cardRk
-
-theorem cardRk_le_of_subset (M : Matroid α) (hXY : X ⊆ Y) : M.cardRk X ≤ M.cardRk Y :=
-  M.cardRk_mono hXY
-
-@[simp] theorem cardRk_inter_ground (M : Matroid α) (X : Set α) :
-    M.cardRk (X ∩ M.E) = M.cardRk X :=
-  (M.cardRk_le_of_subset inter_subset_left).antisymm <|
-    cardRk_le_iff.2 fun _ h ↦ h.basis_inter_ground.cardinalMk_le_cardRk
-
-theorem cardRk_restrict_subset (M : Matroid α) (hYX : Y ⊆ X) : (M ↾ X).cardRk Y = M.cardRk Y := by
-  have aux : ∀ ⦃I⦄, M.Basis' I Y ↔ (M ↾ X).Basis' I Y := by
-    simp_rw [basis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
-    exact fun I h ↦ h.subset.trans hYX
-  simp_rw [le_antisymm_iff, cardRk_le_iff]
-  exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cardRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cardRk⟩
-
-theorem cardRk_restrict (M : Matroid α) (X Y : Set α) : (M ↾ X).cardRk Y = M.cardRk (X ∩ Y) := by
-  rw [← cardRk_inter_ground, restrict_ground_eq, cardRk_restrict_subset _ inter_subset_right,
-    inter_comm]
-
-theorem Indep.cardRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cardRk I :=
-  (M.cardRk_le_cardinalMk I).antisymm' (hI.basis_self.cardinalMk_le_cardRk)
-
-@[simp] theorem cardRk_map_eq {α β : Type u} {f : α → β} {X : Set α} (M : Matroid α)
-    (hf : InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) :
-    (M.map f hf).cardRk (f '' X) = M.cardRk X := by
-  simp_rw [le_antisymm_iff, cardRk_le_iff, basis'_iff_basis hX,
-    basis'_iff_basis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
-  refine ⟨fun I hI ↦ ?_, fun I hI ↦ le_of_eq_of_le ?_ (hI.map hf).cardinalMk_le_cardRk ⟩
-  · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_basis_iff'.1 hI
-    obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
-    rw [mk_image_eq_of_injOn _ _ (hf.mono hIX.indep.subset_ground)]
-    exact hIX.cardinalMk_le_cardRk
-  rw [mk_image_eq_of_injOn _ _ (hf.mono hI.indep.subset_ground)]
-
-variable [CardinalRank M]
-
-theorem Base.cardinalMk_eq_cardRank (hB : M.Base B) : #B = M.cardRank := by
-  have hrw : ∀ B' : {B : Set α // M.Base B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
-  simp [cardRank, hrw]
-
-theorem Basis'.cardinalMk_eq_cardRk (hIX : M.Basis' I X) : #I = M.cardRk X := by
-  rw [cardRk, (base_restrict_iff'.2 hIX).cardinalMk_eq_cardRank]
-
-theorem Basis.cardinalMk_eq_cardRk (hIX : M.Basis I X) : #I = M.cardRk X :=
-  hIX.basis'.cardinalMk_eq_cardRk
-
-@[simp] theorem cardRk_closure (M : Matroid α) [CardinalRank M] (X : Set α) :
-    M.cardRk (M.closure X) = M.cardRk X := by
-  obtain ⟨I, hI⟩ := M.exists_basis' X
-  rw [← hI.basis_closure_right.cardinalMk_eq_cardRk, ← hI.cardinalMk_eq_cardRk]
-
-theorem cardRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cardRk X = M.cardRk Y := by
-  rw [← cardRk_closure, hXY, cardRk_closure]
-
-@[simp] theorem cardRk_union_closure_right_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
-    M.cardRk (X ∪ M.closure Y) = M.cardRk (X ∪ Y) :=
-  M.cardRk_closure_congr (M.closure_union_closure_right_eq _ _)
-
-@[simp] theorem cardRk_union_closure_left_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
-    M.cardRk (M.closure X ∪ Y) = M.cardRk (X ∪ Y) :=
-  M.cardRk_closure_congr (M.closure_union_closure_left_eq _ _)
-
-@[simp] theorem cardRk_insert_closure_eq (M : Matroid α) [CardinalRank M] (e : α) (X : Set α) :
-    M.cardRk (insert e (M.closure X)) = M.cardRk (insert e X) := by
-  rw [← union_singleton, cardRk_union_closure_left_eq, union_singleton]
-
-theorem cardRk_union_closure_eq (M : Matroid α) [CardinalRank M] (X Y : Set α) :
-    M.cardRk (M.closure X ∪ M.closure Y) = M.cardRk (X ∪ Y) := by
-  simp
-
-/-- The `Cardinal` rank function is submodular. -/
-theorem cardRk_inter_add_cardRk_union_le (M : Matroid α) [CardinalRank M] (X Y : Set α) :
-    M.cardRk (X ∩ Y) + M.cardRk (X ∪ Y) ≤ M.cardRk X + M.cardRk Y := by
-  obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
-  obtain ⟨IX, hIX, hIX'⟩ :=
-    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)
-  obtain ⟨IY, hIY, hIY'⟩ :=
-    hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
-  rw [← cardRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
-    cardRk_union_closure_eq, ← hIi.cardinalMk_eq_cardRk, ← hIX.cardinalMk_eq_cardRk,
-    ← hIY.cardinalMk_eq_cardRk, ← mk_union_add_mk_inter, add_comm]
-  exact add_le_add (M.cardRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))
+instance invariantCardinalRank_comap (M : Matroid β) [InvariantCardinalRank M] (f : α → β) :
+    InvariantCardinalRank (M.comap f) := by
+  refine ⟨fun I J X hI hJ ↦ ?_⟩
+  obtain ⟨hI, hfI, hIX⟩ := comap_basis_iff.1 hI
+  obtain ⟨hJ, hfJ, hJX⟩ := comap_basis_iff.1 hJ
+  rw [← lift_inj.{u,v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono diff_subset),
+    ← mk_image_eq_of_injOn_lift _ _ (hfJ.mono diff_subset), lift_inj, hfI.image_diff,
+    hfJ.image_diff, ← diff_union_diff_cancel inter_subset_left (image_inter_subset f I J),
+    inter_comm, diff_inter_self_eq_diff, mk_union_of_disjoint, hI.cardinalMk_diff_comm hJ,
+    ← diff_union_diff_cancel inter_subset_left (image_inter_subset f J I), inter_comm,
+    diff_inter_self_eq_diff, mk_union_of_disjoint, inter_comm J I] <;>
+  exact disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)
 
-end Rank
+end Instances
 
 end Matroid

From eb82f6136ebc60f298f986d19beddbf08b8bef02 Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Sun, 26 Jan 2025 19:40:50 -0500
Subject: [PATCH 12/13] tidying

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index d337d9a50d93be..056698bb79d016 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -46,8 +46,8 @@ they are well-defined for all matroids.
 However, for matroids that do not satisfy `InvariantCardinalRank`, they are badly behaved.
 For instance, in general `cRk` is not submodular,
 and its value may differ on a set `X` and the closure of `X`.
-We state and prove theorems without the instance whenever possible,
-which sometime makes their proofs longer than they would be without the instance.
+We state and prove theorems without `InvariantCardinalRank` whenever possible,
+which sometime makes their proofs longer than they would be with the instance.
 
 # TODO
 
@@ -248,25 +248,22 @@ theorem Basis.cardinalMk_eq_cRk (hIX : M.Basis I X) : #I = M.cRk X :=
 theorem cRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cRk X = M.cRk Y := by
   rw [← cRk_closure, hXY, cRk_closure]
 
-@[simp] theorem cRk_union_closure_right_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
-    M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y) :=
+variable (M : Matroid α) [InvariantCardinalRank M] (e : α) (X Y : Set α)
+
+@[simp] theorem cRk_union_closure_right_eq : M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y) :=
   M.cRk_closure_congr (M.closure_union_closure_right_eq _ _)
 
-@[simp] theorem cRk_union_closure_left_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
-    M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y) :=
+@[simp] theorem cRk_union_closure_left_eq : M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y) :=
   M.cRk_closure_congr (M.closure_union_closure_left_eq _ _)
 
-@[simp] theorem cRk_insert_closure_eq (M : Matroid α) [InvariantCardinalRank M] (e : α)
-    (X : Set α) : M.cRk (insert e (M.closure X)) = M.cRk (insert e X) := by
+@[simp] theorem cRk_insert_closure_eq : M.cRk (insert e (M.closure X)) = M.cRk (insert e X) := by
   rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]
 
-theorem cRk_union_closure_eq (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
-    M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y) := by
+theorem cRk_union_closure_eq : M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y) := by
   simp
 
 /-- The `Cardinal` rank function is submodular. -/
-theorem cRk_inter_add_cRk_union_le (M : Matroid α) [InvariantCardinalRank M] (X Y : Set α) :
-    M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y := by
+theorem cRk_inter_add_cRk_union_le : M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y := by
   obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
   obtain ⟨IX, hIX, hIX'⟩ :=
     hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)

From 74c464f94aa9c9050d769d8cf9bb27b3e21d01ee Mon Sep 17 00:00:00 2001
From: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Date: Mon, 27 Jan 2025 16:35:01 -0500
Subject: [PATCH 13/13] comments

---
 Mathlib/Data/Matroid/Rank/Cardinal.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Matroid/Rank/Cardinal.lean b/Mathlib/Data/Matroid/Rank/Cardinal.lean
index 056698bb79d016..0d10845213b063 100644
--- a/Mathlib/Data/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Data/Matroid/Rank/Cardinal.lean
@@ -68,10 +68,11 @@ section Rank
 
 variable {κ : Cardinal}
 
-/-- The rank (size of a largest base) of a matroid `M` as a `Cardinal`. -/
+/-- The rank (supremum of the cardinalities of bases) of a matroid `M` as a `Cardinal`. -/
 noncomputable def cRank (M : Matroid α) := ⨆ (B : {B // M.Base B}), #B
 
-/-- The rank (size of a largest basis) of a set `X` in a matroid `M`, as a `Cardinal`. -/
+/-- The rank (supremum of the cardinalities of bases) of a set `X` in a matroid `M`,
+as a `Cardinal`. -/
 noncomputable def cRk (M : Matroid α) (X : Set α) := (M ↾ X).cRank
 
 theorem Base.cardinalMk_le_cRank (hB : M.Base B) : #B ≤ M.cRank :=