rw [h2] at h3
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm1 : f^[2] m = f^[↑(f m)] m
hm2 : f^[↑(f m)] m = m
hm3 : Odd ↑m
k : ℕ+ := f m
h1 : f k = m
h2 : f^[2] k = k
h3 : f^[↑(f k)] k * f^[2] k = k ^ 2
⊢ f m = m
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm1 : f^[2] m = f^[↑(f m)] m
hm2 : f^[↑(f m)] m = m
hm3 : Odd ↑m
k : ℕ+ := f m
h1 : f k = m
h2 : f^[2] k = k
h3 : f^[↑(f k)] k * k = k ^ 2
⊢ f m = m