rw [←h1] at h10
case inl
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 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False
case inl
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 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : f^[↑(f m2)] m2 * f (f m2) < f^[↑(f m2)] m2 * f (f m2)
⊢ False