-- Mathlib/RingTheory/Ideal/Quotient/Index.lean
/-- Let `N` be a finite index f.g. `R`-submodule, and `I` be a finite index ideal.
Then `I • N` also has finite index. -/
lemma Submodule.finite_quotient_smul [Finite (R ⧸ I)] [Finite (M ⧸ N)] (hN : N.FG) :
    Finite (M ⧸ I • N)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : (I • N).toAddSubgroup.FiniteIndex
⊢ Finite (M ⧸ I • N)

Tactic:
exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Tactic:
rw [Nat.card_congr e.toEquiv]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Proof state:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.index ≠ 0

Tactic:
rw [← AddSubgroup.relindex_mul_index
  (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]

Result:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ Finite (M ⧸ I • N)

Tactic:
suffices (I • N).toAddSubgroup.FiniteIndex by
  exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ (I • N).toAddSubgroup.FiniteIndex

Proof state:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
inst : Finite (M ⧸ N.toAddSubgroup)
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Tactic:
exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ (I • N).toAddSubgroup.FiniteIndex

Tactic:
suffices Nat.card (N ⧸ (I • N).comap N.subtype) ≠ 0 by
  constructor
  rw [← AddSubgroup.relindex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
  exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Proof state:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Tactic:
have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›

Result:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
inst : Finite (M ⧸ N.toAddSubgroup)
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
this : Module.Finite R ↥N
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Tactic:
have : Finite ((R ⧸ I) ⊗[R] N) := Module.finite_of_finite (R ⧸ I)

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
this✝ : Module.Finite R ↥N
this : Finite ((R ⧸ I) ⊗[R] ↥N)
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
this✝ : Module.Finite R ↥N
this : Finite ((R ⧸ I) ⊗[R] ↥N)
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Tactic:
exact Nat.card_pos.ne'

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ map N.subtype (comap N.subtype (I • N)) = map N.subtype (I • ⊤)

Tactic:
simp [Submodule.smul_le_right]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Tactic:
let e : (N ⧸ (I • N).comap N.subtype) ≃ₗ[R] (R ⧸ I) ⊗[R] N :=
  Submodule.quotEquivOfEq _ (I • (⊤ : Submodule R N)) (Submodule.map_injective_of_injective
    N.injective_subtype (by simp [Submodule.smul_le_right])) ≪≫ₗ
      (quotTensorEquivQuotSMul N I).symm

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.FiniteIndex

Tactic:
constructor

Result:
case finiteIndex
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.index ≠ 0