awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
inr :
  ∀ (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}

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq R (B + 1)

Premises used: Infinite.exists_subset_card_eq, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}

Tactic:
Set.Finite.of_diff ?_ (Set.finite_singleton ⊥)

Premises used: Bot.bot, Set.finite_singleton, Set.Finite.of_diff
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
inr : 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}

Tactic:
refine Set.Finite.of_diff ?_ (Set.finite_singleton ⊥)

Premises used: Bot.bot, Set.finite_singleton, Set.Finite.of_diff
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
this :
  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})
x : R
hx : x ∈ (↑t : Set R)
⊢ x ≠ 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
inr :
  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 (α := Ideal R) ({I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})

Tactic:
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
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (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
⊢ Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}

Tactic:
rw [Set.mem_diff, Set.mem_setOf, Submodule.cardQuot_apply] at hI

Premises used: Set.mem_setOf, Set.mem_diff, Submodule.cardQuot_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
inr : ∃ i ∈ t, i ∈ I
⊢ Membership.mem (γ := Set (Submodule R R)) (⋃ x ∈ t, {I : Submodule R R | x ∈ I}) I

Tactic:
simp_rw [Set.mem_iUnion, exists_prop, Set.mem_setOf_eq]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
⊢ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
have := finiteQuotient hI.2
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this : Finite.{u_1 + 1} (R ⧸ I)
have :
  ∀ (this : Fintype (R ⧸ I)),
    Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card

Tactic:
have := Fintype.ofFinite (R ⧸ I)
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this_1 : Finite.{u_1 + 1} (R ⧸ I)
this : Fintype (R ⧸ I)
grw : Fintype.card.{u_1} (R ⧸ I) < s.card
grw₁ : Nat.card.{u_1} (R ⧸ I) < s.card
grw₂ : B < s.card
grw₃ : B < B + 1
grw₄ grw₅ : B ≤ B
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card

Tactic:
grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]

Premises used: Nat.lt_add_one_iff, Finset.card_le_univ, And.left, Fintype.card_eq_nat_card
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card

Tactic:
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]
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
inr :
  ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s) (hxy : x ≠ y)
    (h :
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)),
    ∃ i ∈ t, i ∈ I
⊢ ∃ i ∈ t, i ∈ I

Tactic:
obtain ⟨x, hx, y, hy, hxy, h⟩ := Finset.exists_ne_map_eq_of_card_image_lt hs

Premises used: Finset.exists_ne_map_eq_of_card_image_lt
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h_1 : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ ∃ i ∈ t, i ∈ I

Tactic:
⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩

Premises used: Submodule.Quotient.eq, HSub.hSub, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h_1 : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
inr : x - y ∈ t
⊢ ∃ i ∈ t, i ∈ I

Tactic:
refine ⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h_1 : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ x - y ∈ t

Tactic:
Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, Finset.mem_sub, Finset.mem_sdiff, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h_1 : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
inr : x - y ∉ {0}
⊢ x - y ∈ t

Tactic:
refine Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩

Premises used: Iff.mpr, Finset.mem_sub, Finset.mem_sdiff, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h_1 : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
inr : x - y ≠ 0
inr₁ inr₂ inr₃ inr₄ : x ≠ y
⊢ x - y ∉ {0}

Tactic:
rwa [Finset.notMem_singleton, sub_ne_zero]

Premises used: Finset.notMem_singleton, sub_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
inst_2 : IsDedekindDomain R
inst_3 : Module.Free ℤ R
B : ℕ
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | (Ideal.absNorm : (a : Ideal R) → ℕ) I ≤ B}

Tactic:
finite_cardQuot_le B

Premises used: AddSubgroup.index, setOf, Nat.card, Submodule.cardQuot, Ring.HasFiniteQuotients.finite_cardQuot_le, ENat.toNat, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
⊢ Set.MapsTo (β := Ideal R) (fun (x : IsDedekindDomain.HeightOneSpectrum R) ↦ x.asIdeal)
    {p : IsDedekindDomain.HeightOneSpectrum R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) p.asIdeal ≤ B}
    {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}

Tactic:
simp [Set.MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
inst_2 : IsDedekindDomain R
inst_3 : Module.Free ℤ R
B : ℕ
⊢ Set.Finite.{u_1} (α := IsDedekindDomain.HeightOneSpectrum R)
    {p : IsDedekindDomain.HeightOneSpectrum R | (Ideal.absNorm : (a : Ideal R) → ℕ) p.asIdeal ≤ B}

Tactic:
finite_cardQuot_heightOneSpectrum_le B

Premises used: AddSubgroup.index, setOf, Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le, Nat.card, Submodule.cardQuot, ENat.toNat, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
⊢ Northcott (β := ℕ) fun (p : Ideal R) ↦ Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) p

Tactic:
⟨Ring.HasFiniteQuotients.finite_cardQuot_le⟩

Premises used: Northcott.mk, Ring.HasFiniteQuotients.finite_cardQuot_le
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
inst_2 : IsDedekindDomain R
inst_3 : Module.Free ℤ R
⊢ Northcott (β := ℕ) fun (p : IsDedekindDomain.HeightOneSpectrum R) ↦ (Ideal.absNorm : (a : Ideal R) → ℕ) p.asIdeal

Tactic:
⟨Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le⟩

Premises used: Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, Northcott.mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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)
inr : ∀ (hR : Nontrivial R), Finite.{u_2 + 1} (S ⧸ I)
⊢ Finite.{u_2 + 1} (S ⧸ I)

