have h1 := hf m2
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
⊢ f m2 = m2
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 ^ 2
⊢ f m2 = m2