Finite Equation374794 implies Equation2

@[equational_result]theorem Finite.Equation374794_implies_Equation2 (G : Type*) [Magma G] [Finite G] (h : Equation374794 G) :    Equation2 G := by  have : ∀ (y z u : G), (y ◇ y) ◇ z = (y ◇ y) ◇ u := by    intro y    let f (x : G) := ((y ◇ y) ◇ y) ◇ x    let g (x : G) := x ◇ ((y ◇ y) ◇ y)    have : Function.RightInverse f g := fun x ↦ by simp [f, g, ← h]    refine fun z u ↦ this.injective ?_    obtain ⟨finv, hf⟩ := (Finite.surjective_of_injective this.injective).hasRightInverse    let fy := finv ((y ◇ y) ◇ y)    replace hf : ((y ◇ y) ◇ y) ◇ fy = (y ◇ y) ◇ y := hf _    have := h fy y    simp only [hf] at this    simp [f, ← this]  intro x u  have y := x  have z := x  rw [h x y z, this y y (y ◇ y), this (y ◇ y) x u, ← this y y (y ◇ y), ← h]