Theorem: FiniteDimensional.finrank_of_surjective_of_le_torsion (FltRegular/NumberTheory/Finrank.lean)

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
l : M →ₗ[R] M'
hl : Function.Surjective ⇑l
hl' : LinearMap.ker l ≤ Submodule.torsion R M
⊢ finrank R M' = finrank R M
Tactic:
have := FiniteDimensional.finrank_map_of_le_torsion ⊤ l (inf_le_right.trans hl')
State after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
l : M →ₗ[R] M'
hl : Function.Surjective ⇑l
hl' : LinearMap.ker l ≤ Submodule.torsion R M
this : finrank R ↥(Submodule.map l ⊤) = finrank R ↥⊤
⊢ finrank R M' = finrank R M

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
l : M →ₗ[R] M'
hl : Function.Surjective ⇑l
hl' : LinearMap.ker l ≤ Submodule.torsion R M
this : finrank R ↥(Submodule.map l ⊤) = finrank R ↥⊤
⊢ finrank R M' = finrank R M
Tactic:
rw [← LinearMap.range_eq_map l, LinearMap.range_eq_top.mpr hl] at this
State after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
l : M →ₗ[R] M'
hl : Function.Surjective ⇑l
hl' : LinearMap.ker l ≤ Submodule.torsion R M
this : finrank R ↥⊤ = finrank R ↥⊤
⊢ finrank R M' = finrank R M

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Submodule R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
l : M →ₗ[R] M'
hl : Function.Surjective ⇑l
hl' : LinearMap.ker l ≤ Submodule.torsion R M
this : finrank R ↥⊤ = finrank R ↥⊤
⊢ finrank R M' = finrank R M
Tactic:
simpa only [finrank_top] using this
State after:
no goals