Theorem: IMOSL.IMO2011A4.final_solution_PNat (IMOSLLean4/IMO2011/A4/A4.lean)

State before:
f g : ℕ+ → ℕ+
⊢ (∀ (n : ℕ+), f^[↑(g n) + 1] n + (g^[↑(f n)] n + g (n + 1)) = f (n + 1) + 1) ↔ f = id ∧ g = fun x => 1
Tactic:
obtain ⟨f, rfl⟩ := PNat_exists_Nat_conj f
State after:
case intro
g : ℕ+ → ℕ+
f : ℕ → ℕ
⊢ (∀ (n : ℕ+),
      (fun n => (f n.natPred).succPNat)^[↑(g n) + 1] n + (g^[↑((fun n => (f n.natPred).succPNat) n)] n + g (n + 1)) =
        (fun n => (f n.natPred).succPNat) (n + 1) + 1) ↔
    (fun n => (f n.natPred).succPNat) = id ∧ g = fun x => 1

State before:
case intro
g : ℕ+ → ℕ+
f : ℕ → ℕ
⊢ (∀ (n : ℕ+),
      (fun n => (f n.natPred).succPNat)^[↑(g n) + 1] n + (g^[↑((fun n => (f n.natPred).succPNat) n)] n + g (n + 1)) =
        (fun n => (f n.natPred).succPNat) (n + 1) + 1) ↔
    (fun n => (f n.natPred).succPNat) = id ∧ g = fun x => 1
Tactic:
obtain ⟨g, rfl⟩ := PNat_exists_Nat_conj g
State after:
case intro.intro
f g : ℕ → ℕ
⊢ (∀ (n : ℕ+),
      (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n) + 1] n +
          ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n)] n +
            (fun n => (g n.natPred).succPNat) (n + 1)) =
        (fun n => (f n.natPred).succPNat) (n + 1) + 1) ↔
    (fun n => (f n.natPred).succPNat) = id ∧ (fun n => (g n.natPred).succPNat) = fun x => 1

State before:
case intro.intro
f g : ℕ → ℕ
⊢ (∀ (n : ℕ+),
      (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n) + 1] n +
          ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n)] n +
            (fun n => (g n.natPred).succPNat) (n + 1)) =
        (fun n => (f n.natPred).succPNat) (n + 1) + 1) ↔
    (fun n => (f n.natPred).succPNat) = id ∧ (fun n => (g n.natPred).succPNat) = fun x => 1
Tactic:
rw [eq_comm, PNat_eq_Nat_conj_iff, eq_comm (b := λ _ ↦ 1),
  PNat_eq_Nat_conj_iff, PNat_to_Nat_prop, Iff.comm]
State after:
case intro.intro
f g : ℕ → ℕ
⊢ ((f = fun n => (id n.succPNat).natPred) ∧ g = fun n => PNat.natPred 1) ↔
    ∀ (n : ℕ),
      (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat +
          ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat +
            (fun n => (g n.natPred).succPNat) (n.succPNat + 1)) =
        (fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1

State before:
case intro.intro
f g : ℕ → ℕ
⊢ ((f = fun n => (id n.succPNat).natPred) ∧ g = fun n => PNat.natPred 1) ↔
    ∀ (n : ℕ),
      (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat +
          ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat +
            (fun n => (g n.natPred).succPNat) (n.succPNat + 1)) =
        (fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1
Tactic:
refine final_solution.symm.trans <| forall_congr' (λ n ↦ ?_)
State after:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat +
        ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat +
          (fun n => (g n.natPred).succPNat) (n.succPNat + 1)) =
      (fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1

State before:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    (fun n => (f n.natPred).succPNat)^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat +
        ((fun n => (g n.natPred).succPNat)^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat +
          (fun n => (g n.natPred).succPNat) (n.succPNat + 1)) =
      (fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1
Tactic:
rw [← PNat.coe_inj, PNat_Nat_conj_iterate, PNat_Nat_conj_iterate]
State after:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    ↑((f^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat.natPred).succPNat +
          ((g^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat.natPred).succPNat +
            (fun n => (g n.natPred).succPNat) (n.succPNat + 1))) =
      ↑((fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1)

State before:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    ↑((f^[↑((fun n => (g n.natPred).succPNat) n.succPNat) + 1] n.succPNat.natPred).succPNat +
          ((g^[↑((fun n => (f n.natPred).succPNat) n.succPNat)] n.succPNat.natPred).succPNat +
            (fun n => (g n.natPred).succPNat) (n.succPNat + 1))) =
      ↑((fun n => (f n.natPred).succPNat) (n.succPNat + 1) + 1)
Tactic:
simp_rw [Nat.natPred_succPNat, PNat.add_coe, Nat.succPNat_coe, Nat.succ_add]
State after:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    (f^[(g n + 1).succ] n + (g^[(f n).succ] n + (g (n.succPNat + 1).natPred).succ).succ).succ =
      (f (n.succPNat + 1).natPred + ↑1).succ

State before:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 = f (n + 1) ↔
    (f^[(g n + 1).succ] n + (g^[(f n).succ] n + (g (n.succPNat + 1).natPred).succ).succ).succ =
      (f (n.succPNat + 1).natPred + ↑1).succ
Tactic:
rw [← add_left_inj 2]
State after:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 + 2 = f (n + 1) + 2 ↔
    (f^[(g n + 1).succ] n + (g^[(f n).succ] n + (g (n.succPNat + 1).natPred).succ).succ).succ =
      (f (n.succPNat + 1).natPred + ↑1).succ

State before:
case intro.intro
f g : ℕ → ℕ
n : ℕ
⊢ f^[g n + 2] n + (g^[f n + 1] n + g (n + 1)) + 1 + 2 = f (n + 1) + 2 ↔
    (f^[(g n + 1).succ] n + (g^[(f n).succ] n + (g (n.succPNat + 1).natPred).succ).succ).succ =
      (f (n.succPNat + 1).natPred + ↑1).succ
Tactic:
rfl
State after:
no goals