awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
refine :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Set M) {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} x)
    (a b : M) (x : Membership.mem (γ := Submonoid M) (Submonoid.closure S) a)
    (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) b)
    (ha : (fun (x : M) (x_2 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) a x)
    (hb : (fun (x : M) (x_2 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) b x_1)
    (h : Irreducible (a * b)), a * b ∈ S
⊢ {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} ⊆ S

Tactic:
refine fun x hx ↦
      Submonoid.closure_induction (s := S) (motive := fun x _ ↦ (Irreducible x → x ∈ S))
      (fun _ hx _ ↦ hx) (by simp) (fun a b _ _ ha hb h ↦ ?_) hx.1 hx.2

Premises used: Submonoid.closure_induction
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
x : M
hx : Membership.mem (γ := Set M) {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} x
a b : M
h_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) a
h_2 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) b
ha : (fun (x : M) (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) a h_1
hb : (fun (x : M) (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) b h_2
h : Irreducible (a * b)
inl :
  Membership.mem (γ := Submonoid M) (Submonoid.closure S) 1 →
    ∀ (ha : Irreducible.{u_1} (M := M) 1 → 1 ∈ S) (h : Irreducible (1 * b)), 1 * b ∈ S
inr :
  Membership.mem (γ := Submonoid M) (Submonoid.closure S) 1 →
    ∀ (hb : Irreducible.{u_1} (M := M) 1 → 1 ∈ S) (h : Irreducible (a * 1)), a * 1 ∈ S
⊢ a * b ∈ S

Tactic:
obtain rfl | rfl := h.eq_one_or_eq_one

Premises used: Irreducible.eq_one_or_eq_one, rfl
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
x : M
hx : Membership.mem (γ := Set M) {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} x
b : M
h_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) b
hb : (fun (x : M) (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) b h_1
h_2 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) 1
ha : Irreducible.{u_1} (M := M) 1 → 1 ∈ S
h : Irreducible (1 * b)
⊢ 1 * b ∈ S

Tactic:
simp_all
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
x : M
hx : Membership.mem (γ := Set M) {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} x
a : M
h_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) a
ha : (fun (x : M) (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) a h_1
h_2 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) 1
hb : Irreducible.{u_1} (M := M) 1 → 1 ∈ S
h : Irreducible (a * 1)
⊢ a * 1 ∈ S

Tactic:
simp_all
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
hS : Eq (α := Submonoid M) (Submonoid.closure S) ⊤
⊢ {p : M | Irreducible p} ⊆ S

Tactic:
simpa [hS] using irreducible_mem_submonoidClosure_subset (S := S)

Premises used: irreducible_mem_submonoidClosure_subset
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Submonoid M
hS : S.FG
obtain : ∀ (T : Finset M) (hT : closure (↑T : Set M) = S), Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}
⊢ Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}

Tactic:
obtain ⟨T, hT⟩ := hS
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Submonoid M
T : Finset M
hT : closure (↑T : Set M) = S
⊢ Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}

Tactic:
T.finite_toSet.subset <| hT ▸ irreducible_mem_submonoidClosure_subset

Premises used: Eq.rec, Set.Finite.subset, Finset.finite_toSet, irreducible_mem_submonoidClosure_subset
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Submonoid M
T : Finset M
hT : closure (↑T : Set M) = S
⊢ Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}

Tactic:
exact T.finite_toSet.subset <| hT ▸ irreducible_mem_submonoidClosure_subset

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
⊢ Set.Finite.{u_1} (α := M) {p : M | Irreducible p}

Tactic:
simpa using Monoid.FG.fg_top.finite_irreducible_mem_submonoidClosure

Premises used: Monoid.FG.fg_top, Submonoid.FG.finite_irreducible_mem_submonoidClosure
-- 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
obtain :
  ∀ (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}) ⊤
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤

Tactic:
obtain ⟨S, hSgen, hSmax⟩ := Submonoid.exists_minimal_closure_eq_top M

Premises used: Submonoid.exists_minimal_closure_eq_top
-- 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
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 (α := Submonoid M) (closure (↑S : Set M)) ⊤

Tactic:
hSgen
-- 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
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
h : {p : M | Irreducible p} = (↑S : Set M)
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤

Tactic:
convert! hSgen
-- 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
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)

Tactic:
(irreducible_subset_of_submonoidClosure_eq_top hSgen).antisymm fun r hrS ↦ ?_

Premises used: irreducible_subset_of_submonoidClosure_eq_top, HasSubset.Subset.antisymm
-- 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
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
h : ∀ (r : M) (hrS : r ∈ (↑S : Set M)), Membership.mem (γ := Set M) {p : M | Irreducible p} r
⊢ {p : M | Irreducible p} = (↑S : Set M)

Tactic:
refine (irreducible_subset_of_submonoidClosure_eq_top hSgen).antisymm fun r hrS ↦ ?_

Premises used: irreducible_subset_of_submonoidClosure_eq_top, HasSubset.Subset.antisymm
-- 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
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)
h : ∀ (hrirred : r ∉ {p : M | Irreducible p}), False
⊢ Membership.mem (γ := Set M) {p : M | Irreducible p} r