Tactic:
obtain hR | hR := subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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 S

Tactic:
have : Finite S := Module.finite_of_finite R
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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
this : Finite S
⊢ Finite.{u_2 + 1} (S ⧸ I)

Tactic:
Quotient.finite _

Premises used: Quotient.finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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
this : Finite S
⊢ Finite.{u_2 + 1} (S ⧸ I)

Tactic:
exact Quotient.finite _

Premises used: Quotient.finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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_1 + 1} (R ⧸ J)

Tactic:
have : Finite (R ⧸ J) := finiteQuotient <| Ideal.under_ne_bot R hI
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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)
⊢ Module.Finite.{u_1, u_2} (R ⧸ J) (S ⧸ I)

Tactic:
have : Module.Finite (R ⧸ J) (S ⧸ I) := Module.Finite.of_restrictScalars_finite R _ _
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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_1 : Finite.{u_1 + 1} (R ⧸ J)
this : Module.Finite.{u_1, u_2} (R ⧸ J) (S ⧸ I)
⊢ Finite.{u_2 + 1} (S ⧸ I)

Tactic:
Module.finite_of_finite (R ⧸ J)

Premises used: HasQuotient.Quotient, Module.finite_of_finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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_1 : Finite.{u_1 + 1} (R ⧸ J)
this : Module.Finite.{u_1, u_2} (R ⧸ J) (S ⧸ I)
⊢ Finite.{u_2 + 1} (S ⧸ I)

Tactic:
exact Module.finite_of_finite (R ⧸ J)

Premises used: HasQuotient.Quotient, Module.finite_of_finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
I : Ideal ℤ
hI : I ≠ ⊥
obtain : ∀ (n : ℤ) (hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥), Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (ℤ ∙ n))
⊢ Finite (ℤ ⧸ I)

Tactic:
obtain ⟨n, rfl⟩ := Submodule.IsPrincipal.principal I

Premises used: Submodule.IsPrincipal.principal, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥
⊢ n ≠ 0

Tactic:
simpa using hI
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by simpa using hI⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥
this : NeZero n
⊢ Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (ℤ ∙ n))

Tactic:
inferInstanceAs <| Finite (ℤ ⧸ Ideal.span {n})

Premises used: _private.0.Ring.HasFiniteQuotients.instInt._proof_1
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hI : Ne (α := Ideal ℤ) (ℤ ∙ n) ⊥
this : NeZero n
⊢ Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (ℤ ∙ n))

Tactic:
exact inferInstanceAs <| Finite (ℤ ⧸ Ideal.span {n})
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddGroup.FG R
⊢ HasFiniteQuotients R

Tactic:
of_module_finite ℤ R

Premises used: Int, Ring.HasFiniteQuotients.of_module_finite
-- 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
this : (I • N).toAddSubgroup.FiniteIndex
⊢ Finite.{u_2 + 1} (M ⧸ I • N)

Tactic:
(I • N).toAddSubgroup.finite_quotient_of_finiteIndex

Premises used: AddSubgroup.finite_quotient_of_finiteIndex, Submodule.quotientRel
-- 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
this : (I • N).toAddSubgroup.FiniteIndex
⊢ Finite.{u_2 + 1} (M ⧸ I • N)

Tactic:
exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex

Premises used: AddSubgroup.finite_quotient_of_finiteIndex
-- 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
suffices : (I • N).toAddSubgroup.FiniteIndex
⊢ Finite.{u_2 + 1} (M ⧸ I • N)

Tactic:
suffices (I • N).toAddSubgroup.FiniteIndex by
    exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex
-- 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
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
index_ne_zero : (I • N).toAddSubgroup.index ≠ 0
⊢ (I • N).toAddSubgroup.FiniteIndex

Tactic:
constructor
-- 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
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
index_ne_zero : (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0
⊢ (I • N).toAddSubgroup.index ≠ 0

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)
inst_4 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ Finite.{u_2 + 1} (M ⧸ N.toAddSubgroup)

Tactic:
have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
I : Ideal R
N : Submodule R M
inst_4 : Finite.{u_1 + 1} (R ⧸ I)
inst_5 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
inst : Finite.{u_2 + 1} (M ⧸ N.toAddSubgroup)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Tactic:
mul_ne_zero this AddSubgroup.index_ne_zero_of_finite

Premises used: AddSubgroup.index_ne_zero_of_finite, mul_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Index
Goal:
R : Type u_1
M : Type u_2
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
I : Ideal R
N : Submodule R M
inst_4 : Finite.{u_1 + 1} (R ⧸ I)
inst_5 : Finite.{u_2 + 1} (M ⧸ N)
hN : N.FG
this : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
inst : Finite.{u_2 + 1} (M ⧸ N.toAddSubgroup)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≠ 0

Tactic:
exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite

Premises used: AddSubgroup.index_ne_zero_of_finite, mul_ne_zero
-- 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
suffices : Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.FiniteIndex

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
-- 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
⊢ 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)
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)
rw : Nat.card (TensorProduct.{u_1, u_1, u_2} R (R ⧸ I) ↥N) ≠ 0
⊢ Nat.card.{u_2} (↥N ⧸ comap N.subtype (I • N)) ≠ 0

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)
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)
⊢ Module.Finite.{u_1, u_2} R ↥N

Tactic:
have : Module.Finite R N := .of_fg hN