. intro h
  exact ⟨Nat.eq_one_of_mul_eq_one_right h, Nat.eq_one_of_mul_eq_one_left h⟩
case mp
a b : Nat
⊢ a * b = 1 → a = 1 ∧ b = 1

case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1