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

Tactic:
show (Nat.card (N ⧸ (I • N).comap N.subtype)) ≤ Nat.card (R ⧸ I) ^ s.card

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)
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card (R ⧸ I) ^ s.card

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
have : Function.Surjective
    (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R (R ⧸ I) s).symm.toLinearMap) :=
  (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
hf : Function.Surjective ⇑f
this : Function.Surjective ⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ ↑(finsuppScalarRight R (R ⧸ I) { x // x ∈ s }).symm)
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
let f : (s →₀ R) →ₗ[R] N := (Finsupp.linearCombination R (↑)).codRestrict _
  (fun c => by rw [← H, LinearMap.mem_range]; exact exists_apply_eq_apply _ _)

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

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)
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card (R ⧸ I) ^ s.card

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

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
c : { x // x ∈ s } →₀ R
⊢ (Finsupp.linearCombination R Subtype.val) c ∈ N

Tactic:
rw [← H, LinearMap.mem_range]

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)
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
c : { x // x ∈ s } →₀ R
⊢ ∃ y, (Finsupp.linearCombination R Subtype.val) y = (Finsupp.linearCombination R Subtype.val) c

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
hf : Function.Surjective ⇑f
this : Function.Surjective ⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ ↑(finsuppScalarRight R (R ⧸ I) { x // x ∈ s }).symm)
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
refine (Nat.card_le_card_of_surjective _ this).trans ?_

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
H : LinearMap.range (Finsupp.linearCombination R Subtype.val) = N
f : ({ x // x ∈ s } →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
hf : Function.Surjective ⇑f
this : Function.Surjective ⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ ↑(finsuppScalarRight R (R ⧸ I) { x // x ∈ s }).symm)
⊢ Nat.card ({ x // x ∈ s } →₀ R ⧸ I) ≤ Nat.card (R ⧸ I) ^ s.card