Theorem: Usa2019P1.lemma_2 (Compfiles/Usa2019P1.lean)

State before:
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
⊢ f m = m
Tactic:
let k := f m
State after:
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
⊢ f m = m

State before:
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
⊢ f m = m
Tactic:
have h1 : f k = m := by
  unfold_let k; dsimp at hm1 hm2; rw[hm1, hm2]
State after:
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
⊢ f m = m

State before:
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
⊢ f m = m
Tactic:
have h2 : f^[2] k = k := by dsimp; rw[h1]
State after:
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
⊢ f m = m

State before:
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
⊢ f m = m
Tactic:
have h3 : f^[f k] k * f^[2] k = k^2 := hf k
State after:
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

State before:
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
Tactic:
rw [h2] at h3
State after:
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

State before:
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
Tactic:
have h4 : f^[f k] k = k := by
  rwa [sq k, mul_left_inj] at h3
State after:
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
h4 : f^[↑(f k)] k = k
⊢ f m = m

State before:
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
h4 : f^[↑(f k)] k = k
⊢ f m = m
Tactic:
rw [h1] at h4
State after:
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
h4 : f^[↑m] k = k
⊢ f m = m

State before:
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
h4 : f^[↑m] k = k
h6 : ∀ (r : ℕ), f^[2 * r] k = k
⊢ f m = m
Tactic:
obtain ⟨m', hm'⟩ := hm3
State after:
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
h4 : f^[↑m] k = k
h6 : ∀ (r : ℕ), f^[2 * r] k = k
m' : ℕ
hm' : ↑m = 2 * m' + 1
⊢ f m = m

State before:
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
h4 : f^[↑m] k = k
h6 : ∀ (r : ℕ), f^[2 * r] k = k
m' : ℕ
hm' : ↑m = 2 * m' + 1
⊢ f m = m
Tactic:
rw [hm', add_comm, Function.iterate_add, Function.iterate_one] at h4
State after:
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' : ℕ
h4 : (f ∘ f^[2 * m']) k = k
hm' : ↑m = 2 * m' + 1
⊢ f m = m

State before:
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' : ℕ
h4 : (f ∘ f^[2 * m']) k = k
hm' : ↑m = 2 * m' + 1
⊢ f m = m
Tactic:
change f (f^[2 * m'] k) = k at h4
State after:
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

State before:
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
Tactic:
rw [h6 m'] at h4
State after:
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

State before:
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
Tactic:
rw [h1] at h4
State after:
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 : m = k
⊢ f m = m

State before:
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 : m = k
⊢ f m = m
Tactic:
exact h4.symm
State after:
no goals

State before:
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
⊢ f k = m
Tactic:
unfold_let k
State after:
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
⊢ f (f m) = m

State before:
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
⊢ f (f m) = m
Tactic:
dsimp at hm1 hm2
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm1 : f (f m) = f^[↑(f m)] m
hm2 : f^[↑(f m)] m = m
hm3 : Odd ↑m
k : ℕ+ := f m
⊢ f (f m) = m

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm1 : f (f m) = f^[↑(f m)] m
hm2 : f^[↑(f m)] m = m
hm3 : Odd ↑m
k : ℕ+ := f m
⊢ f (f m) = m
Tactic:
rw[hm1, hm2]
State after:
no goals

State before:
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
⊢ f^[2] k = k
Tactic:
dsimp
State after:
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
⊢ f (f k) = k

State before:
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
⊢ f (f k) = k
Tactic:
rw[h1]
State after:
no goals

State before:
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^[↑(f k)] k = k
Tactic:
rwa [sq k, mul_left_inj] at h3
State after:
no goals

State before:
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
h4 : f^[↑m] k = k
r : ℕ
⊢ f^[2 * r] k = k
Tactic:
induction' r with r ih
State after:
case zero
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
h4 : f^[↑m] k = k
⊢ f^[2 * 0] k = k

case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * (r + 1)] k = k

State before:
case zero
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
h4 : f^[↑m] k = k
⊢ f^[2 * 0] k = k
Tactic:
simp
State after:
no goals

State before:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * (r + 1)] k = k
Tactic:
rw [Nat.mul_succ]
State after:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r + 2] k = k

State before:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r + 2] k = k
Tactic:
rw [Function.iterate_add]
State after:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ (f^[2 * r] ∘ f^[2]) k = k

State before:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ (f^[2 * r] ∘ f^[2]) k = k
Tactic:
change f^[2 * r] (f^[2] k) = k
State after:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r] (f^[2] k) = k

State before:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r] (f^[2] k) = k
Tactic:
rw[h2]
State after:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r] k = k

State before:
case succ
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
h4 : f^[↑m] k = k
r : ℕ
ih : f^[2 * r] k = k
⊢ f^[2 * r] k = k
Tactic:
exact ih
State after:
no goals