awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
this : Module.Finite.{u_1, u_2} R ↥N
⊢ Finite (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)

Tactic:
have : Finite ((R ⧸ I) ⊗[R] N) := Module.finite_of_finite (R ⧸ I)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
this_1 : Module.Finite.{u_1, u_2} R ↥N
this : Finite (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0

Tactic:
Nat.card_pos.ne'

Premises used: Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
this_1 : Module.Finite.{u_1, u_2} R ↥N
this : Finite (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0

Tactic:
exact Nat.card_pos.ne'

Premises used: Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
intro :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index

Tactic:
cases nonempty_fintype (R ⧸ I)

Premises used: HasQuotient.Quotient, nonempty_fintype
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
intro :
  (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index

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

Premises used: AddSubgroup.relIndex_mul_index, Submodule.smul_le_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
intro : (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
intro : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card

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

Premises used: Membership.mem, Subtype, Nat.card, HasQuotient.Quotient, Submodule.comap, Submodule.subtype, Finset.card, HSMul.hSMul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
⊢ map N.subtype (comap N.subtype (I • N)) = map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤)

Tactic:
simp [Submodule.smul_le_right]

Premises used: Submodule.smul_le_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
intro : Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
⊢ Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card

Tactic:
rw [Nat.card_congr e.toEquiv]

Premises used: Nat.card_congr, LinearEquiv.toEquiv
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
rw : span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
rw₁ :
  Eq (α := Submodule R M) (span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) (span R (↑s : Set M))
rw₂ rw₃ : Eq (α := Submodule R M) (span R (↑s : Set M)) (span R (↑s : Set M))
⊢ LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N

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

Premises used: Subtype.range_val, Finsupp.range_linearCombination
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
⊢ LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N

Tactic:
have H : LinearMap.range (Finsupp.linearCombination R (α := s) (↑)) = N := by
    rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
c : Finsupp.{u_2, u_1} (↥s) R
rw :
  ∃ (y : Finsupp.{u_2, u_1} (↥s) R),
    Eq.{u_2 + 1} (α := M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y : M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) c : M)
⊢ Membership.mem (α := M) N
    ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) c : M)

Tactic:
rw [← H, LinearMap.mem_range]

Premises used: LinearMap.mem_range
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
c : Finsupp.{u_2, u_1} (↥s) R
⊢ ∃ (y : Finsupp.{u_2, u_1} (↥s) R),
    Eq.{u_2 + 1} (α := M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y : M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) c : M)

Tactic:
exists_apply_eq_apply _ _

Premises used: exists_apply_eq_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
c : Finsupp.{u_2, u_1} (↥s) R
⊢ ∃ (y : Finsupp.{u_2, u_1} (↥s) R),
    Eq.{u_2 + 1} (α := M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y : M)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) c : M)

Tactic:
exact exists_apply_eq_apply _ _

Premises used: exists_apply_eq_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
x : ↥N
obtain :
  ∀ (y : Finsupp.{u_2, u_1} (↥s) R)
    (hy : (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y = (↑x : M)),
    ∃ (a : Finsupp.{u_2, u_1} (↥s) R), (f : (a : ↥s →₀ R) → ↥N) a = x
⊢ ∃ (a : Finsupp.{u_2, u_1} (↥s) R), (f : (a : ↥s →₀ R) → ↥N) a = x

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

Premises used: Eq.ge, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
x : ↥N
y : Finsupp.{u_2, u_1} (↥s) R
hy : (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y = (↑x : M)
⊢ ∃ (a : Finsupp.{u_2, u_1} (↥s) R), (f : (a : ↥s →₀ R) → ↥N) a = x

Tactic:
⟨y, Subtype.ext hy⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
x : ↥N
y : Finsupp.{u_2, u_1} (↥s) R
hy : (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) y = (↑x : M)
⊢ ∃ (a : Finsupp.{u_2, u_1} (↥s) R), (f : (a : ↥s →₀ R) → ↥N) a = x

Tactic:
exact ⟨y, Subtype.ext hy⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
⊢ Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := ↥N) (⇑f : (a : ↥s →₀ R) → ↥N)

Tactic:
have hf : Function.Surjective f := fun x ↦ by
    obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
hf : Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := ↥N) (⇑f : (a : ↥s →₀ R) → ↥N)
⊢ Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) (β := TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
    (⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R (R ⧸ I) ↥s)) : (↥s →₀ R ⧸ I) →ₗ[R] (R ⧸ I) ⊗[R] (↥s →₀ R))) :
      (a : ↥s →₀ R ⧸ I) → (R ⧸ I) ⊗[R] ↥N)

