refactor, to be discussed: change FiniteDimensional.two_le_rank_of_ra…

…nk_lt_rank to one_lt_rank....

This is what my application for ample sets expects; in this setting,
both are proven the same way.
To be discussed if this is a good change or not!

SphereEversion/Global/Immersion.lean

@@ -77,13 +77,9 @@ theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel
   rintro ⟨⟨m, m'⟩, φ : TangentSpace I m →L[ℝ] TangentSpace I' m'⟩ (p : DualPair (TangentSpace I m))
     (hφ : Injective φ)
   haveI : FiniteDimensional ℝ (TangentSpace I m) := (by infer_instance : FiniteDimensional ℝ E)
-  have hcodim := two_le_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap
-  -- FIXME: prove an analogue of `two_le_rank_of_rank_lt_rank` with `1 < ...` instead
-  have hcodim' : 1 < Module.rank ℝ (E' ⧸ Submodule.map (↑φ) (LinearMap.ker ↑p.π)) := by
-    rw [← Cardinal.two_le_iff_one_lt]
-    exact hcodim
+  have hcodim := one_lt_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap
   rw [immersionRel_slice_eq I I' hφ]
-  exact AmpleSet.of_one_lt_codim hcodim'
+  exact AmpleSet.of_one_lt_codim hcodim
 
 /-- This is lemma `lem:open_ample_immersion` from the blueprint. -/
 theorem immersionRel_open_ample (h : finrank ℝ E < finrank ℝ E') :

SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean

@@ -5,9 +5,9 @@ open FiniteDimensional Submodule
 variable {𝕜 : Type*} [Field 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E] {E' : Type*}
   [AddCommGroup E'] [Module 𝕜 E']
 
-theorem two_le_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜}
+theorem one_lt_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜}
     (hπ : LinearMap.ker π ≠ ⊤) (h : finrank 𝕜 E < finrank 𝕜 E') (φ : E →ₗ[𝕜] E') :
-    2 ≤ Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π)) := by
+    1 < Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π)) := by
   suffices 2 ≤ finrank 𝕜 (E' ⧸ π.ker.map φ) by
     rw [← finrank_eq_rank]
     exact_mod_cast this