Eckmann—Hilton in Lean

eckmann_hilton.lean

import tactic.interactive

universe u

namespace eckmann_hilton
variables (X : Type u)

local notation a `<`m`>` b := @has_mul.mul X m a b

class is_unital [m : has_mul X] [e : has_one X] : Prop :=
(one_mul : ∀ x : X, (e.one <m> x) = x)
(mul_one : ∀ x : X, (x <m> e.one) = x)

attribute [simp] is_unital.one_mul
attribute [simp] is_unital.mul_one

variables {X} {m₁ : has_mul X} {e₁ : has_one X} {m₂ : has_mul X} {e₂ : has_one X}

@[extensionality] lemma mul.ext : m₁.mul = m₂.mul → m₁ = m₂ :=
begin tactic.unfreeze_local_instances, cases m₁, cases m₂, intro h, cases h, refl end

variables (h₁ : @is_unital X m₁ e₁) (h₂ : @is_unital X m₂ e₂)
variables (distrib : ∀ a b c d, ((a <m₂> b) <m₁> (c <m₂> d)) = ((a <m₁> c) <m₂> (b <m₁> d)))
include h₁ h₂ distrib

lemma one : (e₁.one = e₂.one) :=
by convert distrib e₂.one e₁.one e₁.one e₂.one; simp

set_option pp.all true
lemma mul : m₁ = m₂ :=
begin
  ext a b,
  convert distrib a e₁.one e₁.one b;
  { simp <|> { rw [one h₁ h₂ distrib]; simp } <|> { rw ←(one h₁ h₂ distrib); simp } }
end

lemma mul_comm : is_commutative _ m₂.mul :=
⟨λ a b, by convert distrib e₂.one a b e₂.one; try { rw mul h₁ h₂ distrib }; simp⟩

lemma mul_assoc : is_associative _ m₂.mul :=
⟨λ a b c, by convert distrib a b e₂.one c; try { rw mul h₁ h₂ distrib }; simp⟩

instance : comm_monoid X :=
{ mul_comm := (mul_comm h₁ h₂ distrib).comm,
  mul_assoc := (mul_assoc h₁ h₂ distrib).assoc,
  ..e₂,
  ..m₂,
  ..h₂ }

end eckmann_hilton