Theorem: FiniteDimensional.finrank_add_finrank_quotient_of_free (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
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
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)

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
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)

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]
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)

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
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)

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
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)

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
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
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]
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

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
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

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
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

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
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

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
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
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
State after:
no goals