-- 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:
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
⊢ (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
cases nonempty_fintype (R ⧸ I)

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.index ≤ (toAddSubgroup I).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)
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

Tactic:
have H : LinearMap.range (Finsupp.linearCombination R (α := s) (↑)) = N := by
  rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]; rfl

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
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥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
⊢ ∃ y, (Finsupp.linearCombination R Subtype.val) y = (Finsupp.linearCombination R Subtype.val) c

Tactic:
exact exists_apply_eq_apply _ _

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
⊢ span R (Membership.mem s.val) = span R ↑s

Tactic:
rfl

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
⊢ (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
classical
cases nonempty_fintype (R ⧸ I)
rw [← AddSubgroup.relindex_mul_index
  (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
gcongr
show (Nat.card (N ⧸ (I • N).comap N.subtype)) ≤ Nat.card (R ⧸ I) ^ s.card
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
rw [Nat.card_congr e.toEquiv]
have H : LinearMap.range (Finsupp.linearCombination R (α := s) (↑)) = N := by
  rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]; rfl
let f : (s →₀ R) →ₗ[R] N := (Finsupp.linearCombination R (↑)).codRestrict _
  (fun c => by rw [← H, LinearMap.mem_range]; exact exists_apply_eq_apply _ _)
have hf : Function.Surjective f := fun x ↦ by
  obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩
have : Function.Surjective
    (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R (R ⧸ I) s).symm.toLinearMap) :=
  (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)
refine (Nat.card_le_card_of_surjective _ this).trans ?_
simp only [Nat.card_eq_fintype_card, Fintype.card_finsupp, Fintype.card_coe, le_rfl]

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
⊢ LinearMap.range (Finsupp.linearCombination R Subtype.val) = N

Tactic:
rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]

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
⊢ span R (Membership.mem s.val) = span R ↑s

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) ⋯
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
have hf : Function.Surjective f := fun x ↦ by
  obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩

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

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_finsupp, Fintype.card_coe, le_rfl]

Result:
no goals