rw [h6 m'] at h4
case intro
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
k : ℕ+ := f m
h1 : f k = m
h2 : f^[2] k = k
h3 : f^[↑(f k)] k * k = k ^ 2
h6 : ∀ (r : ℕ), f^[2 * r] k = k
m' : ℕ
hm' : ↑m = 2 * m' + 1
h4 : f (f^[2 * m'] k) = k
⊢ f m = m
case intro
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
k : ℕ+ := f m
h1 : f k = m
h2 : f^[2] k = k
h3 : f^[↑(f k)] k * k = k ^ 2
h6 : ∀ (r : ℕ), f^[2 * r] k = k
m' : ℕ
hm' : ↑m = 2 * m' + 1
h4 : f k = k
⊢ f m = m