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

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
⊢ Function.Injective f
Tactic:
intro p q hpq
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ p = q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ p = q
Tactic:
have h1 : f^[2] p = f^[2] q := by
  apply_fun f at hpq
  exact hpq
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ p = q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ p = q
Tactic:
have h2 : ∀ n : ℕ+, f^[n] p = f^[n] q := by
  intro n
  obtain ⟨n, hn⟩ := n
  cases' n with n <;> aesop
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ p = q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ p = q
Tactic:
have h3 : f^[f p] p = f^[f q] q := by rw[hpq]; exact h2 (f q)
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
⊢ p = q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
⊢ p = q
Tactic:
have h4 :=
  calc p^2
    = f^[f p] p * f^[2] p := (hf p).symm
  _ = f^[f q] q * f^[2] q := by rw[h3, h1]
  _ = q^2 := hf q
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
h4 : p ^ 2 = q ^ 2
⊢ p = q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
h4 : p ^ 2 = q ^ 2
⊢ p = q
Tactic:
obtain ⟨p, hp⟩ := p
State after:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
q : ℕ+
p : ℕ
hp : 0 < p
hpq : f ⟨p, hp⟩ = f q
h1 : f^[2] ⟨p, hp⟩ = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] q
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f q)] q
h4 : ⟨p, hp⟩ ^ 2 = q ^ 2
⊢ ⟨p, hp⟩ = q

State before:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
q : ℕ+
p : ℕ
hp : 0 < p
hpq : f ⟨p, hp⟩ = f q
h1 : f^[2] ⟨p, hp⟩ = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] q
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f q)] q
h4 : ⟨p, hp⟩ ^ 2 = q ^ 2
⊢ ⟨p, hp⟩ = q
Tactic:
obtain ⟨q, hq⟩ := q
State after:
case mk.mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ ⟨p, hp⟩ = ⟨q, hq⟩

State before:
case mk.mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ ⟨p, hp⟩ = ⟨q, hq⟩
Tactic:
congr
State after:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ p = q

State before:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ p = q
Tactic:
apply_fun (fun x ↦ x.val) at h4
State after:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ↑(⟨p, hp⟩ ^ 2) = ↑(⟨q, hq⟩ ^ 2)
⊢ p = q

State before:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ↑(⟨p, hp⟩ ^ 2) = ↑(⟨q, hq⟩ ^ 2)
⊢ p = q
Tactic:
rw [PNat.pow_coe, PNat.pow_coe, PNat.mk_coe, PNat.mk_coe] at h4
State after:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : p ^ 2 = q ^ 2
⊢ p = q

State before:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : p ^ 2 = q ^ 2
⊢ p = q
Tactic:
rw [pow_left_inj (le_of_lt hp) (le_of_lt hq) two_ne_zero] at h4
State after:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : p = q
⊢ p = q

State before:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : p = q
⊢ p = q
Tactic:
exact h4
State after:
no goals

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ f^[2] p = f^[2] q
Tactic:
apply_fun f at hpq
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f (f p) = f (f q)
⊢ f^[2] p = f^[2] q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f (f p) = f (f q)
⊢ f^[2] p = f^[2] q
Tactic:
exact hpq
State after:
no goals

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
Tactic:
intro n
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
n : ℕ+
⊢ f^[↑n] p = f^[↑n] q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
n : ℕ+
⊢ f^[↑n] p = f^[↑n] q
Tactic:
obtain ⟨n, hn⟩ := n
State after:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
n : ℕ
hn : 0 < n
⊢ f^[↑⟨n, hn⟩] p = f^[↑⟨n, hn⟩] q

State before:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
n : ℕ
hn : 0 < n
⊢ f^[↑⟨n, hn⟩] p = f^[↑⟨n, hn⟩] q
Tactic:
cases' n with n <;> aesop
State after:
no goals

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ f^[↑(f p)] p = f^[↑(f q)] q
Tactic:
rw[hpq]
State after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ f^[↑(f q)] p = f^[↑(f q)] q

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ f^[↑(f q)] p = f^[↑(f q)] q
Tactic:
exact h2 (f q)
State after:
no goals

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
⊢ f^[↑(f p)] p * f^[2] p = f^[↑(f q)] q * f^[2] q
Tactic:
rw[h3, h1]
State after:
no goals