internlm/Lean-Github huggingface dataset:
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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)
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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 _)) ?_
Proof 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)
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]
Proof 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)
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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 _)
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]
Proof 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))
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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 _)
Proof 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))
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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⟩
Proof 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))
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]⟩
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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]
Proof 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
Theorem: FiniteDimensional.finrank_add_finrank_quotient
Proof 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
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_quotient
Proof 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 (M ⧸ N) = finrank R M - finrank R ↥N
Tactic:
rw [← FiniteDimensional.finrank_add_finrank_quotient N, add_tsub_cancel_left]
Proof state after:
no goals
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof 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
h : finrank R ↥N < finrank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic:
obtain ⟨s, hs, hs'⟩ :=
  FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent R (M ⧸ N)
Proof state after:
case intro.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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case intro.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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic:
obtain ⟨v, hv⟩ : s.Nonempty
Proof 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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ s.Nonempty

case intro.intro.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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M ⧸ N
hv : v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case intro.intro.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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M ⧸ N
hv : v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic:
obtain ⟨v, rfl⟩ := N.mkQ_surjective v
Proof state after:
case intro.intro.intro.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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N