internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_1.intro
k : ℕ
⊢ id^[(fun x => 0) k + 2] k + ((fun x => 0)^[id k + 1] k + (fun x => 0) (k + 1)) + 1 = id (k + 1)
Tactic:
rw [iterate_id, iterate_succ_apply']
Proof state after:
case refine_1.intro
k : ℕ
⊢ id k + (0 + (fun x => 0) (k + 1)) + 1 = id (k + 1)
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_1.intro
k : ℕ
⊢ id k + (0 + (fun x => 0) (k + 1)) + 1 = id (k + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_2
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id ∧ g = fun x => 0
Tactic:
obtain rfl : f = id := by
  refine main_step (g := g) (λ k ↦ ?_)
  rw [← h, Nat.lt_succ_iff]
  exact Nat.le_add_right _ _
Proof state after:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
⊢ id = id ∧ g = fun x => 0
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
⊢ id = id ∧ g = fun x => 0
Tactic:
refine ⟨rfl, funext λ n ↦ ?_⟩
Proof state after:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
n : ℕ
⊢ g n = 0
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
n : ℕ
⊢ g n = 0
Tactic:
simp_rw [iterate_id, Function.id_def, Nat.succ_inj',
  add_right_eq_self, add_eq_zero_iff] at h
Proof state after:
case refine_2
g : ℕ → ℕ
n : ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g n = 0
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_2
g : ℕ → ℕ
n : ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g n = 0
Tactic:
rcases n with _ | n
Proof state after:
case refine_2.zero
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g 0 = 0

case refine_2.succ
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
n : ℕ
⊢ g (n + 1) = 0
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_2.zero
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g 0 = 0

case refine_2.succ
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
n : ℕ
⊢ g (n + 1) = 0
Tactic:
exacts [(h 0).1, (h n).2]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id
Tactic:
refine main_step (g := g) (λ k ↦ ?_)
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k < f (k + 1)
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k < f (k + 1)
Tactic:
rw [← h, Nat.lt_succ_iff]
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k ≤ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1))
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k ≤ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1))
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.PNat_exists_Nat_conj
Proof state before:
f : ℕ+ → ℕ+
n : ℕ+
⊢ f n = ((fun n => (f n.succPNat).natPred) n.natPred).succPNat
Tactic:
simp_rw [PNat.succPNat_natPred]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.PNat_eq_Nat_conj_iff
Proof state before:
f : ℕ+ → ℕ+
g : ℕ → ℕ
h : g = fun n => (f n.succPNat).natPred
n : ℕ+
⊢ f n = (g n.natPred).succPNat
Tactic:
rw [h, PNat.succPNat_natPred, PNat.succPNat_natPred]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.PNat_Nat_conj_iterate
Proof state before:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (fun n => (f n.natPred).succPNat)^[k + 1] m = (f^[k + 1] m.natPred).succPNat
Tactic:
rw [iterate_succ_apply', iterate_succ_apply',
  PNat_Nat_conj_iterate f m k]
