Lemmas about the divisibility relation in product (semi)groups

theorem prod_dvd_iff {G₁ : Type u_1} {G₂ : Type u_2} [Semigroup G₁] [Semigroup G₂] {x : G₁ × G₂} {y : G₁ × G₂} : x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

@[simp]

theorem Prod.mk_dvd_mk {G₁ : Type u_1} {G₂ : Type u_2} [Semigroup G₁] [Semigroup G₂] {x₁ : G₁} {y₁ : G₁} {x₂ : G₂} {y₂ : G₂} : (x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