Theorem: FiniteDimensional.finrank_add_finrank_quotient (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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
Tactic:
have : IsNoetherian R M := isNoetherian_of_isNoetherianRing_of_finite R M
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this : IsNoetherian R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = 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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this : IsNoetherian R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
Tactic:
have := FiniteDimensional.finrank_add_finrank_quotient_of_free (N.map (Submodule.torsion R M).mkQ)
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R (M ⧸ Submodule.torsion R M)
⊢ finrank R ↥N + finrank R (M ⧸ N) = 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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R (M ⧸ Submodule.torsion R M)
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
Tactic:
rw [FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl,
  FiniteDimensional.finrank_map_of_le_torsion] 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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion 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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M
Tactic:
convert this using 2
State after:
case h.e'_2.h.e'_6
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R (M ⧸ N) = finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N)

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M

State before:
case h.e'_2.h.e'_6
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R (M ⧸ N) = finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N)

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M
Tactic:
symm
State after:
case h.e'_2.h.e'_6
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R (M ⧸ N)

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M

State before:
case h.e'_2.h.e'_6
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R (M ⧸ N)

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M
Tactic:
fapply FiniteDimensional.finrank_of_surjective_of_le_torsion
State after:
case h.e'_2.h.e'_6.l
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ M ⧸ N →ₗ[R] (M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N

case h.e'_2.h.e'_6.hl
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Function.Surjective ⇑?h.e'_2.h.e'_6.l

case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ LinearMap.ker ?h.e'_2.h.e'_6.l ≤ Submodule.torsion R (M ⧸ N)

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M

State before:
case h.e'_2.h.e'_6.l
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ M ⧸ N →ₗ[R] (M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N
Tactic:
refine Submodule.liftQ N ((Submodule.mkQ _).comp (Submodule.mkQ _)) ?_
State after:
case h.e'_2.h.e'_6.l
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ N ≤ LinearMap.ker ((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ)

State before:
case h.e'_2.h.e'_6.l
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ N ≤ LinearMap.ker ((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ)
Tactic:
rw [LinearMap.ker_comp, ← Submodule.map_le_iff_le_comap, Submodule.ker_mkQ]
State after:
no goals

State before:
case h.e'_2.h.e'_6.hl
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Function.Surjective ⇑(N.liftQ ((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ) ⋯)
Tactic:
rw [← LinearMap.range_eq_top, Submodule.range_liftQ, LinearMap.range_eq_top]
State after:
case h.e'_2.h.e'_6.hl
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Function.Surjective ⇑((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ)

State before:
case h.e'_2.h.e'_6.hl
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Function.Surjective ⇑((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ)
Tactic:
exact (Submodule.mkQ_surjective _).comp (Submodule.mkQ_surjective _)
State after:
no goals

State before:
case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ LinearMap.ker (N.liftQ ((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ) ⋯) ≤
    Submodule.torsion R (M ⧸ N)
Tactic:
rw [Submodule.ker_liftQ, Submodule.map_le_iff_le_comap, LinearMap.ker_comp,
  Submodule.ker_mkQ, Submodule.comap_map_eq, Submodule.ker_mkQ]
State after:
case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ N ⊔ Submodule.torsion R M ≤ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))

State before:
case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ N ⊔ Submodule.torsion R M ≤ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))
Tactic:
apply sup_le (N.le_comap_mkQ _)
State after:
case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Submodule.torsion R M ≤ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))

State before:
case h.e'_2.h.e'_6.hl'
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ Submodule.torsion R M ≤ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))
Tactic:
rintro x ⟨r, hrx⟩
State after:
case h.e'_2.h.e'_6.hl'.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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
x : M
r : ↥(nonZeroDivisors R)
hrx : r • x = 0
⊢ x ∈ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))

State before:
case h.e'_2.h.e'_6.hl'.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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
x : M
r : ↥(nonZeroDivisors R)
hrx : r • x = 0
⊢ x ∈ Submodule.comap N.mkQ (Submodule.torsion R (M ⧸ N))
Tactic:
exact ⟨r, by rw [← LinearMap.map_smul_of_tower, hrx, map_zero]⟩
State after:
no goals

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
x : M
r : ↥(nonZeroDivisors R)
hrx : r • x = 0
⊢ r • N.mkQ x = 0
Tactic:
rw [← LinearMap.map_smul_of_tower, hrx, map_zero]
State after:
no goals

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M
Tactic:
rw [Submodule.ker_mkQ]
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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ Submodule.torsion R M ≤ Submodule.torsion R M

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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ Submodule.torsion R M ≤ Submodule.torsion R M
Tactic:
exact inf_le_right
State after:
no goals