awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
⊢ ∃ (a : Finsupp.{u_2, u_1} (↥s) R), (f : (a : ↥s →₀ R) → ↥N) a = x
have 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
Tactic: obtain ⟨y, hy⟩ := H.ge x.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (hypothesis)
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))) ⋯
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
have hf : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (hypothesis)
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)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
have 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)
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 _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
have intro : Nat.card (Finsupp.{u_2, u_1} (↥s) (R ⧸ I)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: refine (Nat.card_le_card_of_surjective _ this).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro : ∀ (val : Fintype (R ⧸ I)),
  (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ 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
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
have intro₁ : ∀ (val : Fintype (R ⧸ I)),
  (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ 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
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
intro₁ :
  ∀ (val : Fintype (R ⧸ I)),
    (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
have intro₂ : ∀ (val : Fintype (R ⧸ I)),
  (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
Tactic: classical
  cases nonempty_fintype (R ⧸ I)
  rw [← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  gcongr
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
intro₁ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
      AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
intro₂ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro₃ : ∀ (val : Fintype (R ⧸ I)), Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: classical
  cases nonempty_fintype (R ⧸ I)
  rw [← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  gcongr
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
intro₁ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
      AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
intro₂ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
intro₃ : ∀ (val : Fintype (R ⧸ I)), Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
intro₄ : ∀ (val : Fintype (R ⧸ I)), Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro₅ : ∀ (val : Fintype (R ⧸ I)), Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: classical
  cases nonempty_fintype (R ⧸ I)
  rw [← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  gcongr
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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
intro₁ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
      AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
intro₂ :
  ∀ (val : Fintype (R ⧸ I)),
    (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
intro₃ : ∀ (val : Fintype (R ⧸ I)), Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
intro₄ : ∀ (val : Fintype (R ⧸ I)), Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
intro₅ :
  ∀ (val : Fintype (R ⧸ I)), Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro₆ : ∀ (val : Fintype (R ⧸ I))
  (H :
    LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
        (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
      N),
  Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: classical
  cases nonempty_fintype (R ⧸ I)
  rw [← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  gcongr
  change (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]
  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 (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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) (∏ i ∈ ∅, I i))
have empty : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
Tactic: simp only [Finset.prod_empty, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
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} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ insert a s, I i))
have insert : Finite.{u_1 + 1} (R ⧸ (∏ x ∈ s, I x) * I a)
Tactic: rw [Finset.prod_insert has, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (hypothesis)
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 ⧸ (∏ x ∈ s, I x) * I a)
have this : Finite.{u_1 + 1} (R ⧸ I a)
Tactic: have := hI' a (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (hypothesis)
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} (R ⧸ (∏ x ∈ s, I x) * I a)
have this₁ : 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]))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
s : Finset ι
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))
have empty : ∀ (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) (∏ i ∈ ∅, I i))
Tactic: induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, one_eq_top]; infer_instance
  | insert a s has IH =>
    rw [Finset.prod_insert has, mul_comm]
    have := hI' a (by simp)
    have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))
    exact Submodule.finite_quotient_smul _ (hI a (by simp))
Cleared hypotheses: s, hI, hI'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Index (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
I : ι → Ideal R
s : Finset ι
hI : ∀ i ∈ s, (I i).FG
hI' : ∀ i ∈ s, Finite.{u_1 + 1} (R ⧸ I i)
empty :
  ∀ (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) (∏ i ∈ ∅, I i))
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, I i))
have insert : ∀ (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} (HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ insert a s, I i))
Tactic: induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, one_eq_top]; infer_instance
  | insert a s has IH =>
    rw [Finset.prod_insert has, mul_comm]
    have := hI' a (by simp)
    have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))
    exact Submodule.finite_quotient_smul _ (hI a (by simp))
Cleared hypotheses: s, hI, hI'