obtain ⟨b, hb⟩ := b
case mk
b c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
h : ⟨a, ha⟩ * b = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑b
case mk.mk
c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
h : ⟨a, ha⟩ * ⟨b, hb⟩ = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