-- Mathlib/LinearAlgebra/Dimension/Free.lean
/-- The rank of a free module `M` over an infinite scalar ring `R` is the cardinality of `M`
whenever `#R < #M`. -/
lemma rank_eq_mk_of_infinite_lt [Infinite R] (h_lt : lift.{v} #R < lift.{u} #M) :
    Module.rank R M = #M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Module.rank R M = #M

Tactic:
have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
⊢ Module.rank R M = #M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{v, max u v} #(ChooseBasisIndex R M →₀ R)
⊢ Module.rank R M = #M

Tactic:
simp only [mk_finsupp_lift_of_infinite', lift_id', ← rank_eq_card_chooseBasisIndex, lift_max,
  lift_lift] at h

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{max u v, v} (Module.rank R M) ⊔ lift.{v, u} #R
⊢ Module.rank R M = #M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ lift.{u, v} ℵ₀ ≤ lift.{v, u} #R

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
⊢ Module.rank R M = #M

Tactic:
have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{v, max u v} #(ChooseBasisIndex R M →₀ R)
⊢ Module.rank R M = #M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{max u v, v} (Module.rank R M) ⊔ lift.{v, u} #R
⊢ ¬lift.{v, u} #R = lift.{max u v, v} #M

Tactic:
exact (lift_umax.{v, u}.symm ▸ h_lt).ne

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{max u v, v} (Module.rank R M) ⊔ lift.{v, u} #R
⊢ Module.rank R M = #M

Tactic:
refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{max u v, v} (Module.rank R M) ⊔ lift.{v, u} #R
⊢ ¬lift.{v, u} #R = lift.{max u v, v} #M