case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n
x m n : ℕ
⊢ x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
constructor
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
intro h
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h :
  ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
      ↑({ val := y, property := hy }, { val := z, property := hz }).snd ∣
    m * n
⊢ ∃ y_1 z_1,
    y_1 ∣ m ∧
      z_1 ∣ n ∧
        y_1 * z_1 =
          ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
            ↑({ val := y, property := hy }, { val := z, property := hz }).snd
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
obtain ⟨⟨⟨y, hy⟩, ⟨z, hz⟩⟩, rfl⟩ := prod_dvd_and_dvd_of_dvd_prod h
no goals
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h :
  ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
      ↑({ val := y, property := hy }, { val := z, property := hz }).snd ∣
    m * n
⊢ ∃ y_1 z_1,
    y_1 ∣ m ∧
      z_1 ∣ n ∧
        y_1 * z_1 =
          ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
            ↑({ val := y, property := hy }, { val := z, property := hz }).snd
exact ⟨y, z, hy, hz, rfl⟩
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n
case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n
rintro ⟨y, z, hy, hz, rfl⟩
no goals
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n
exact mul_dvd_mul hy hz