internlm/Lean-Github huggingface dataset:
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.f_injective
Proof 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]
Proof 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
Theorem: Usa2019P1.f_injective
Proof 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)
Proof state after:
no goals
Theorem: Usa2019P1.f_injective
Proof 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]
Proof state after:
no goals
Theorem: Usa2019P1.lemma_1
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_1
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_1
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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]
Proof 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
Theorem: Usa2019P1.lemma_2
Proof 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
Proof state after:
no goals
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
a b c : ℕ+
h : a * b = c * c
hc : Odd ↑c
⊢ Odd ↑a ∧ Odd ↑b
Tactic:
obtain ⟨a, ha⟩ := a
Proof state after:
case mk
b c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
h : ⟨a, ha⟩ * b = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk
b c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
h : ⟨a, ha⟩ * b = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑b
Tactic:
obtain ⟨b, hb⟩ := b
Proof state after:
case mk.mk
c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
h : ⟨a, ha⟩ * ⟨b, hb⟩ = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk
c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
h : ⟨a, ha⟩ * ⟨b, hb⟩ = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Tactic:
obtain ⟨c, hc⟩ := c
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Tactic:
simp only [PNat.mk_coe]
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Tactic:
rw [PNat.mk_coe] at hc
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Tactic:
apply_fun (fun x ↦ x.val) at h
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ↑(⟨a, ha⟩ * ⟨b, hb⟩) = ↑(⟨c, hc✝⟩ * ⟨c, hc✝⟩)
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ↑(⟨a, ha⟩ * ⟨b, hb⟩) = ↑(⟨c, hc✝⟩ * ⟨c, hc✝⟩)
⊢ Odd a ∧ Odd b
Tactic:
dsimp at h
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
⊢ Odd a ∧ Odd b
Tactic:
have h1 : Odd (c * c) := Odd.mul hc hc
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (c * c)
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (c * c)
⊢ Odd a ∧ Odd b
Tactic:
rw [←h] at h1
Proof state after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (a * b)
⊢ Odd a ∧ Odd b
Theorem: Usa2019P1.pnat_odd_mul
Proof state before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (a * b)
⊢ Odd a ∧ Odd b
Tactic:
exact Nat.odd_mul.mp h1
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm3 : Odd ↑m
⊢ f m = m
Tactic:
induction' m using PNat.strongInductionOn with m2 ih
Proof state after:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
⊢ f m2 = m2
Tactic:
have h1 := hf m2
Proof state after:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 ^ 2
⊢ f m2 = m2