import equational_theories.Equations

class NaturalCentralGroupoid (S : Type _) where
  op : (S × S) → (S × S) → (S × S)
  op_eq : ∀ (x1 x2 y1 y2 : S), op (x1, x2) (y1, y2) = (x2, y1)

instance {S : Type*} [NaturalCentralGroupoid S] : Magma (S × S) where
  op := NaturalCentralGroupoid.op

lemma NaturalCentralGroupoid_as_Magma {S : Type*} [NaturalCentralGroupoid S] (x1 x2 y1 y2 : S) : (x1, x2) ◇ (y1, y2) = (x2, y1) := by
  exact NaturalCentralGroupoid.op_eq x1 x2 y1 y2

theorem NaturalCentralGroupoid_implies_Equation26302 (S : Type*) [NaturalCentralGroupoid S]  : Equation26302 (S × S) := by
  intro x y z w
  let (x1, x2) := x
  let (y1, y2) := y
  let (z1, z2) := z
  let (w1, w2) := w
  calc
    (x1, x2)
    _= (y2, x1) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma y2 x1 x2 w1]
    _= ((y1, y2) ◇ (x1, w1)) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma y1 y2 x1 w1]
    _= ((y1, y2) ◇ ((z2,x1) ◇ (w1, w2))) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma z2 x1 w1 w2]
    _= ((y1, y2) ◇ (((z1, z2) ◇ (x1, x2)) ◇ (w1, w2))) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma z1 z2 x1 x2]
    _= ((y1, y2) ◇ (((z1, z2) ◇ (x1, x2)) ◇ (w1, w2))) ◇ ((x1, x2) ◇ (w1, w2)) := by rw [← NaturalCentralGroupoid_as_Magma x1 x2 w1 w2]