-- 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 : 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

Tactic:
simp_rw [smul_zero, Finset.smul_sum, ← mul_smul, Submonoid.smul_def, ← mul_smul, mul_comm] at hc

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
⊢ (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
⊢ ∀ x ∈ t, ↑(u x) • (sec (g x)).1 • f ↑x = ↑(∏ j ∈ t, (sec (g j)).2) • g x • f ↑x

Tactic:
intro j hj

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
j : ↑s
hj : j ∈ t
⊢ ↑(u j) • (sec (g j)).1 • f ↑j = ↑(∏ j ∈ t, (sec (g j)).2) • g j • f ↑j

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
j : ↑s
hj : j ∈ t
⊢ ↑(u j) • (sec (g j)).1 • f ↑j = ↑(∏ j ∈ t, (sec (g j)).2) • g j • f ↑j

Tactic:
simp only [u, ← @IsScalarTower.algebraMap_smul R S N, Submonoid.coe_finset_prod, map_prod]

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
j : ↑s
hj : j ∈ t
⊢ (∏ x ∈ t.erase j, (algebraMap R S) ↑(sec (g x)).2) • (algebraMap R S) (sec (g j)).1 • f ↑j =
    (∏ x ∈ t, (algebraMap R S) ↑(sec (g x)).2) • g j • f ↑j

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 : ∀ (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
⊢ g i = 0

Tactic:
apply (IsLocalization.map_units S (sec (g i)).2).mul_left_injective

Result:
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
⊢ (fun x => x * (algebraMap R S) ↑(sec (g i)).2) (g i) = (fun x => x * (algebraMap R S) ↑(sec (g i)).2) 0