awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
inl : Finite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr inr₁ :
  Infinite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₂ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₃ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have inr₄ : Infinite R →
  ∀ (s : Finset R) (hs : s.card = B + 1),
    Set.Finite (α := Ideal R) ({I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
Tactic: classical
  rcases finite_or_infinite R
  · apply Set.toFinite
  -- if `R` is infinite, then we can pick a finite set `s` of cardinality `B + 1`
  obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq R (B + 1)
  -- and consider the finite set `t` of nonzero differences
  let t := (s - s) \ {0}
  refine Set.Finite.of_diff ?_ (Set.finite_singleton ⊥)
  -- in a ring with finite quotients, each nonzero element is contained in only finitely many ideals
  -- so it is enough to show that each ideal `I` of norm at most `B` contains some element of `t`
  suffices {I | Submodule.cardQuot I ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I} from
    (t.finite_toSet.biUnion fun x hx ↦ finite_setOf_mem x (by grind)).subset this
  intro I hI
  rw [Set.mem_diff, Set.mem_setOf, Submodule.cardQuot_apply] at hI
  simp_rw [Set.mem_iUnion, exists_prop, Set.mem_setOf_eq]
  -- `s` has cardinality `B + 1`, but the quotient `R ⧸ I` has cardinality at most `B`
  replace hs : (s.image (Ideal.Quotient.mk I)).card < s.card := by
    have := finiteQuotient hI.2
    have := Fintype.ofFinite (R ⧸ I)
    grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
  -- so we can find distinct `x, y ∈ s` with the desired collision `x - y ∈ I`
  obtain ⟨x, hx, y, hy, hxy, h⟩ := Finset.exists_ne_map_eq_of_card_image_lt hs
  refine ⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩
  refine Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩
  rwa [Finset.notMem_singleton, sub_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
inl : Finite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr inr₁ :
  Infinite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₂ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₃ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₄ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite (α := Ideal R) ({I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have inr₅ : Infinite R →
  ∀ (s : Finset R) (hs : s.card = B + 1),
    let t := (s - s) \ {0};
    Subset (α := Set (Submodule R R))
      ({I : Submodule R R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
      (⋃ x ∈ t, {I : Submodule R R | x ∈ I})
Tactic: classical
  rcases finite_or_infinite R
  · apply Set.toFinite
  -- if `R` is infinite, then we can pick a finite set `s` of cardinality `B + 1`
  obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq R (B + 1)
  -- and consider the finite set `t` of nonzero differences
  let t := (s - s) \ {0}
  refine Set.Finite.of_diff ?_ (Set.finite_singleton ⊥)
  -- in a ring with finite quotients, each nonzero element is contained in only finitely many ideals
  -- so it is enough to show that each ideal `I` of norm at most `B` contains some element of `t`
  suffices {I | Submodule.cardQuot I ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I} from
    (t.finite_toSet.biUnion fun x hx ↦ finite_setOf_mem x (by grind)).subset this
  intro I hI
  rw [Set.mem_diff, Set.mem_setOf, Submodule.cardQuot_apply] at hI
  simp_rw [Set.mem_iUnion, exists_prop, Set.mem_setOf_eq]
  -- `s` has cardinality `B + 1`, but the quotient `R ⧸ I` has cardinality at most `B`
  replace hs : (s.image (Ideal.Quotient.mk I)).card < s.card := by
    have := finiteQuotient hI.2
    have := Fintype.ofFinite (R ⧸ I)
    grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
  -- so we can find distinct `x, y ∈ s` with the desired collision `x - y ∈ I`
  obtain ⟨x, hx, y, hy, hxy, h⟩ := Finset.exists_ne_map_eq_of_card_image_lt hs
  refine ⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩
  refine Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩
  rwa [Finset.notMem_singleton, sub_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
inl : Finite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr inr₁ :
  Infinite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₂ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₃ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr₄ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      Set.Finite (α := Ideal R) ({I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
inr₅ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      let t := (s - s) \ {0};
      Subset (α := Set (Submodule R R))
        ({I : Submodule R R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
        (⋃ x ∈ t, {I : Submodule R R | x ∈ I})
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have inr₆ : Infinite R →
  ∀ (s : Finset R) (hs : s.card = B + 1),
    let t := (s - s) \ {0};
    ∀ ⦃I : Submodule R R⦄
      (hI :
        Membership.mem (γ := Set (Submodule R R))
          ({I : Submodule R R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥}) I),
      Membership.mem (γ := Set (Submodule R R)) (⋃ x ∈ t, {I : Submodule R R | x ∈ I}) I
Tactic: classical
  rcases finite_or_infinite R
  · apply Set.toFinite
  -- if `R` is infinite, then we can pick a finite set `s` of cardinality `B + 1`
  obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq R (B + 1)
  -- and consider the finite set `t` of nonzero differences
  let t := (s - s) \ {0}
  refine Set.Finite.of_diff ?_ (Set.finite_singleton ⊥)
  -- in a ring with finite quotients, each nonzero element is contained in only finitely many ideals
  -- so it is enough to show that each ideal `I` of norm at most `B` contains some element of `t`
  suffices {I | Submodule.cardQuot I ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I} from
    (t.finite_toSet.biUnion fun x hx ↦ finite_setOf_mem x (by grind)).subset this
  intro I hI
  rw [Set.mem_diff, Set.mem_setOf, Submodule.cardQuot_apply] at hI
  simp_rw [Set.mem_iUnion, exists_prop, Set.mem_setOf_eq]
  -- `s` has cardinality `B + 1`, but the quotient `R ⧸ I` has cardinality at most `B`
  replace hs : (s.image (Ideal.Quotient.mk I)).card < s.card := by
    have := finiteQuotient hI.2
    have := Fintype.ofFinite (R ⧸ I)
    grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
  -- so we can find distinct `x, y ∈ s` with the desired collision `x - y ∈ I`
  obtain ⟨x, hx, y, hy, hxy, h⟩ := Finset.exists_ne_map_eq_of_card_image_lt hs
  refine ⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩
  refine Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩
  rwa [Finset.notMem_singleton, sub_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
S : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
⊢ Finite.{u_2 + 1} (S ⧸ I)
have inl : ∀ (hR : Subsingleton R), Finite.{u_2 + 1} (S ⧸ I)
Tactic: obtain hR | hR := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
S : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
inl : ∀ (hR : Subsingleton R), Finite.{u_2 + 1} (S ⧸ I)
⊢ Finite.{u_2 + 1} (S ⧸ I)
have inr : ∀ (hR : Nontrivial R), Finite.{u_2 + 1} (S ⧸ I)
Tactic: obtain hR | hR := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
S : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Subsingleton R
⊢ Finite.{u_2 + 1} (S ⧸ I)
have this : Finite S
Tactic: have : Finite S := Module.finite_of_finite R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
S : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Nontrivial R
J : Ideal R := Ideal.under R I
⊢ Finite.{u_2 + 1} (S ⧸ I)
have this : Finite.{u_1 + 1} (R ⧸ J)
Tactic: have : Finite (R ⧸ J) := finiteQuotient <| Ideal.under_ne_bot R hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
S : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Nontrivial R
J : Ideal R := Ideal.under R I
this : Finite.{u_1 + 1} (R ⧸ J)
⊢ Finite.{u_2 + 1} (S ⧸ I)
have this₁ : Module.Finite.{u_1, u_2} (R ⧸ J) (S ⧸ I)
Tactic: have : Module.Finite (R ⧸ J) (S ⧸ I) := Module.Finite.of_restrictScalars_finite R _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal ℤ
hI : I ≠ ⊥
⊢ Finite (ℤ ⧸ I)
have obtain : ∀ (n : ℤ) (hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥), Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (ℤ ∙ n))
Tactic: obtain ⟨n, rfl⟩ := Submodule.IsPrincipal.principal I
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥
⊢ Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (ℤ ∙ n))
have this : NeZero n
Tactic: have : NeZero n := ⟨by simpa using hI⟩
-- 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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
⊢ Finite.{u_2 + 1} (M ⧸ I • N)
have suffices : (I • N).toAddSubgroup.FiniteIndex
Tactic: suffices (I • N).toAddSubgroup.FiniteIndex by
    exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex
-- 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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.FiniteIndex
have index_ne_zero : (I • N).toAddSubgroup.index ≠ 0
Tactic: constructor
-- 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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.index ≠ 0
have index_ne_zero : (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0
Tactic: rw [← AddSubgroup.relIndex_mul_index
      (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
-- 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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0
have inst : Finite.{u_2 + 1} (M ⧸ N.toAddSubgroup)
Tactic: have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
-- 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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
⊢ (I • N).toAddSubgroup.FiniteIndex
have suffices : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
Tactic: suffices Nat.card (N ⧸ (I • N).comap N.subtype) ≠ 0 by
    constructor
    rw [← AddSubgroup.relIndex_mul_index
      (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
    have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
    exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite
-- 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)
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)
⊢ Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
have rw : Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0
Tactic: rw [Nat.card_congr e.toEquiv]
-- 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)
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)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0
have this : Module.Finite.{u_1, u_2} R ↥N
Tactic: have : Module.Finite R N := .of_fg hN
-- 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)
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
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0
have this₁ : 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)
-- 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: cases nonempty_fintype (R ⧸ I)
-- 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)
⊢ (I • N).toAddSubgroup.index ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro : (I • N).toAddSubgroup.relIndex N.toAddSubgroup * 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]
-- 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)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card * N.toAddSubgroup.index
have intro : (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
Tactic: gcongr
-- 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)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ AddSubgroup.index.{u_1} (G := R) (toAddSubgroup I) ^ s.card
have intro : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: change (Nat.card (N ⧸ (I • N).comap N.subtype)) ≤ Nat.card (R ⧸ I) ^ s.card
-- 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)
⊢ Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
have intro : Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
Tactic: rw [Nat.card_congr e.toEquiv]
-- 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)
⊢ LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
have rw : span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
Tactic: rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]
-- 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)
rw : span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
have rw₁ : Eq (α := Submodule R M) (span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) (span R (↑s : Set M))
Tactic: rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]
-- 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)
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))
⊢ LinearMap.range (M := Finsupp.{u_2, u_1} (↥s) R)
      (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) =
    N
have rw₂ : Eq (α := Submodule R M) (span R (↑s : Set M)) (span R (↑s : Set M))
Tactic: rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]
-- 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)
⊢ Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≤ Nat.card.{u_1} (R ⧸ I) ^ s.card
have H : 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]
-- 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
c : Finsupp.{u_2, u_1} (↥s) R
⊢ Membership.mem (α := M) N
    ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) c : M)
have 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)
Tactic: rw [← H, LinearMap.mem_range]