-- Mathlib/RingTheory/LocalProperties/Projective.lean
theorem Module.lift_rank_of_isLocalizedModule_of_free
    (Rₛ : Type uR') {Mₛ : Type uM'} [AddCommGroup Mₛ] [Module R Mₛ]
    [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R)
    (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Free R M]
    [Nontrivial Rₛ] :
    Cardinal.lift.{uM} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM'} (Module.rank R M)

Proof state:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm

Result:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Proof state:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
have := (algebraMap R Rₛ).domain_nontrivial

Result:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Proof state:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)

Tactic:
convert this

Result:
case h.e'_2.h.e
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}

Proof state:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
simp only [rank_tensorProduct, rank_self,
  Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢

Result:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)

Proof state:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)

Tactic:
apply Cardinal.lift_injective.{max uM' uR'}

Result:
case a
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Proof state:
case h.e'_2.h.e
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}

Tactic:
exact Cardinal.lift_umax

Result:
no goals