awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
⊢ Eq (α := R ⧸ J ≃+* R ⧸ I) (RingEquiv.symm (quotEquivOfEq h)) (quotEquivOfEq ⋯)
have h₁ : ∀ (x : R ⧸ J),
  Eq (α := R ⧸ I) ((RingEquiv.symm (quotEquivOfEq h) : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)
    ((quotEquivOfEq sorry : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
⊢ IsNoetherianRing R
have refine : ∀ (I : Ideal R), I.FG
Tactic: refine (isNoetherianRing_iff_ideal_fg R).mpr fun I ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
⊢ I.FG
have pos : ∀ (hI : I = 0), I.FG
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
pos : ∀ (hI : I = 0), I.FG
⊢ I.FG
have neg : ∀ (hI : ¬I = 0), I.FG
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
⊢ I.FG
have neg : ∀ (x : R) (hx₁ : x ∈ I) (hx₂ : x ≠ 0), I.FG
Tactic: obtain ⟨x, hx₁, hx₂⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ I.FG
have neg : Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
  (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)
Tactic: refine Submodule.fg_of_fg_map_of_fg_inf_ker (Submodule.mkQ (Ideal.span {x})) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
neg :
  Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
    (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)
⊢ I.FG
have neg₁ : (I ⊓
    LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x})) (τ₁₂ := RingHom.id R)
      (Submodule.mkQ (Ideal.span {x}))).FG
Tactic: refine Submodule.fg_of_fg_map_of_fg_inf_ker (Submodule.mkQ (Ideal.span {x})) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
    (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)
have this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
Tactic: have := finiteQuotient (I := Ideal.span {x}) (by simp [hx₂])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (I ⊓
      LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x})) (τ₁₂ := RingHom.id R)
        (Submodule.mkQ (Ideal.span {x}))).FG
have neg : Submodule.FG (R := R) (Ideal.span {x})
Tactic: rw [Submodule.ker_mkQ, inf_eq_right.mpr ((Ideal.span_singleton_le_iff_mem I).mpr hx₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I ≠ ⊥
⊢ 0 < Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I
have this : Finite.{u_1 + 1} (R ⧸ I)
Tactic: have := finiteQuotient hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
x : R
hx : x ≠ 0
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | x ∈ I}
have this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
Tactic: have := finiteQuotient (mt Ideal.span_singleton_eq_bot.mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
x : R
hx : x ≠ 0
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | x ∈ I}
have this₁ : Set.Finite.{u_1} (α := Ideal R)
  {I : Ideal R |
    Ideal.comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x})) (Ideal.Quotient.mk (Ideal.span {x}))
        ⊥ ≤
      I}
Tactic: have : {I | Ideal.comap (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤ I}.Finite :=
    .of_equiv _ (Ideal.relIsoOfSurjective _ Ideal.Quotient.mk_surjective).toEquiv
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have inl : Finite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
Tactic: rcases finite_or_infinite R
-- 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}
⊢ 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 → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
Tactic: rcases finite_or_infinite R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Infinite R
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have 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}
Tactic: obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq R (B + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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}
have inr : Set.Finite (α := 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 ⊥)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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 (α := Ideal R) ({I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B} \ {⊥})
have 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})
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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
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
⊢ Membership.mem (γ := Set (Submodule R R)) (⋃ x ∈ t, {I : Submodule R R | x ∈ I}) I
have hI₁ : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}
Tactic: rw [Set.mem_diff, Set.mem_setOf, Submodule.cardQuot_apply] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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 ∉ {⊥}
⊢ Membership.mem (γ := Set (Submodule R R)) (⋃ x ∈ t, {I : Submodule R R | x ∈ I}) I
have inr : ∃ i ∈ t, i ∈ I
Tactic: simp_rw [Set.mem_iUnion, exists_prop, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
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
have this : Finite.{u_1 + 1} (R ⧸ I)
Tactic: have := finiteQuotient hI.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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)
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have have : ∀ (this : Fintype (R ⧸ I)),
  Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
Tactic: have := Fintype.ofFinite (R ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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)
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have grw : Fintype.card.{u_1} (R ⧸ I) < s.card
Tactic: grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have grw₁ : Nat.card.{u_1} (R ⧸ I) < s.card
Tactic: grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have grw₂ : B < s.card
Tactic: grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have grw₃ : B < B + 1
Tactic: grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
⊢ Finset.card (α := R ⧸ I) (Finset.image (⇑(Ideal.Quotient.mk I) : (a : R) → R ⧸ I) s) < s.card
have grw₄ : B ≤ B
Tactic: grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (hypothesis)
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 ∉ {⊥}
⊢ ∃ i ∈ t, i ∈ I
have hs₁ : 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
⊢ ∃ i ∈ t, i ∈ I
have 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
Tactic: obtain ⟨x, hx, y, hy, hxy, h⟩ := Finset.exists_ne_map_eq_of_card_image_lt hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
have inr : x - y ∈ t
Tactic: refine ⟨x - y, ?_, (Submodule.Quotient.eq I).mp h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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
have inr : x - y ∉ {0}
Tactic: refine Finset.mem_sdiff.mpr ⟨Finset.mem_sub.mpr ⟨x, hx, y, hy, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients (goal)
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 ∉ {0}
have inr : x - y ≠ 0
Tactic: 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 : ℕ
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
have inl : Finite R → Set.Finite.{u_1} (α := 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}
⊢ 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 → Set.Finite.{u_1} (α := 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}
⊢ 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.{u_1} (α := 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]