-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
Pick :
  ∀ (S : Finset M) (hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤)
    (hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y),
    Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤
h :
  ∀ (S : Finset M) (hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤)
    (hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y),
    {p : M | Irreducible p} = (↑S : Set M)
h₁ :
  ∀ (S : Finset M) (hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤)
    (hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y)
    (r : M) (hrS : r ∈ (↑S : Set M)), Membership.mem (γ := Set M) {p : M | Irreducible p} r
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤
have h₂ : ∀ (S : Finset M) (hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤)
  (hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y)
  (r : M) (hrS : r ∈ (↑S : Set M)) (hrirred : r ∉ {p : M | Irreducible p}), False
Tactic: classical
  -- Pick a minimal set `S` generating `M`.
  obtain ⟨S, hSgen, hSmax⟩ := Submonoid.exists_minimal_closure_eq_top M
  -- We claim that `S` is the set of irreducible elements of `M`.
  convert! hSgen
  -- We already know that `S` contains all irreducible elements...
  refine (irreducible_subset_of_submonoidClosure_eq_top hSgen).antisymm fun r hrS ↦ ?_
  -- So let us for contradiction assume that `r ∈ S` is reducible.
  by_contra hrirred
  -- If `r = 1`, then `S` isn't minimal. Contradiction.
  obtain rfl | hr₀ := eq_or_ne r 1
  · simpa using hSmax (y := S \ {1}) (by simpa) Finset.sdiff_subset hrS
  -- Else find `a`, `b` non-units such that `a * b = r`.
  simp only [irreducible_iff, Set.mem_setOf_eq, not_and, not_forall, not_or] at hrirred
  obtain ⟨a, b, hr, ha, hb⟩ := hrirred <| by simpa
  -- Write `a = ∏ s ∈ S, s ^ m s`, `b = ∏ s ∈ S, s ^ n s` for some coefficients `m`, `n`.
  obtain ⟨m, -, hm⟩ := Submonoid.mem_closure_finset (x := a).mp (by rw [hSgen]; exact mem_top _)
  obtain ⟨n, -, hn⟩ := Submonoid.mem_closure_finset (x := b).mp (by rw [hSgen]; exact mem_top _)
  -- Single out the `r` term in the two products.
  replace hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s := by
    rw [← hm, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]
  replace hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s := by
    rw [← hn, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]
  -- Multiply the two equations together to write `r` as a power (namely `m r + n r`) of itself
  -- times a product of elements of `S \ {r}` (namely `∏ s ∈ S \ {r}, s ^ (m s + n s)`).
  have hr' : r = r ^ (m r + n r) * (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s := by
    rwa [pow_add, mul_assoc, mul_assoc, ← mul_assoc (r ^ n r), mul_comm (r ^ n r) _, mul_assoc,
      ← hn, ← mul_assoc, ← hm]
  -- Case on whether that power is `0`, `1` or at least `2`.
  match hr : m r + n r with
  -- If that power is `0`, then `r` can be written as a product of elements of `S \ {r}` and `S` was
  -- not minimal. Contradiction.
  | 0 =>
    have : ({r} : Set M) ⊆ closure (S \ {r}) := by
      simp only [hr, pow_zero, one_mul] at hr'
      rw [hr', Set.singleton_subset_iff]
      refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr'] <;> simpa using hs
    specialize hSmax (y := S \ {r}) (by simp [Submonoid.closure_sdiff_eq_closure this, hSgen])
      Finset.sdiff_subset
    simpa using hSmax hrS
  -- Assume that power is `1`.
  | 1 =>
    -- By cancelling on both sides we get `∏ s ∈ S \ {r}, s ^ (m s + n s) = 1`.
    simp only [hr, pow_one, mul_assoc, eq_comm (a := r), mul_eq_left, LeftCancelMonoid.mul_eq_one,
      Finset.prod_eq_one_iff] at hr'
    -- Since `M` has a single unit, this means that
    -- `∏ s ∈ S \ {r}, s ^ m s = ∏ s ∈ S \ {r}, s ^ n s = 1`.
    -- Furthermore, `m r + n r = 1` implies that one of `m r` or `n r` is zero.
    -- Therefore one of `a` or `b` is `1`, contradicting the fact that they are non-units.
    obtain h | h : m r = 0 ∨ n r = 0 := by lia
    · obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
      simp at ha
    · obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
      simp at hb
  -- If that power is at least `2`, then we can write `1` as `r` times something.
  -- Since `M` has a single unit, this means that `r = 1`. Contradiction.
  | N + 2 => simp [hr, hr₀, pow_add, mul_assoc, mul_left_comm] at hr'