The proposition 1.4 of hungerford algebra textbook.

Stream: maths

[Lingwei Peng (彭灵伟)]

This question comes from the Algebra book by Hungerford.

Let G be a semigroup. Then, G is a group if for all a, b \in G, the equations a \cdot x = b and y \cdot a = b have solutions in G.

This is the code in Lean 4. Can you help me to complete EquationGroup.exists_left_inv?

import Mathlib

namespace MyAlgebra

universe u

class Magma (α : Type u) where
  op : α → α → α
infixl:70 " * " => Magma.op

class Neutral (α : Type u) where
  neutral : α
instance (priority := 300) Neutral.toOfNat1 {α} [Neutral α] : OfNat α (nat_lit 1) where
  ofNat := ‹Neutral α›.neutral
instance (priority := 200) Neutral.ofOfNat1 {α} [OfNat α (nat_lit 1)] : Neutral α where
  neutral := 1

class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

class Semigroup (G : Type u) extends Magma G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class Monoid (G : Type u) extends Semigroup G, Neutral G where
  one_mul : ∀ a : G, (1 : G) * a = a
  mul_one : ∀ a : G, a * (1 : G) = a

class Group (G : Type u) extends Monoid G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1
  mul_inv : ∀ a : G, a * a⁻¹ = 1

class CommMagma (α : Type u) extends Magma α where
  mul_comm : ∀ a b : α, a * b = b * a
class CommSemigroup (G : Type u) extends Semigroup G, CommMagma G where
class CommMonoid (G : Type u) extends Monoid G, CommSemigroup G
class CommGroup (G : Type u) extends Group G, CommSemigroup G

theorem Monoid.unique_left_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, e * a = a) : e = 1 := by
  rw [← h 1, mul_one]
theorem Monoid.unique_right_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, a * e = a) : e = 1 := by
  rw [← h 1, one_mul]

class LeftGroup (G : Type u) extends Semigroup G, Neutral G, Inv G where
  one_mul : ∀ a : G, (1 : G) * a = a
  inv_mul : ∀ a : G, a⁻¹ * a = 1
theorem LeftGroup.self_op_self_eq_one (G : Type u) [lg : LeftGroup G] (a : G) (h : a * a = a) : a = 1 := by
  rw [← lg.one_mul a]
  apply Eq.subst (motive := fun x => x * a = 1 ) (lg.inv_mul a)
  rw [lg.mul_assoc, h]
  exact lg.inv_mul a
theorem LeftGroup.mul_inv (G : Type u) [lg : LeftGroup G] (a : G) : a * a⁻¹ = 1 := by
  apply lg.self_op_self_eq_one
  rw [lg.mul_assoc]
  apply Eq.subst (motive := fun (x : G) => a * x = a * a⁻¹) (lg.mul_assoc a⁻¹ a a⁻¹)
  rw [lg.inv_mul, lg.one_mul]
theorem LeftGroup.mul_one (G : Type u) [lg : LeftGroup G] (a : G) : a * (1 : G) = a := by
  rw [← lg.inv_mul a, ← lg.mul_assoc, lg.mul_inv, lg.one_mul]
instance LeftGroup.toGroup (G : Type u) [lg : LeftGroup G] : Group G where
  one_mul := lg.one_mul
  inv_mul := lg.inv_mul
  mul_inv := lg.mul_inv
  mul_one := lg.mul_one

