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

Tactic:
have := (algebraMap R S).codomain_trivial

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
this : Subsingleton S
⊢ 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 : ∀ (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
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → S), ∑ i ∈ s_1, g i • f ↑i = 0 → ∀ i ∈ s_1, g i = 0

Tactic:
intro t g hg i hit

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

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

Tactic:
let u := fun (i : s) ↦ (t.erase i).prod (fun j ↦ (sec (g j)).2)

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
u : ↑s → ↥p := fun i => ∏ j ∈ t.erase i, (sec (g j)).2
⊢ (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 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
this : Subsingleton S
⊢ Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)

Tactic:
simp only [rank_subsingleton, lift_one]

Result:
no goals