Tactic:
have : Function.Surjective
      (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R R (R ⧸ I) s).symm.toLinearMap) :=
    (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
hf : Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := ↥N) (⇑f : (a : ↥s →₀ R) → ↥N)
this :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) (β := TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
    (⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R (R ⧸ I) ↥s)) : (↥s →₀ R ⧸ I) →ₗ[R] (R ⧸ I) ⊗[R] (↥s →₀ R))) :
      (a : ↥s →₀ R ⧸ I) → (R ⧸ I) ⊗[R] ↥N)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card

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

Premises used: Nat.card_le_card_of_surjective, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
hf : Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := ↥N) (⇑f : (a : ↥s →₀ R) → ↥N)
this :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) (β := TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
    (⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R (R ⧸ I) ↥s)) : (↥s →₀ R ⧸ I) →ₗ[R] (R ⧸ I) ⊗[R] (↥s →₀ R))) :
      (a : ↥s →₀ R ⧸ I) → (R ⧸ I) ⊗[R] ↥N)
intro : Nat.card (Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card

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

Premises used: Nat.card_le_card_of_surjective, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
inst_3 : Finite.{u_1 + 1} (R ⧸ I)
s : Finset M
hs : span R (↑s : Set M) = N
val : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (HSMul.hSMul (β := Submodule R ↥N) I ⊤) ⋯ ≪≫ₗ
    LinearEquiv.symm (quotTensorEquivQuotSMul (↥N) I)
H :
  LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
f : Finsupp.{u_2, u_1} (↥s) R →ₗ[R] ↥N :=
  LinearMap.codRestrict N (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) ⋯
hf : Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := ↥N) (⇑f : (a : ↥s →₀ R) → ↥N)
this :
  Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) (β := TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N)
    (⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R (R ⧸ I) ↥s)) : (↥s →₀ R ⧸ I) →ₗ[R] (R ⧸ I) ⊗[R] (↥s →₀ R))) :
      (a : ↥s →₀ R ⧸ I) → (R ⧸ I) ⊗[R] ↥N)
⊢ Nat.card (Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card

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

Premises used: le_rfl, Fintype.card_finsupp, Fintype.card_coe, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
hI : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (I i).FG
hI' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Finite.{u_1 + 1} (R ⧸ I i)
empty : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ ∅, I i))

Tactic:
simp only [Finset.prod_empty, one_eq_top]

Premises used: Finset.prod_empty, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
hI : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (I i).FG
hI' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Finite.{u_1 + 1} (R ⧸ I i)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
hI : ∀ i ∈ Insert.insert a s, (I i).FG
hI' : ∀ i ∈ Insert.insert a s, Finite.{u_1 + 1} (R ⧸ I i)
insert : Finite.{u_1 + 1} (R ⧸ (∏ x ∈ s, I x) * I a)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ Insert.insert a s, I i))

Tactic:
rw [Finset.prod_insert has, mul_comm]

Premises used: Finset.prod_insert, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite.{u_1 + 1} (R ⧸ I i)
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite.{u_1 + 1} (R ⧸ I i)
⊢ Finite.{u_1 + 1} (R ⧸ I a)

Tactic:
have := hI' a (by simp)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite.{u_1 + 1} (R ⧸ I i)
this : Finite.{u_1 + 1} (R ⧸ I a)
i : ι
hi : i ∈ s
⊢ i ∈ insert a s

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)),
    Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite.{u_1 + 1} (R ⧸ I i)
this : Finite.{u_1 + 1} (R ⧸ I a)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))

Tactic:
have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))