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

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
a b : ℕ+
r : ℕ
fab1 : f^[r] b = a
fab2 : f a = a
⊢ b = a
Tactic:
have h1 : ∀ s, f^[s] a = a := fun s ↦ Function.iterate_fixed fab2 s
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
a b : ℕ+
r : ℕ
fab1 : f^[r] b = a
fab2 : f a = a
h1 : ∀ (s : ℕ), f^[s] a = a
⊢ b = a

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
a b : ℕ+
r : ℕ
fab1 : f^[r] b = a
fab2 : f a = a
h1 : ∀ (s : ℕ), f^[s] a = a
⊢ b = a
Tactic:
have h2 := calc f^[r] b
    = a := fab1
  _ = f^[r] a := (h1 r).symm
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
a b : ℕ+
r : ℕ
fab1 : f^[r] b = a
fab2 : f a = a
h1 : ∀ (s : ℕ), f^[s] a = a
h2 : f^[r] b = f^[r] a
⊢ b = a

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
a b : ℕ+
r : ℕ
fab1 : f^[r] b = a
fab2 : f a = a
h1 : ∀ (s : ℕ), f^[s] a = a
h2 : f^[r] b = f^[r] a
⊢ b = a
Tactic:
exact Function.Injective.iterate (f_injective f hf) r h2
State after:
no goals