awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
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
⊢ False
have hm₁ : 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]
Cleared hypotheses: hm
-- 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
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
have rw : ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
Tactic: rw [← hn, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]
-- 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
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
⊢ b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
have rw₁ : ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
Tactic: rw [← hn, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]
-- 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
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
⊢ b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
have rw₂ : r ^ n r * ∏ x ∈ S.erase r, x ^ n x = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
Tactic: rw [← hn, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
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
⊢ False
have hn₁ : 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]
Cleared hypotheses: hn
-- 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
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
have rwa : r = (r ^ m r * 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]
-- 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
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
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₁ : r = r ^ m r * r ^ n r * HMul.hMul (α := M) (∏ 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]
-- 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
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)
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₂ : r = r ^ m r * (r ^ n r * HMul.hMul (α := M) (∏ 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]
-- 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
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))
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₃ : r = r ^ m r * ((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]
-- 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
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)
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₄ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * r ^ n r * ∏ 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]
-- 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
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)
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₅ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * (r ^ n r * ∏ 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]
-- 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
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))
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₆ : r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * b)
Tactic: rwa [pow_add, mul_assoc, mul_assoc, ← mul_assoc (r ^ n r), mul_comm (r ^ n r) _, mul_assoc,
      ← hn, ← mul_assoc, ← hm]
-- 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
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)
⊢ r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
have rwa₇ : r = (r ^ m r * ∏ s ∈ S \ {r}, s ^ m s) * b
Tactic: rwa [pow_add, mul_assoc, mul_assoc, ← mul_assoc (r ^ n r), mul_comm (r ^ n r) _, mul_assoc,
      ← hn, ← mul_assoc, ← hm]
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
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
⊢ False
have hr' : 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]
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
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} ⊆ (↑(closure ((↑S : Set M) \ {r})) : Set M)
have hr'₁ : 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'
Cleared hypotheses: hr'
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
⊢ {r} ⊆ (↑(closure ((↑S : Set M) \ {r})) : Set M)
have rw : HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s) ∈
  (↑(closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)})) : Set M)
Tactic: rw [hr', Set.singleton_subset_iff]
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
⊢ HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s) ∈
    (↑(closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)})) : Set M)
have refine_1 : Membership.mem (γ := Submonoid M)
  (closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}))
  (∏ s ∈ S \ {r}, s ^ m s)
Tactic: refine mul_mem ?_ ?_
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
refine_1 :
  Membership.mem (γ := Submonoid M)
    (closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}))
    (∏ s ∈ S \ {r}, s ^ m s)
⊢ HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s) ∈
    (↑(closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)})) : Set M)
have refine_2 : Membership.mem (γ := Submonoid M)
  (closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}))
  (∏ s ∈ S \ {r}, s ^ n s)
Tactic: refine mul_mem ?_ ?_
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
⊢ Membership.mem (γ := Submonoid M)
    (closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}))
    (∏ s ∈ S \ {r}, s ^ m s)
have refine_1 : ∀ (s : M) (hs : s ∈ S \ {r}), s ∈ (↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}
Tactic: refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
⊢ Membership.mem (γ := Submonoid M)
    (closure ((↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}))
    (∏ s ∈ S \ {r}, s ^ n s)
have refine_2 : ∀ (s : M) (hs : s ∈ S \ {r}), s ∈ (↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}
Tactic: refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
s : M
hs : s ∈ S \ {r}
⊢ s ∈ (↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}
have refine_1 : s ∈ (↑S : Set M) \ {r}
Tactic: rw [← hr']
-- 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
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 : m r + n r = 0
hr' : r = HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)
s : M
hs : s ∈ S \ {r}
⊢ s ∈ (↑S : Set M) \ {HMul.hMul (α := M) (∏ s ∈ S \ {r}, s ^ m s) (∏ s ∈ S \ {r}, s ^ n s)}
have refine_2 : s ∈ (↑S : Set M) \ {r}
Tactic: rw [← hr']