rw [←h] at h1
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (c * c)
⊢ 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
h1 : Odd (a * b)
⊢ Odd a ∧ Odd b