-- Mathlib/RingTheory/Ideal/Quotient/Index.lean
lemma Submodule.index_smul_le [Finite (R ⧸ I)]
    (s : Finset M) (hs : Submodule.span R s = N) :
    (I • N).toAddSubgroup.index ≤ I.toAddSubgroup.index ^ s.card * N.toAddSubgroup.index

Proof state:
case intro
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≤
    (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
gcongr

Result:
case intro.bc
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup ≤ (toAddSubgroup I).index ^ s.card

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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ map N.subtype (comap N.subtype (I • N)) = map N.subtype (I • ⊤)

Tactic:
simp [Submodule.smul_le_right]

Result:
no goals

Proof state:
case intro
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
y : { x // x ∈ s } →₀ R
hy : (Finsupp.linearCombination R Subtype.val) y = ↑x
⊢ ∃ a, f a = x

Tactic:
exact ⟨y, Subtype.ext hy⟩

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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, hy⟩ := H.ge x.2

Result:
case intro
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
y : { x // x ∈ s } →₀ R
hy : (Finsupp.linearCombination R Subtype.val) y = ↑x
⊢ ∃ a, f a = x

Proof state:
case intro.bc
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
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)) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
rw [Nat.card_congr e.toEquiv]

Result:
case intro.bc
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
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) ≤ Nat.card (R ⧸ I) ^ s.card

Proof state:
case intro
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

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

Result:
case intro
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.relindex N.toAddSubgroup * N.toAddSubgroup.index ≤
    (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index