-- 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:
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 : ∑ x ∈ t, ((sec (g x)).1 * ↑(c * u x)) • ↑x = 0
⊢ (sec (g i)).1 = 0

Tactic:
apply hp (c * u i).prop

Result:
case inr.a.h.a.intro.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
c : ↥p
hc : ∑ x ∈ t, ((sec (g x)).1 * ↑(c * u x)) • ↑x = 0
⊢ (sec (g i)).1 * ↑(c * u i) = 0

Proof state:
case inr.a.h.a.intro.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
c : ↥p
hc : ∑ x ∈ t, ((sec (g x)).1 * ↑(c * u x)) • ↑x = 0
⊢ (sec (g i)).1 * ↑(c * u i) = 0

Tactic:
exact hs t _ hc _ hit

Result:
no goals

Proof state:
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 : ∑ x ∈ t, ((sec (g x)).1 * ↑(c * u x)) • ↑x = 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:
simp only [hsec, zero_mul, map_eq_zero_iff (algebraMap R S) (IsLocalization.injective S hp)]

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 : ∑ x ∈ t, ((sec (g x)).1 * ↑(c * u x)) • ↑x = 0
⊢ (sec (g i)).1 = 0

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
⊢ Cardinal.lift.{v', v} #↑↑⟨s, hs⟩ ≤ Cardinal.lift.{v, v'} (Module.rank S N)

Tactic:
choose sec hsec using IsLocalization.surj p (S := S)

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
⊢ Cardinal.lift.{v', v} #↑↑⟨s, hs⟩ ≤ Cardinal.lift.{v, v'} (Module.rank S N)

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 N
hs : LinearIndepOn S id s
⊢ Cardinal.lift.{v, v'} #↑↑⟨s, hs⟩ ≤ Cardinal.lift.{v', v} (Module.rank R M)

Tactic:
exact (IsLocalizedModule.linearIndependent_lift p f hp hs).choose_spec.cardinal_lift_le_rank

Result:
no goals