Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2 (IMOSLLean4/IMO2013/A5/A5.lean)

State before:
f : ℕ → ℕ
h : good f
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rcases exists_rangeCompl_eq_singleton h with ⟨a, h0⟩
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h1 := iterRangeCompl_three_subset h
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
h1 : (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
h1 : (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2
Tactic:
let C := finChainFnOfgood h
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
h1 : (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
C : FinChainFn f := finChainFnOfgood h
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
h1 : (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
C : FinChainFn f := finChainFnOfgood h
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [C.iterRangeCompl_succ, C.iterRangeCompl_succ, C.iterRangeCompl_one] at h1
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  C.exactIterRange 2 ∪ (C.exactIterRange 1 ∪ C.rangeCompl) ⊆
    {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  C.exactIterRange 2 ∪ (C.exactIterRange 1 ∪ C.rangeCompl) ⊆
    {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2
Tactic:
unfold FinChainFn.exactIterRange at h1
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  image f^[2] C.rangeCompl ∪ (image f^[1] C.rangeCompl ∪ C.rangeCompl) ⊆
    {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  image f^[2] C.rangeCompl ∪ (image f^[1] C.rangeCompl ∪ C.rangeCompl) ⊆
    {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h0, image_singleton, image_singleton, image_singleton, union_subset_iff,
  union_subset_iff, f.iterate_succ_apply, f.iterate_one] at h1
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 : {f (f a)} ⊆ {0, (f 0).succ} ∪ {a.succ} ∧ {f a} ⊆ {0, (f 0).succ} ∪ {a.succ} ∧ {a} ⊆ {0, (f 0).succ} ∪ {a.succ}
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 : {f (f a)} ⊆ {0, (f 0).succ} ∪ {a.succ} ∧ {f a} ⊆ {0, (f 0).succ} ∪ {a.succ} ∧ {a} ⊆ {0, (f 0).succ} ∪ {a.succ}
⊢ f = Nat.succ ∨ f = answer2
Tactic:
iterate 3 rw [singleton_subset_iff, mem_union,
  mem_singleton, mem_insert, mem_singleton] at h1
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h2 : ∀ n, f (f n) ≠ n := λ n h2 ↦ by
  apply absurd (iter_four_eq_add_four h n)
  change f (f (f (f n))) ≠ n + 4
  rw [h2, h2, self_ne_add_right]
  exact Nat.succ_ne_zero 3
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
h2 : ∀ (n : ℕ), f (f n) ≠ n
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
h2 : ∀ (n : ℕ), f (f n) ≠ n
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h3 : ∀ n, f n ≠ n := λ n h3 ↦ h2 n <| Function.iterate_fixed h3 2
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rcases h1 with ⟨h1, h4, (rfl | rfl) | h5⟩
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : (f (f 0) = 0 ∨ f (f 0) = (f 0).succ) ∨ f (f 0) = Nat.succ 0
h4 : (f 0 = 0 ∨ f 0 = (f 0).succ) ∨ f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2

case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : (f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ) ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : (f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ) ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2

case intro.intro.intro.inr
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h1 : (f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ
h4 : (f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ
h5 : a = a.succ
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ {a} ⊆ {0, (f 0).succ} ∪ {a.succ}
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [singleton_subset_iff, mem_union,
mem_singleton, mem_insert, mem_singleton] at h1
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
⊢ f = Nat.succ ∨ f = answer2

State before:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ False
Tactic:
apply absurd (iter_four_eq_add_four h n)
State after:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ ¬f^[4] n = n + 4

State before:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ ¬f^[4] n = n + 4
Tactic:
change f (f (f (f n))) ≠ n + 4
State after:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ f (f (f (f n))) ≠ n + 4

State before:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ f (f (f (f n))) ≠ n + 4
Tactic:
rw [h2, h2, self_ne_add_right]
State after:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ 4 ≠ 0

State before:
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h1 :
  ((f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ) ∧
    ((f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ) ∧ ((a = 0 ∨ a = (f 0).succ) ∨ a = a.succ)
n : ℕ
h2 : f (f n) = n
⊢ 4 ≠ 0
Tactic:
exact Nat.succ_ne_zero 3
State after:
no goals

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : (f (f 0) = 0 ∨ f (f 0) = (f 0).succ) ∨ f (f 0) = Nat.succ 0
h4 : (f 0 = 0 ∨ f 0 = (f 0).succ) ∨ f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [or_iff_right (h3 0), or_iff_right (f 0).succ_ne_self.symm] at h4
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : (f (f 0) = 0 ∨ f (f 0) = (f 0).succ) ∨ f (f 0) = Nat.succ 0
h4 : f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : (f (f 0) = 0 ∨ f (f 0) = (f 0).succ) ∨ f (f 0) = Nat.succ 0
h4 : f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [or_iff_right (h2 0), h4, or_iff_left (h3 1)] at h1
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h5 : f (f (f 0)) = f 1 + 1 := h 0
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h6 : f (f (f (f 0))) = 4 := iter_four_zero_eq_four h
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
h6 : f (f (f (f 0))) = 4
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
h6 : f (f (f (f 0))) = 4
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h5, h1] at h6
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (f (f 0)) = f 1 + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, h1] at h5
State after:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ ∨ f = answer2
Tactic:
left
State after:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ

State before:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ f = Nat.succ
Tactic:
refine funext (add_four_induction h4 h1 h5 h6 ?_)
State after:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ ∀ (n : ℕ), f n = n.succ → f (n + 4) = (n + 4).succ

State before:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
⊢ ∀ (n : ℕ), f n = n.succ → f (n + 4) = (n + 4).succ
Tactic:
intro n h7
State after:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
n : ℕ
h7 : f n = n.succ
⊢ f (n + 4) = (n + 4).succ

State before:
case intro.intro.intro.inl.inl.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {0}
h1 : f (Nat.succ 0) = (Nat.succ 0).succ
h4 : f 0 = Nat.succ 0
h5 : f (Nat.succ 0).succ = (Nat.succ 0).succ + 1
h6 : f ((Nat.succ 0).succ + 1) = 4
n : ℕ
h7 : f n = n.succ
⊢ f (n + 4) = (n + 4).succ
Tactic:
rw [map_add_four h, h7]
State after:
no goals

State before:
case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : (f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ) ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : (f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ) ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [or_iff_left (h3 _)] at h4
State after:
case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : (f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ) ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : (f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ) ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [or_iff_left (h2 _)] at h1
State after:
case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0 ∨ f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rcases h4 with h4 | h4
State after:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2

case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, or_iff_left (h3 _)] at h1
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1 := h (f 0).succ
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
⊢ f = Nat.succ ∨ f = answer2
Tactic:
have h6 : f (f (f (f (f 0 + 1)))) = f 0 + 5 := iter_four_eq_add_four h _
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f (f (f (f (f 0 + 1)))) = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f (f (f (f (f 0 + 1)))) = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h5, h1, zero_add] at h6
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, h1, zero_add] at h5
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f 0 = 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f 0 = 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h5] at h1 h4 h6
State after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
right
State after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = answer2

State before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = answer2
Tactic:
refine funext (add_four_induction h5 h6 h4 h1 ?_)
State after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ ∀ (n : ℕ), f n = answer2 n → f (n + 4) = answer2 (n + 4)

State before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ ∀ (n : ℕ), f n = answer2 n → f (n + 4) = answer2 (n + 4)
Tactic:
intro n h7
State after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
n : ℕ
h7 : f n = answer2 n
⊢ f (n + 4) = answer2 (n + 4)

State before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
n : ℕ
h7 : f n = answer2 n
⊢ f (n + 4) = answer2 (n + 4)
Tactic:
rw [map_add_four h, h7, answer2]
State after:
no goals

State before:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, or_iff_right (h3 0)] at h1
State after:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f 0 = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2

State before:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f 0 = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
exact absurd h1 (Nat.lt_succ.mpr (f 0).le_succ).ne
State after:
no goals

State before:
case intro.intro.intro.inr
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h1 : (f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ
h4 : (f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ
h5 : a = a.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
exact absurd h5 a.lt_succ_self.ne
State after:
no goals