awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
rw : (p₁ -ᵥ p₁) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
have rw₁ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
Tactic: rw [vsub_add_vsub_cancel, vsub_self]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p q : P
⊢ (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)
have rw : g + (p -ᵥ q) = g - (q -ᵥ p)
Tactic: rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p q : P
rw : g + (p -ᵥ q) = g - (q -ᵥ p)
⊢ (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)
have rw₁ : g + (p -ᵥ q) = g + -(q -ᵥ p)
Tactic: rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p q : P
rw : g + (p -ᵥ q) = g - (q -ᵥ p)
rw₁ : g + (p -ᵥ q) = g + -(q -ᵥ p)
⊢ (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)
have rw₂ : g + (p -ᵥ q) = g + (p -ᵥ q)
Tactic: rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₄ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂) - g
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₄ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂) - g
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₅ : -g = -(p₁ -ᵥ p₂) + (p₁ -ᵥ p₂) - g
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₄ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂) - g
rw₅ : -g = -(p₁ -ᵥ p₂) + (p₁ -ᵥ p₂) - g
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₆ : -g = 0 - g
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₄ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂) - g
rw₅ : -g = -(p₁ -ᵥ p₂) + (p₁ -ᵥ p₂) - g
rw₆ : -g = 0 - g
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
have rw₇ : -g = -g
Tactic: rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
have rw : p₁ -ᵥ ((p₂ -ᵥ p₃) +ᵥ p₃) = p₁ -ᵥ p₂
Tactic: rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
rw : p₁ -ᵥ ((p₂ -ᵥ p₃) +ᵥ p₃) = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
have rw₁ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
Tactic: rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
have rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
Tactic: rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
have rw₁ : v₁ + (p₁ -ᵥ p₂) = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
Tactic: rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₁ : v₁ + (p₁ -ᵥ p₂) = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
have rw₂ : -v₁ + (v₁ + (p₁ -ᵥ p₂)) = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
Tactic: rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₁ : v₁ + (p₁ -ᵥ p₂) = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₂ : -v₁ + (v₁ + (p₁ -ᵥ p₂)) = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
have rw₃ : p₁ -ᵥ p₂ = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
Tactic: rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₁ : v₁ + (p₁ -ᵥ p₂) = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₂ : -v₁ + (v₁ + (p₁ -ᵥ p₂)) = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₃ : p₁ -ᵥ p₂ = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
have rw₄ : -v₁ + v₂ = p₁ -ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
Tactic: rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂
have rw : (v₁ +ᵥ p) -ᵥ p - v₂ = v₁ - v₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
rw : (v₁ +ᵥ p) -ᵥ p - v₂ = v₁ - v₂
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂
have rw₁ : v₁ + (p -ᵥ p) - v₂ = v₁ - v₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
rw : (v₁ +ᵥ p) -ᵥ p - v₂ = v₁ - v₂
rw₁ : v₁ + (p -ᵥ p) - v₂ = v₁ - v₂
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂
have rw₂ : v₁ + 0 - v₂ = v₁ - v₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
rw : (v₁ +ᵥ p) -ᵥ p - v₂ = v₁ - v₂
rw₁ : v₁ + (p -ᵥ p) - v₂ = v₁ - v₂
rw₂ : v₁ + 0 - v₂ = v₁ - v₂
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂
have rw₃ : v₁ - v₂ = v₁ - v₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ Eq (α := P) ((pointReflection x : (a : P) → P) y : P) ((Equiv.symm (pointReflection x) : (a : P) → P) y : P)
have rw : Eq (α := P) ((pointReflection x : (a : P) → P) y : P) ((pointReflection x : (a : P) → P) y : P)
Tactic: rw [pointReflection_symm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
⊢ Subsingleton G ↔ Subsingleton P
have inhabit : ∀ (inhabited_h : Inhabited P), Subsingleton G ↔ Subsingleton P
Tactic: inhabit P
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
⊢ {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} ⊆ S
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
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)
⊢ a * b ∈ S
have 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
Tactic: obtain rfl | rfl := h.eq_one_or_eq_one
Cleared hypotheses: a, h_1, ha, h
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
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
⊢ a * b ∈ S
have 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
Tactic: obtain rfl | rfl := h.eq_one_or_eq_one
Cleared hypotheses: b, h_2, hb, h
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Submonoid M
hS : S.FG
⊢ Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}
have obtain : ∀ (T : Finset M) (hT : closure (↑T : Set M) = S), Set.Finite.{u_1} (α := M) {p : M | p ∈ S ∧ Irreducible p}
Tactic: obtain ⟨T, hT⟩ := hS
Cleared hypotheses: hS
-- 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
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤
have 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}) ⊤
Tactic: obtain ⟨S, hSgen, hSmax⟩ := Submonoid.exists_minimal_closure_eq_top M
-- 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
⊢ Eq.{u_1 + 1} (α := Submonoid M) (closure {p : M | Irreducible p}) ⊤
have h : {p : M | Irreducible p} = (↑S : Set M)
Tactic: convert! hSgen
-- 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
⊢ {p : M | Irreducible p} = (↑S : Set M)
have h : ∀ (r : M) (hrS : r ∈ (↑S : Set M)), Membership.mem (γ := Set M) {p : M | Irreducible p} r
Tactic: refine (irreducible_subset_of_submonoidClosure_eq_top hSgen).antisymm fun r 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)
⊢ Membership.mem (γ := Set M) {p : M | Irreducible p} r
have h : ∀ (hrirred : r ∉ {p : M | Irreducible p}), False
Tactic: by_contra hrirred
-- 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)
hrirred : r ∉ {p : M | Irreducible p}
⊢ False
have h : ∀ (hrS : 1 ∈ (↑S : Set M)) (hrirred : 1 ∉ {p : M | Irreducible p}), False
Tactic: obtain rfl | hr₀ := eq_or_ne r 1
Cleared hypotheses: r, hrS, hrirred
-- 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)
hrirred : r ∉ {p : M | Irreducible p}
h : ∀ (hrS : 1 ∈ (↑S : Set M)) (hrirred : 1 ∉ {p : M | Irreducible p}), False
⊢ False
have h₁ : ∀ (hr₀ : r ≠ 1), False
Tactic: obtain rfl | hr₀ := eq_or_ne r 1
-- 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)
hrirred : r ∉ {p : M | Irreducible p}
hr₀ : r ≠ 1
⊢ False
have hrirred₁ : ¬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
Cleared hypotheses: hrirred
-- 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
⊢ False
have h : ∀ (a b : M) (hr : r = a * b) (ha : ¬IsUnit a) (hb : ¬IsUnit b), False
Tactic: obtain ⟨a, b, hr, ha, hb⟩ := hrirred <| by simpa
-- 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
⊢ Membership.mem (γ := Submonoid M) (closure (↑S : Set M)) a
have rw : Membership.mem (γ := Submonoid M) ⊤ a
Tactic: rw [hSgen]
-- 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
⊢ False
have h : ∀ (m : M → ℕ) (hm : ∏ a ∈ S, a ^ m a = a), False
Tactic: obtain ⟨m, -, hm⟩ := Submonoid.mem_closure_finset (x := a).mp (by rw [hSgen]; exact mem_top _)
-- 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 : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ Membership.mem (γ := Submonoid M) (closure (↑S : Set M)) b
have rw : Membership.mem (γ := Submonoid M) ⊤ b
Tactic: rw [hSgen]
-- 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 : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ False
have h : ∀ (n : M → ℕ) (hn : ∏ a ∈ S, a ^ n a = b), False
Tactic: obtain ⟨n, -, hn⟩ := Submonoid.mem_closure_finset (x := b).mp (by rw [hSgen]; exact mem_top _)
-- 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 : 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
have rw : ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
Tactic: rw [← hm, 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 : 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
⊢ a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
have rw₁ : ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
Tactic: rw [← hm, 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 : 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
⊢ a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
have rw₂ : r ^ m r * ∏ x ∈ S.erase r, x ^ m x = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
Tactic: rw [← hm, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]