Theorem: Imo2009P5.final_solution_pnat (Compfiles/Imo2009P5.lean)

State before:
f : ℕ+ → ℕ+
⊢ ((∀ (x y : ℕ+), f (y + f x - 1) < f y + x) ∧
      (∀ (x y : ℕ+), x < f y + f (y + f x - 1)) ∧ ∀ (x y : ℕ+), f y < f (y + f x - 1) + x) ↔
    f = fun x => x
Tactic:
obtain ⟨g, rfl⟩ : ∃ g : ℕ → ℕ, f = λ x ↦ (g x.natPred).succPNat :=
  ⟨λ x ↦ (f x.succPNat).natPred,
    funext (λ x ↦ by rw [PNat.succPNat_natPred, PNat.succPNat_natPred])⟩
State after:
case intro
g : ℕ → ℕ
⊢ ((∀ (x y : ℕ+),
        (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) <
          (fun x => (g x.natPred).succPNat) y + x) ∧
      (∀ (x y : ℕ+),
          x <
            (fun x => (g x.natPred).succPNat) y +
              (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1)) ∧
        ∀ (x y : ℕ+),
          (fun x => (g x.natPred).succPNat) y <
            (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) + x) ↔
    (fun x => (g x.natPred).succPNat) = fun x => x

State before:
case intro
g : ℕ → ℕ
⊢ ((∀ (x y : ℕ+),
        (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) <
          (fun x => (g x.natPred).succPNat) y + x) ∧
      (∀ (x y : ℕ+),
          x <
            (fun x => (g x.natPred).succPNat) y +
              (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1)) ∧
        ∀ (x y : ℕ+),
          (fun x => (g x.natPred).succPNat) y <
            (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) + x) ↔
    (fun x => (g x.natPred).succPNat) = fun x => x
Tactic:
simp_rw [pnat_to_nat_prop2, Function.funext_iff, pnat_to_nat_prop, Nat.natPred_succPNat,
         Nat.succPNat_inj, ← Function.funext_iff, succ_pnat_add_succ_pnat, pnat_add_sub_cancel,
         Nat.natPred_succPNat, PNat.lt_add_one_iff, Nat.succPNat_le_succPNat]
State after:
case intro
g : ℕ → ℕ
⊢ ((∀ (m n : ℕ), g (n + g m) ≤ g n + m) ∧ (∀ (m n : ℕ), m ≤ g n + g (n + g m)) ∧ ∀ (m n : ℕ), g n ≤ g (n + g m) + m) ↔
    (fun a => g a) = fun a => a

State before:
case intro
g : ℕ → ℕ
⊢ ((∀ (m n : ℕ), g (n + g m) ≤ g n + m) ∧ (∀ (m n : ℕ), m ≤ g n + g (n + g m)) ∧ ∀ (m n : ℕ), g n ≤ g (n + g m) + m) ↔
    (fun a => g a) = fun a => a
Tactic:
exact final_solution_nat g
State after:
no goals

State before:
f : ℕ+ → ℕ+
x : ℕ+
⊢ f x = ((fun x => (f x.succPNat).natPred) x.natPred).succPNat
Tactic:
rw [PNat.succPNat_natPred, PNat.succPNat_natPred]
State after:
no goals