-- Mathlib/LinearAlgebra/Dimension/Localization.lean
lemma IsLocalizedModule.lift_rank_eq :
    Cardinal.lift.{v} (Module.rank S N) = Cardinal.lift.{v'} (Module.rank R M)

Proof state:
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
⊢ Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Subsingleton R
⊢ Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)

case inr
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)

Proof state:
case inr.a.h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : LinearIndepOn R id s
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
⊢ LinearIndependent S fun (i : ↑s) => f ↑i

Tactic:
rw [LinearIndepOn] at hs

Result:
case inr.a.h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : LinearIndependent R fun (x : ↑s) => id ↑x
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
⊢ LinearIndependent S fun (i : ↑s) => f ↑i

Proof state:
case inr.a.h.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this✝ : Nontrivial S
s : Set M
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
t : Finset ↑s
g : ↑s → S
hg : ∑ i ∈ t, g i • f ↑i = 0
i : ↑s
hit : i ∈ t
u : ↑s → ↥p := fun i => ∏ j ∈ t.erase i, (sec (g j)).2
this : f (∑ i ∈ t, u i • (sec (g i)).1 • ↑i) = f 0
⊢ (fun x => x * (algebraMap R S) ↑(sec (g i)).2) (g i) = (fun x => x * (algebraMap R S) ↑(sec (g i)).2) 0

Tactic:
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := p) this

Result:
case inr.a.h.a.intro
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this✝ : Nontrivial S
s : Set M
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
t : Finset ↑s
g : ↑s → S
hg : ∑ i ∈ t, g i • f ↑i = 0
i : ↑s
hit : i ∈ t
u : ↑s → ↥p := fun i => ∏ j ∈ t.erase i, (sec (g j)).2
this : f (∑ i ∈ t, u i • (sec (g i)).1 • ↑i) = f 0
c : ↥p
hc : c • ∑ i ∈ t, u i • (sec (g i)).1 • ↑i = c • 0
⊢ (fun x => x * (algebraMap R S) ↑(sec (g i)).2) (g i) = (fun x => x * (algebraMap R S) ↑(sec (g i)).2) 0

Proof state:
case h.e'_2
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
t : Finset ↑s
g : ↑s → S
hg : ∑ i ∈ t, g i • f ↑i = 0
i : ↑s
hit : i ∈ t
u : ↑s → ↥p := fun i => ∏ j ∈ t.erase i, (sec (g j)).2
⊢ f (∑ i ∈ t, u i • (sec (g i)).1 • ↑i) = (∏ j ∈ t, (sec (g j)).2) • ∑ i ∈ t, g i • f ↑i

Tactic:
simp only [map_sum, map_smul, Submonoid.smul_def, Finset.smul_sum]

Result:
case h.e'_2
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
t : Finset ↑s
g : ↑s → S
hg : ∑ i ∈ t, g i • f ↑i = 0
i : ↑s
hit : i ∈ t
u : ↑s → ↥p := fun i => ∏ j ∈ t.erase i, (sec (g j)).2
⊢ ∑ x ∈ t, ↑(u x) • (sec (g x)).1 • f ↑x = ∑ x ∈ t, ↑(∏ j ∈ t, (sec (g j)).2) • g x • f ↑x

Proof state:
case inr.a.h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : LinearIndepOn R id s
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
⊢ Cardinal.lift.{v', v} #↑↑⟨s, hs⟩ ≤ Cardinal.lift.{v, v'} (Module.rank S N)

Tactic:
refine LinearIndependent.cardinal_lift_le_rank (ι := s) (v := fun i ↦ f i) ?_

Result:
case inr.a.h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
this : Nontrivial S
s : Set M
hs : LinearIndepOn R id s
sec : S → R × ↥p
hsec : ∀ (z : S), z * (algebraMap R S) ↑(sec z).2 = (algebraMap R S) (sec z).1
⊢ LinearIndependent S fun (i : ↑s) => f ↑i