internlm/Lean-Github huggingface dataset:
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
x : M
h₁ : x ∈ Subtype.val '' ↑s
h₂ : x ∈ f '' ↑t
⊢ x ∈ ∅
Tactic:
obtain rfl : x = 0 :=
  (disjoint_iff.mp H).le ⟨Submodule.subset_span h₁, Submodule.subset_span h₂⟩
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₁ : 0 ∈ Subtype.val '' ↑s
h₂ : 0 ∈ f '' ↑t
⊢ 0 ∈ ∅
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₁ : 0 ∈ Subtype.val '' ↑s
h₂ : 0 ∈ f '' ↑t
⊢ 0 ∈ ∅
Tactic:
simp only [Set.mem_image, Finset.mem_coe, ZeroMemClass.coe_eq_zero, exists_eq_right] at h₁
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ 0 ∈ ∅
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ 0 ∈ ∅
Tactic:
exact hs'.ne_zero ⟨0, h₁⟩ (by simp only)
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
h₂ : 0 ∈ f '' ↑t
h₁ : 0 ∈ s
⊢ ↑⟨0, h₁⟩ = 0
Tactic:
simp only
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_map_of_le_torsion
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
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]
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
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
Theorem: FiniteDimensional.finrank_map_of_le_torsion
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
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
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
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
Theorem: FiniteDimensional.finrank_map_of_le_torsion
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
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
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
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
Theorem: FiniteDimensional.finrank_map_of_le_torsion
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
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⟩
Proof 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
Theorem: FiniteDimensional.finrank_map_of_le_torsion
Proof 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⟩
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_of_surjective_of_le_torsion
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
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')
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
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
Theorem: FiniteDimensional.finrank_of_surjective_of_le_torsion
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
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
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
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
Theorem: FiniteDimensional.finrank_of_surjective_of_le_torsion
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
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
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
Tactic:
apply (finrank_add_finrank_quotient_le N).antisymm
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
inst✝ : Module.Free R M
N : Submodule R M
⊢ finrank R M ≤ finrank R ↥N + finrank R (M ⧸ N)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
⊢ finrank R M ≤ finrank R ↥N + finrank R (M ⧸ N)
Tactic:
let B := Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ finrank R M ≤ finrank R ↥N + finrank R (M ⧸ N)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ finrank R M ≤ finrank R ↥N + finrank R (M ⧸ N)
Tactic:
rw [← tsub_le_iff_left]
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Tactic:
have : LinearIndependent R (N.mkQ ∘ B.2.bM ∘ Subtype.val : ((Set.range B.2.f)ᶜ : _) → _) := by
  rw [linearIndependent_iff]
  intros l hl
  ext i
  rw [← Finsupp.apply_total, N.mkQ_apply, Submodule.Quotient.mk_eq_zero, Finsupp.total_apply,
    Finsupp.sum_fintype _ _ (by simp)] at hl
  simpa only [Function.comp_apply, map_sum, map_smul, Basis.repr_self, Finsupp.smul_single,
    smul_eq_mul, mul_one, Finsupp.single_apply, Finsupp.finset_sum_apply,
    ← Subtype.ext_iff, Finset.sum_ite_eq', Finset.mem_univ, ite_true] using
    B.2.repr_eq_zero_of_nmem_range ⟨_, hl⟩ i.prop
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
this : LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
this : LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Tactic:
have := this.fintype_card_le_finrank
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
this✝ : LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
this : Fintype.card ↑(Set.range ⇑B.snd.f)ᶜ ≤ finrank R (M ⧸ N)
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
this✝ : LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
this : Fintype.card ↑(Set.range ⇑B.snd.f)ᶜ ≤ finrank R (M ⧸ N)
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
Tactic:
rwa [Fintype.card_compl_set, ← finrank_eq_card_chooseBasisIndex,
  Fintype.card_range, ← finrank_eq_card_basis B.2.bN] at this
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
Tactic:
rw [linearIndependent_iff]
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ ∀ (l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R),
    (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0 → l = 0
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ ∀ (l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R),
    (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0 → l = 0
Tactic:
intros l hl
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0
⊢ l = 0
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0
⊢ l = 0
Tactic:
ext i
Proof state after:
case h
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ l i = 0 i
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
Proof state before:
case h
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ l i = 0 i
Tactic:
rw [← Finsupp.apply_total, N.mkQ_apply, Submodule.Quotient.mk_eq_zero, Finsupp.total_apply,
  Finsupp.sum_fintype _ _ (by simp)] at hl
Proof state after:
case h
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : ∑ i : ↑(Set.range ⇑B.snd.f)ᶜ, l i • (⇑B.snd.bM ∘ Subtype.val) i ∈ N
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ l i = 0 i
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
Proof state before:
case h
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : ∑ i : ↑(Set.range ⇑B.snd.f)ᶜ, l i • (⇑B.snd.bM ∘ Subtype.val) i ∈ N
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ l i = 0 i
Tactic:
simpa only [Function.comp_apply, map_sum, map_smul, Basis.repr_self, Finsupp.smul_single,
  smul_eq_mul, mul_one, Finsupp.single_apply, Finsupp.finset_sum_apply,
  ← Subtype.ext_iff, Finset.sum_ite_eq', Finset.mem_univ, ite_true] using
  B.2.repr_eq_zero_of_nmem_range ⟨_, hl⟩ i.prop
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : (l.sum fun i a => a • (⇑B.snd.bM ∘ Subtype.val) i) ∈ N
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ ∀ (i : ↑(Set.range ⇑B.snd.f)ᶜ), 0 • (⇑B.snd.bM ∘ Subtype.val) i = 0
Tactic:
simp
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
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
Tactic:
have : IsNoetherian R M := isNoetherian_of_isNoetherianRing_of_finite R M
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
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M