[GOAL]
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
x y : G₁ × G₂
⊢ x ∣ y ↔ x.fst ∣ y.fst ∧ x.snd ∣ y.snd
[PROOFSTEP]
cases x
[GOAL]
case mk
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).fst ∣ y.fst ∧ (fst✝, snd✝).snd ∣ y.snd
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).fst ∣ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd ∣ (fst✝, snd✝).snd
[PROOFSTEP]
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq, exists_and_left, exists_and_right, and_self, true_and]