Tactic:
by_contra hrirred
-- 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
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}
h : ∀ (hrS : 1 ∈ (↑S : Set M)) (hrirred : 1 ∉ {p : M | Irreducible p}), False
h₁ : ∀ (hr₀ : r ≠ 1), False
⊢ False

Tactic:
obtain rfl | hr₀ := eq_or_ne r 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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
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}
⊢ (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) (S \ {1})

Tactic:
simpa
-- 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
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

Tactic:
simpa using hSmax (y := S \ {1}) (by simpa) Finset.sdiff_subset hrS

Premises used: Finset.sdiff_subset
-- 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
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
⊢ ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1

Tactic:
simp only [irreducible_iff, Set.mem_setOf_eq, not_and, not_forall, not_or] at hrirred

Premises used: Set.mem_setOf_eq, not_or, irreducible_iff, not_and, Classical.not_forall
-- 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
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
⊢ ¬IsUnit r

Tactic:
simpa
-- 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
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
h : ∀ (a b : M) (hr : r = a * b) (ha : ¬IsUnit a) (hb : ¬IsUnit b), False
⊢ False

Tactic:
obtain ⟨a, b, hr, ha, hb⟩ := hrirred <| by simpa
-- 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
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
rw : Membership.mem (γ := Submonoid M) ⊤ a
⊢ Membership.mem (γ := Submonoid M) (closure (↑S : Set M)) a

Tactic:
rw [hSgen]
-- 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
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
⊢ Membership.mem (γ := Submonoid M) ⊤ a

Tactic:
mem_top _

Premises used: Submonoid.mem_top
-- 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
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
⊢ Membership.mem (γ := Submonoid M) ⊤ a

Tactic:
exact mem_top _

Premises used: Submonoid.mem_top
-- 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
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
h : ∀ (m : M → ℕ) (hm : ∏ a ∈ S, a ^ m a = a), False
⊢ False

Tactic:
obtain ⟨m, -, hm⟩ := Submonoid.mem_closure_finset (x := a).mp (by rw [hSgen]; exact mem_top _)

Premises used: Submonoid.mem_closure_finset, Iff.mp
-- 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
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
rw : Membership.mem (γ := Submonoid M) ⊤ b
⊢ Membership.mem (γ := Submonoid M) (closure (↑S : Set M)) b

Tactic:
rw [hSgen]
-- 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
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
⊢ Membership.mem (γ := Submonoid M) ⊤ b

Tactic:
mem_top _

Premises used: Submonoid.mem_top
-- 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
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
⊢ Membership.mem (γ := Submonoid M) ⊤ b

Tactic:
exact mem_top _

Premises used: Submonoid.mem_top
-- 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
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
h : ∀ (n : M → ℕ) (hn : ∏ a ∈ S, a ^ n a = b), False
⊢ False

Tactic:
obtain ⟨n, -, hn⟩ := Submonoid.mem_closure_finset (x := b).mp (by rw [hSgen]; exact mem_top _)

Premises used: Submonoid.mem_closure_finset, Iff.mp
-- 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
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
rw : ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
rw₁ : ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
rw₂ rw₃ : r ^ m r * ∏ x ∈ S.erase r, x ^ m x = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
⊢ a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s

Tactic:
rw [← hm, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]

Premises used: Finset.sdiff_singleton_eq_erase, Finset.mul_prod_erase
-- 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
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
⊢ a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s

Tactic:
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]
-- 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
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
rw : ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
rw₁ : ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
rw₂ rw₃ : r ^ n r * ∏ x ∈ S.erase r, x ^ n x = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
⊢ b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s

Tactic:
rw [← hn, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]

Premises used: Finset.sdiff_singleton_eq_erase, Finset.mul_prod_erase
-- 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
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
⊢ b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s

Tactic:
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]
-- 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
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
rwa : r = (r ^ m r * r ^ n r * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
rwa₁ : r = r ^ m r * r ^ n r * HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
rwa₂ : r = r ^ m r * (r ^ n r * HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s))
rwa₃ : r = r ^ m r * ((r ^ n r * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s)
rwa₄ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * r ^ n r * ∏ s ∈ S \ {r}, s ^ n s)
rwa₅ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * (r ^ n r * ∏ s ∈ S \ {r}, s ^ n s))
rwa₆ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * b)
rwa₇ : r = (r ^ m r * ∏ s ∈ S \ {r}, s ^ m s) * b
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : r = a * b
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s

Tactic:
rwa [pow_add, mul_assoc, mul_assoc, ← mul_assoc (r ^ n r), mul_comm (r ^ n r) _, mul_assoc,
      ← hn, ← mul_assoc, ← hm]

Premises used: mul_assoc, pow_add, HPow.hPow, mul_comm
-- 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
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
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s

Tactic:
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]
-- 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
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_1 : 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
hr : m r + n r = 0
⊢ r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)

Tactic:
simp only [hr, pow_zero, one_mul] at hr'

Premises used: pow_zero, one_mul