-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
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})
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
inr₇ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      let t := (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
inr₈ :
  Infinite R →
    ∀ (s : Finset R) (hs : s.card = B + 1),
      let t := (s - s) \ {0};
      ∀ ⦃I : Submodule R R⦄ (hI : Nat.card.{u_1} (R ⧸ I) ≤ B ∧ I ∉ {⊥}), ∃ i ∈ t, i ∈ I
inr₉ :
  Infinite R →
    ∀ (s : Finset R),
      let t := (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
inr₁₀ :
  Infinite R →
    ∀ (s : Finset R),
      let t := (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
inr₁₁ :
  Infinite R →
    ∀ (s : Finset R),
      let t := (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
inr₁₂ :
  Infinite R →
    ∀ (s : Finset R) ⦃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}
⊢ 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]

Premises used: Finset.notMem_singleton, sub_ne_zero, Set.mem_iUnion, finite_or_infinite, Bot.bot, Set.mem_setOf_eq, exists_prop, Set.mem_setOf, Set.toFinite, Set.mem_diff, Set.finite_singleton, Set.Finite.of_diff, Submodule.cardQuot_apply