Proof state after:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (f (f^[k] m.natPred).succPNat.natPred).succPNat = (f (f^[k] m.natPred)).succPNat
Theorem: IMOSL.IMO2011A4.PNat_Nat_conj_iterate
Proof state before:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (f (f^[k] m.natPred).succPNat.natPred).succPNat = (f (f^[k] m.natPred)).succPNat
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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]
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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 ↦ ?_)
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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]
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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]
Proof 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
Theorem: IMOSL.IMO2011A4.final_solution_PNat
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_eq
Proof state before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f^[4] (n + 1) = f^[4] n + 1
Tactic:
rw [f.iterate_succ_apply, h, ← h n, ← f.iterate_succ_apply']
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_eq
Proof state before:
f : ℕ → ℕ
h : good f
h0 : ∀ (n : ℕ), f^[4] (n + 1) = f^[4] n + 1
n : ℕ
h1 : f^[4] n = f^[4] 0 + n
⊢ f^[4] n.succ = f^[4] 0 + n.succ
Tactic:
rw [Nat.add_succ, h0, h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.good_injective
Proof state before:
f : ℕ → ℕ
h : good f
m n : ℕ
h0 : f^[4] m = f^[4] n
⊢ m = n
Tactic:
rwa [iter_four_eq h, iter_four_eq h n, add_right_inj] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
⊢ (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
Tactic:
intro x h0
Proof state after:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ x ∈ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ x ∈ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
Tactic:
rw [mem_union, mem_image, mem_insert, mem_singleton, or_assoc]
Proof state after:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ x = 0 ∨ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ x = 0 ∨ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Tactic:
refine x.eq_zero_or_eq_succ_pred.imp id λ h1 ↦ ?_
Proof state after:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : x = x.pred.succ
⊢ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : x = x.pred.succ
⊢ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Tactic:
generalize x.pred = c at h1
Proof state after:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
c : ℕ
h1 : x = c.succ
⊢ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
c : ℕ
h1 : x = c.succ
⊢ x = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = x
Tactic:
subst h1
Proof state after:
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ c.succ = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = c.succ
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ c.succ = (f 0).succ ∨ ∃ a ∈ (finChainFnOfgood h).rangeCompl, a.succ = c.succ
Tactic:
refine (em <| c ∈ Set.range f).imp (λ h1 ↦ ?_) (λ h1 ↦ ⟨c, ?_, rfl⟩)
Proof state after:
case refine_1
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : c ∈ Set.range f
⊢ c.succ = (f 0).succ

case refine_2
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : c ∉ Set.range f
⊢ c ∈ (finChainFnOfgood h).rangeCompl
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_1
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : c ∈ Set.range f
⊢ c.succ = (f 0).succ
Tactic:
rcases h1 with ⟨d, rfl⟩
Proof state after:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ (f d).succ = (f 0).succ
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ (f d).succ = (f 0).succ
Tactic:
refine d.eq_zero_or_eq_succ_pred.elim (λ h2 ↦ h2 ▸ rfl) (λ h2 ↦ ?_)
Proof state after:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h2 : d = d.pred.succ
⊢ (f d).succ = (f 0).succ
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h2 : d = d.pred.succ
⊢ (f d).succ = (f 0).succ
Tactic:
rw [(finChainFnOfgood h).mem_iterRangeCompl_iff] at h0
Proof state after:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∉ Set.range f^[3]
h2 : d = d.pred.succ
⊢ (f d).succ = (f 0).succ
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∉ Set.range f^[3]
h2 : d = d.pred.succ
⊢ (f d).succ = (f 0).succ
Tactic:
refine absurd ⟨d.pred, ?_⟩ h0
Proof state after:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∉ Set.range f^[3]
h2 : d = d.pred.succ
⊢ f^[3] d.pred = (f d).succ
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_1.intro
f : ℕ → ℕ
h : good f
d : ℕ
h0 : (f d).succ ∉ Set.range f^[3]
h2 : d = d.pred.succ
⊢ f^[3] d.pred = (f d).succ
Tactic:
rw [h, ← d.pred.succ_eq_add_one, ← h2]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iterRangeCompl_three_subset
Proof state before:
case refine_2
f : ℕ → ℕ
h : good f
c : ℕ
h0 : c.succ ∈ (finChainFnOfgood h).iterRangeCompl 3
h1 : c ∉ Set.range f
⊢ c ∈ (finChainFnOfgood h).rangeCompl
Tactic:
rwa [(finChainFnOfgood h).mem_rangeCompl_iff]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
f : ℕ → ℕ
h : good f
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
have h0 := (card_le_card <| iterRangeCompl_three_subset h).trans <|
  (card_union_le _ _).trans <| Nat.add_le_add
    (card_pair (f 0).succ_ne_zero.symm).le card_image_le
Proof state after:
f : ℕ → ℕ
h : good f
h0 : ((finChainFnOfgood h).iterRangeCompl 3).card ≤ 2 + (finChainFnOfgood h).rangeCompl.card
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
f : ℕ → ℕ
h : good f
h0 : ((finChainFnOfgood h).iterRangeCompl 3).card ≤ 2 + (finChainFnOfgood h).rangeCompl.card
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
rw [(finChainFnOfgood h).iterRangeCompl_card, Nat.succ_mul,
  Nat.add_le_add_iff_right, mul_comm, ← Nat.le_div_iff_mul_le (Nat.succ_pos 1)] at h0
Proof state after:
f : ℕ → ℕ
h : good f
h0 : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
f : ℕ → ℕ
h : good f
h0 : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
refine h0.eq_or_lt.elim card_eq_one.mp (λ h0 ↦ ?_)
Proof state after:
f : ℕ → ℕ
h : good f
h0✝ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0 : (finChainFnOfgood h).rangeCompl.card < 2 / Nat.succ 1
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
f : ℕ → ℕ
h : good f
h0✝ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0 : (finChainFnOfgood h).rangeCompl.card < 2 / Nat.succ 1
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
rw [Nat.lt_one_iff, card_eq_zero, ← (finChainFnOfgood h).surjective_iff] at h0
Proof state after:
f : ℕ → ℕ
h : good f
h0✝ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0 : Function.Surjective f
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
f : ℕ → ℕ
h : good f
h0✝ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0 : Function.Surjective f
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
obtain ⟨a, h0⟩ := h0.iterate 3 0
Proof state after:
case intro
f : ℕ → ℕ
h : good f
h0✝¹ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0✝ : Function.Surjective f
a : ℕ
h0 : f^[3] a = 0
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Theorem: IMOSL.IMO2013A5.exists_rangeCompl_eq_singleton
Proof state before:
case intro
f : ℕ → ℕ
h : good f
h0✝¹ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0✝ : Function.Surjective f
a : ℕ
h0 : f^[3] a = 0
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}
Tactic:
exact absurd ((h a).symm.trans h0) (f a.succ).succ_ne_zero
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
f : ℕ → ℕ
h : good f
⊢ f^[4] 0 = 4
Tactic:
obtain ⟨a, h0⟩ := exists_rangeCompl_eq_singleton h
Proof state after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f^[4] 0 = 4
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f^[4] 0 = 4
Tactic:
suffices (finChainFnOfgood h).iterRangeCompl 4 = range (f^[4] 0) by
  rw [← card_range (f^[4] 0), ← this,
    (finChainFnOfgood h).iterRangeCompl_card, h0, card_singleton]
Proof state after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ (finChainFnOfgood h).iterRangeCompl 4 = range (f^[4] 0)
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ (finChainFnOfgood h).iterRangeCompl 4 = range (f^[4] 0)
Tactic:
ext n
Proof state after:
case intro.a
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
⊢ n ∈ (finChainFnOfgood h).iterRangeCompl 4 ↔ n ∈ range (f^[4] 0)
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro.a
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
⊢ n ∈ (finChainFnOfgood h).iterRangeCompl 4 ↔ n ∈ range (f^[4] 0)
Tactic:
rw [(finChainFnOfgood h).mem_iterRangeCompl_iff, mem_range, not_iff_comm, not_lt]
Proof state after:
case intro.a
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
⊢ f^[4] 0 ≤ n ↔ n ∈ Set.range f^[4]
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro.a
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
⊢ f^[4] 0 ≤ n ↔ n ∈ Set.range f^[4]
Tactic:
refine ⟨λ h1 ↦ ⟨n - f^[4] 0, ?_⟩, λ ⟨k, h1⟩ ↦ ?_⟩
Proof state after:
case intro.a.refine_1
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
h1 : f^[4] 0 ≤ n
⊢ f^[4] (n - f^[4] 0) = n

case intro.a.refine_2
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
x✝ : n ∈ Set.range f^[4]
k : ℕ
h1 : f^[4] k = n
⊢ f^[4] 0 ≤ n
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
this : (finChainFnOfgood h).iterRangeCompl 4 = range (f^[4] 0)
⊢ f^[4] 0 = 4
Tactic:
rw [← card_range (f^[4] 0), ← this,
  (finChainFnOfgood h).iterRangeCompl_card, h0, card_singleton]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro.a.refine_1
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
h1 : f^[4] 0 ≤ n
⊢ f^[4] (n - f^[4] 0) = n
Tactic:
rw [iter_four_eq h, Nat.add_sub_of_le h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro.a.refine_2
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
x✝ : n ∈ Set.range f^[4]
k : ℕ
h1 : f^[4] k = n
⊢ f^[4] 0 ≤ n
Tactic:
rw [← h1, iter_four_eq h k]
Proof state after:
case intro.a.refine_2
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
x✝ : n ∈ Set.range f^[4]
k : ℕ
h1 : f^[4] k = n
⊢ f^[4] 0 ≤ f^[4] 0 + k
Theorem: IMOSL.IMO2013A5.iter_four_zero_eq_four
Proof state before:
case intro.a.refine_2
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
n : ℕ
x✝ : n ∈ Set.range f^[4]
k : ℕ
h1 : f^[4] k = n
⊢ f^[4] 0 ≤ f^[4] 0 + k
Tactic:
exact Nat.le_add_right _ k
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.iter_four_eq_add_four
Proof state before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f^[4] n = n + 4
Tactic:
rw [iter_four_eq h, add_comm, iter_four_zero_eq_four h]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.map_add_four
Proof state before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f (n + 4) = f n + 4
Tactic:
have h1 := iter_four_eq_add_four h
Proof state after:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (n + 4) = f n + 4
Theorem: IMOSL.IMO2013A5.map_add_four
Proof state before:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (n + 4) = f n + 4
Tactic:
rw [← h1, ← h1]
Proof state after:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (f^[4] n) = f^[4] (f n)
Theorem: IMOSL.IMO2013A5.map_add_four
Proof state before:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (f^[4] n) = f^[4] (f n)
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
f : ℕ → ℕ
h : good f
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rcases exists_rangeCompl_eq_singleton h with ⟨a, h0⟩
Proof state after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f = Nat.succ ∨ f = answer2