dsimp at h
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ↑(⟨a, ha⟩ * ⟨b, hb⟩) = ↑(⟨c, hc✝⟩ * ⟨c, hc✝⟩)
⊢ Odd a ∧ Odd b
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
⊢ Odd a ∧ Odd b