-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
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
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
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)
    (hrS : 1 ∈ (↑S : Set M)) (hrirred : 1 ∉ {p : M | Irreducible p}), False
h₄ 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}) (hr₀ : r ≠ 1), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b) (m : M → ℕ) (hm : ∏ a ∈ S, a ^ m a = a), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b) (m : M → ℕ) (hm : ∏ a ∈ S, a ^ m a = a) (n : M → ℕ) (hn : ∏ a ∈ S, a ^ n a = b),
    False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b) (m n : M → ℕ) (hn : ∏ a ∈ S, a ^ n a = b)
    (hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b) (m n : M → ℕ) (hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s)
    (hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s), False
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)) (hr₀ : r ≠ 1)
    (hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1) (a b : M) (hr : r = a * b)
    (ha : ¬IsUnit a) (hb : ¬IsUnit b) (m n : M → ℕ) (hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s)
    (hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s)
    (hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s), False
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤

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'

Premises used: Submonoid.exists_minimal_closure_eq_top, Set.mem_setOf_eq, not_or, irreducible_iff, not_and, Classical.not_forall, rfl