Theorem: FiniteDimensional.finrank_map_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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ finrank R ↥(Submodule.map l N) = finrank R ↥N
Tactic:
conv_lhs => rw [← N.range_subtype, ← LinearMap.range_comp,
  ← (LinearMap.quotKerEquivRange (l.comp N.subtype)).finrank_eq]
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ finrank R (↥N ⧸ LinearMap.ker (l ∘ₗ N.subtype)) = finrank R ↥N

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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ finrank R (↥N ⧸ LinearMap.ker (l ∘ₗ N.subtype)) = finrank R ↥N
Tactic:
apply FiniteDimensional.finrank_quotient_of_le_torsion
State after:
case hN
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ LinearMap.ker (l ∘ₗ N.subtype) ≤ Submodule.torsion R ↥N

State before:
case hN
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ LinearMap.ker (l ∘ₗ N.subtype) ≤ Submodule.torsion R ↥N
Tactic:
rintro x hx
State after:
case hN
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
x : ↥N
hx : x ∈ LinearMap.ker (l ∘ₗ N.subtype)
⊢ x ∈ Submodule.torsion R ↥N

State before:
case hN
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
x : ↥N
hx : x ∈ LinearMap.ker (l ∘ₗ N.subtype)
⊢ x ∈ Submodule.torsion R ↥N
Tactic:
obtain ⟨a, ha⟩ := hN ⟨x.prop, hx⟩
State after:
case hN.intro
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
x : ↥N
hx : x ∈ LinearMap.ker (l ∘ₗ N.subtype)
a : ↥(nonZeroDivisors R)
ha : a • ↑x = 0
⊢ x ∈ Submodule.torsion R ↥N

State before:
case hN.intro
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'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
x : ↥N
hx : x ∈ LinearMap.ker (l ∘ₗ N.subtype)
a : ↥(nonZeroDivisors R)
ha : a • ↑x = 0
⊢ x ∈ Submodule.torsion R ↥N
Tactic:
exact ⟨a, Subtype.val_injective ha⟩
State after:
no goals