Equation374794 not implies Equation2

@[equational_result]theorem Equation374794_not_implies_Equation2 : ∃ (G : Type) (_ : Magma G), Equation374794 G ∧ ¬Equation2 G := by  letI : Magma ℕ+ := { op := fun a b ↦ if a = b then 2^a.val else    if a = 1 then 3^b.val else    if a = 3 ^ (padicValNat 3 a) then Nat.toPNat' (padicValNat 3 a) else 1}  refine ⟨ℕ+, this, ⟨fun x y z ↦ ?_, fun x ↦ nomatch (x 1 2)⟩⟩  unfold Magma.op  simp only [this, ↓reduceIte, PNat.pow_coe, PNat.val_ofNat]  have t1 (y : ℕ+) : 2 ^ (y : ℕ) ≠ y := by    apply_fun PNat.val    simp [ne_of_gt, Nat.lt_pow_self]  have t3 (y : ℕ+) (n : ℕ) : (2 : ℕ+) ^ (y : ℕ) ≠ 3^n := by    apply_fun PNat.val    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]    intro nh    apply eq_of_prime_pow_eq at nh    · contradiction    · exact Nat.prime_two.prime    · exact Nat.prime_three.prime    · simp  have t2 (y : ℕ+) : (2 : ℕ+) ^ (y : ℕ) ≠ 1 := t3 y 0  have t4 (y : ℕ+) (n : ℕ) : (3 : ℕ+) ^ (y : ℕ) ≠ 2^n := by    apply_fun PNat.val    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]    intro nh    apply eq_of_prime_pow_eq at nh    · contradiction    · exact Nat.prime_three.prime    · exact Nat.prime_two.prime    · simp  have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩  have : Fact (Nat.Prime 3) := ⟨Nat.prime_three⟩  simp only [t1, ↓reduceIte, t2, t3, PNat.val_ofNat, pow_one]  by_cases hx : x = 1  · simp only [hx, ↓reduceIte, PNat.val_ofNat, PNat.ofNat_inj, OfNat.ofNat_ne_one, ne_eq,    Nat.succ_ne_self, not_false_eq_true, padicValNat_primes, pow_zero]    rw [if_neg]    split_ifs    · apply ne_of_lt      simp only [← PNat.coe_lt_coe, PNat.val_ofNat, PNat.pow_coe]      apply lt_self_pow₀ (by simp only [Nat.one_lt_ofNat])      apply one_lt_pow₀ (by simp only [Nat.one_lt_ofNat]) (by simp)    · trivial  simp only [Ne.symm hx, ↓reduceIte, PNat.pow_coe, PNat.val_ofNat, padicValNat.prime_pow,    PNat.coe_toPNat']  rw [if_neg, if_neg]  · simp [pow_eq_one_iff]  · split    · apply t4    · convert t4 _ 0