theorem Group.unique_left_inv {G : Type u} [g : Group G] (a b : G) (h : a * b = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.one_mul b⁻¹)
  rw [← h, g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.unique_right_inv {G : Type u} [g : Group G] (a b : G) (h : b * a = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.mul_one b⁻¹)
  rw [← h, ← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.inv_inv (G : Type u) [g : Group G] (a : G) : a⁻¹⁻¹ = a := by
  apply Eq.symm
  apply g.unique_right_inv
  exact g.inv_mul a
theorem Group.inv_self_mul {G : Type u} [g : Group G] (a b : G) : a⁻¹ * (a * b) = b := by
  rw [← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.self_inv_mul {G : Type u} [g : Group G] (a b : G) : a * (a⁻¹ * b) = b := by
  rw [← g.mul_assoc, g.mul_inv, g.one_mul]
theorem Group.mul_self_inv {G : Type u} [g : Group G] (a b : G) : a * b * b⁻¹ = a := by
  rw [g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.mul_inv_self {G : Type u} [g : Group G] (a b : G) : a * b⁻¹ * b = a := by
  rw [g.mul_assoc, g.inv_mul, g.mul_one]
theorem Group.inv_mul_inv {G : Type u} [g : Group G] (a b : G) : a⁻¹ * b⁻¹ = (b * a)⁻¹ := by
  apply g.unique_left_inv
  rw [g.mul_assoc, g.inv_self_mul, g.inv_mul]
theorem Group.cancel_left {G : Type u} [g : Group G] (a b c : G) (h : a * b = a * c) : b = c := by
  rw [← g.inv_self_mul a b, h, g.inv_self_mul]
theorem Group.cancel_right {G : Type u} [g : Group G] (a b c : G) (h : b * a = c * a) : b = c := by
  rw [← g.mul_self_inv b a, h, g.mul_self_inv]
theorem Group.ax_eq_b {G : Type u} [g : Group G] (a b x : G) (h : a * x = b) : x = a⁻¹ * b := by
  apply g.cancel_left a
  rw [g.self_inv_mul]
  exact h
theorem Group.ya_eq_b {G : Type u} [g : Group G] (a b y : G) (h : y * a = b) : y = b * a⁻¹ := by
  apply g.cancel_right a
  rw [g.mul_inv_self]
  exact h

class EquationGroup (G : Type u) extends Semigroup G where
  left : ∀ a b : G, ∃ x : G, a * x = b
  right : ∀ a b : G, ∃ x : G, x * a = b
  nonempty : ∃ _ : G, True

theorem EquationGroup.exists_left_inv (G : Type u) [eg : EquationGroup G] : ∃ x : G, ∀ a, x * a = a := by
  let some := Classical.choose eg.nonempty
  have h := eg.right some some
  let e := Classical.choose h
  have h' := Classical.choose_spec h
  apply Exists.intro e
  intro a


end MyAlgebra

[Lingwei Peng (彭灵伟)]

The problem is solved, but the code could be optimized. Could you take a look and see if it can be improvemented?

import Mathlib

namespace MyAlgebra

universe u

class Magma (α : Type u) where
  op : α → α → α
infixl:70 " * " => Magma.op

class Neutral (α : Type u) where
  neutral : α
instance (priority := 300) Neutral.toOfNat1 {α} [Neutral α] : OfNat α (nat_lit 1) where
  ofNat := ‹Neutral α›.neutral
instance (priority := 200) Neutral.ofOfNat1 {α} [OfNat α (nat_lit 1)] : Neutral α where
  neutral := 1

class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

class Semigroup (G : Type u) extends Magma G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class Monoid (G : Type u) extends Semigroup G, Neutral G where
  one_mul : ∀ a : G, (1 : G) * a = a
  mul_one : ∀ a : G, a * (1 : G) = a

class Group (G : Type u) extends Monoid G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1
  mul_inv : ∀ a : G, a * a⁻¹ = 1

class CommMagma (α : Type u) extends Magma α where
  mul_comm : ∀ a b : α, a * b = b * a
class CommSemigroup (G : Type u) extends Semigroup G, CommMagma G where
class CommMonoid (G : Type u) extends Monoid G, CommSemigroup G
class CommGroup (G : Type u) extends Group G, CommSemigroup G

theorem Monoid.unique_left_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, e * a = a) : e = 1 := by
  rw [← h 1, mul_one]
theorem Monoid.unique_right_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, a * e = a) : e = 1 := by
  rw [← h 1, one_mul]

class LeftGroup (G : Type u) extends Semigroup G, Neutral G, Inv G where
  one_mul : ∀ a : G, (1 : G) * a = a
  inv_mul : ∀ a : G, a⁻¹ * a = 1
theorem LeftGroup.self_op_self_eq_one (G : Type u) [lg : LeftGroup G] (a : G) (h : a * a = a) : a = 1 := by
  rw [← lg.one_mul a]
  apply Eq.subst (motive := fun x => x * a = 1 ) (lg.inv_mul a)
  rw [lg.mul_assoc, h]
  exact lg.inv_mul a
theorem LeftGroup.mul_inv (G : Type u) [lg : LeftGroup G] (a : G) : a * a⁻¹ = 1 := by
  apply lg.self_op_self_eq_one
  rw [lg.mul_assoc]
  apply Eq.subst (motive := fun (x : G) => a * x = a * a⁻¹) (lg.mul_assoc a⁻¹ a a⁻¹)
  rw [lg.inv_mul, lg.one_mul]
theorem LeftGroup.mul_one (G : Type u) [lg : LeftGroup G] (a : G) : a * (1 : G) = a := by
  rw [← lg.inv_mul a, ← lg.mul_assoc, lg.mul_inv, lg.one_mul]
instance LeftGroup.toGroup (G : Type u) [lg : LeftGroup G] : Group G where
  one_mul := lg.one_mul
  inv_mul := lg.inv_mul
  mul_inv := lg.mul_inv
  mul_one := lg.mul_one

theorem Group.unique_left_inv {G : Type u} [g : Group G] (a b : G) (h : a * b = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.one_mul b⁻¹)
  rw [← h, g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.unique_right_inv {G : Type u} [g : Group G] (a b : G) (h : b * a = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.mul_one b⁻¹)
  rw [← h, ← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.inv_inv (G : Type u) [g : Group G] (a : G) : a⁻¹⁻¹ = a := by
  apply Eq.symm
  apply g.unique_right_inv
  exact g.inv_mul a
theorem Group.inv_self_mul {G : Type u} [g : Group G] (a b : G) : a⁻¹ * (a * b) = b := by
  rw [← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.self_inv_mul {G : Type u} [g : Group G] (a b : G) : a * (a⁻¹ * b) = b := by
  rw [← g.mul_assoc, g.mul_inv, g.one_mul]
theorem Group.mul_self_inv {G : Type u} [g : Group G] (a b : G) : a * b * b⁻¹ = a := by
  rw [g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.mul_inv_self {G : Type u} [g : Group G] (a b : G) : a * b⁻¹ * b = a := by
  rw [g.mul_assoc, g.inv_mul, g.mul_one]
theorem Group.inv_mul_inv {G : Type u} [g : Group G] (a b : G) : a⁻¹ * b⁻¹ = (b * a)⁻¹ := by
  apply g.unique_left_inv
  rw [g.mul_assoc, g.inv_self_mul, g.inv_mul]
theorem Group.cancel_left {G : Type u} [g : Group G] (a b c : G) (h : a * b = a * c) : b = c := by
  rw [← g.inv_self_mul a b, h, g.inv_self_mul]
theorem Group.cancel_right {G : Type u} [g : Group G] (a b c : G) (h : b * a = c * a) : b = c := by
  rw [← g.mul_self_inv b a, h, g.mul_self_inv]
theorem Group.ax_eq_b {G : Type u} [g : Group G] (a b x : G) (h : a * x = b) : x = a⁻¹ * b := by
  apply g.cancel_left a
  rw [g.self_inv_mul]
  exact h
theorem Group.ya_eq_b {G : Type u} [g : Group G] (a b y : G) (h : y * a = b) : y = b * a⁻¹ := by
  apply g.cancel_right a
  rw [g.mul_inv_self]
  exact h

class EquationGroup (G : Type u) extends Semigroup G where
  left : ∀ a b : G, ∃ x : G, a * x = b
  right : ∀ a b : G, ∃ x : G, x * a = b
  nonempty : ∃ _ : G, True

theorem EquationGroup.exists_left_neutral{G : Type u} [eg : EquationGroup G] : ∃ x : G, ∀ a, x * a = a := by
  let some := Classical.choose eg.nonempty
  have h₁ := eg.right some some
  let e := Classical.choose h₁
  have he := Classical.choose_spec h₁
  apply Exists.intro e
  intro a
  have h₃ := eg.left a a
  let e' := Classical.choose h₃
  have he' := Classical.choose_spec h₃
  have h_some_inv := Classical.choose_spec (eg.left some e')
  have h_a_inv := Classical.choose_spec (eg.right a e)
  have h₇ : e * e' = e' := by
    apply Eq.subst (motive := fun x => e * x = e') h_some_inv
    rw [← eg.mul_assoc, he, h_some_inv]
  have h₈ : e * e' = e := by
    apply Eq.subst (motive := fun x => x * e' = e) h_a_inv
    rw [eg.mul_assoc, he', h_a_inv]
  have h₉ : e = e' := by
    apply Eq.trans _ h₇
    apply Eq.symm h₈
  rw [h₉]
  have h10 := eg.right a a
  let e'' := Classical.choose h10
  have he'' := Classical.choose_spec h10
  have h11 := Classical.choose_spec (eg.right a e'')
  have h12 : e'' * e' = e'' := by
    apply Eq.subst (motive := fun x => x * e' = e'') h11
    rw [eg.mul_assoc, he', h11]
  have h13 := Classical.choose_spec (eg.left a e')
  have h14 : e'' * e' = e' := by
    apply Eq.subst (motive := fun x => e'' * x = e') h13
    rw [← eg.mul_assoc, he'', h13]
  have h15 : e' = e'' := by
    apply Eq.trans _ h12
    apply Eq.symm h14
  rw [h15]
  exact he''

noncomputable def EquationGroup.neutral{G : Type u} [eg : EquationGroup G] := Classical.choose (EquationGroup.exists_left_neutral (G := G))
theorem EquationGroup.one_mul{G : Type u} [eg : EquationGroup G] : ∀ a : G, EquationGroup.neutral * a = a := Classical.choose_spec (EquationGroup.exists_left_neutral (G := G))
noncomputable def EquationGroup.inv{G: Type u} [eg : EquationGroup G] := fun (a : G) => Classical.choose (eg.right a EquationGroup.neutral)
theorem EquationGroup.inv_mul{G : Type u} [eg : EquationGroup G] : ∀ a : G, (EquationGroup.inv a) * a = EquationGroup.neutral := by
  intro a
  simp [EquationGroup.inv]
  apply Classical.choose_spec (eg.right a EquationGroup.neutral)

noncomputable instance EquationGroup.toLeftGroup (G : Type u) [eg : EquationGroup G] : LeftGroup G where
  neutral := EquationGroup.neutral
  inv := EquationGroup.inv
  one_mul := EquationGroup.one_mul
  inv_mul := EquationGroup.inv_mul

noncomputable instance EquationGroup.toGroup (G : Type u) [eg : EquationGroup G] : Group G :=
  LeftGroup.toGroup (G := G)

end MyAlgebra

[Yury G. Kudryashov]

Why don't you reuse Mathlib's algebraic hierarchy?

[Yury G. Kudryashov]

Also, why have you decided to formalize this particular problem?

[Lingwei Peng (彭灵伟)]

I’m currently studying the group section in mathlib. I usually learn the source code by building a small code around it. Don’t laugh—I’ve been stuck on this problem for quite a while.

[Yury G. Kudryashov]

If you're looking for exercises, then you can

• reformulate the theorem in terms of Mathlib classes;
• prove this version and PR it to Mathlib.

[Yury G. Kudryashov]

BTW, is it enough to require that one of these divisions is possible?

[Kevin Buzzard]

I think that rolling your own algebra heirarchy can be a good exercise to learn something about the system, but ultimately it's kind of futile building on it because if you want to get anywhere then you need so many helper lemmas and domain-specific tactics that you may as well just use mathlib. A couple of comments on your code:

-- line 49
  nth_rw 1 [← lg.inv_mul a]
  --apply Eq.subst (motive := fun x => x * a = 1 ) (lg.inv_mul a)

I would never use Eq.subst directly; we have tactics which can do anything you want. Another example:

-- line 55
  rw [← lg.mul_assoc a⁻¹]
  --apply Eq.subst (motive := fun (x : G) => a * x = a * a⁻¹) (lg.mul_assoc a⁻¹ a a⁻¹)

Also, you don't need to use all this Classical.choose stuff when your goal is a prop: here is the first half of one of your theorems, with all the Classical stuff removed, and using calc which is a far less painful way to do it than your continual have's (I skip h7 and h8).

theorem EquationGroup.exists_left_neutral{G : Type u} [eg : EquationGroup G] : ∃ x : G, ∀ a, x * a = a := by
  obtain ⟨some, _⟩ := eg.nonempty
  obtain ⟨e, he⟩ := eg.right some some
  use e
  intro a
  obtain ⟨e', he'⟩ := eg.left a a
  obtain ⟨some_inv, h_some_inv⟩ := eg.left some e'
  obtain ⟨a_inv, h_a_inv⟩ := eg.right a e
  have h₉ : e = e' := calc
    e = a_inv * a * e' := by rw [eg.mul_assoc, he', h_a_inv]
    _ = e * e' := by rw [h_a_inv]
    _ = e * (some * some_inv) := by rw [h_some_inv]
    _ = e' := by rw [← eg.mul_assoc, he, h_some_inv]
  rw [h₉]
  ...

I couldn't face doing any more but you get the point. If you look at the proofs in mathlib they are all much shorter.

[Lingwei Peng (彭灵伟)]

You are absolutely right. Using obtain (or Exists.elim) is more appropriate than Classical.choose. Thank you so much!