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

State before:
f : ℕ → ℕ
h : good f
⊢ f^[4] 0 = 4
Tactic:
obtain ⟨a, h0⟩ := exists_rangeCompl_eq_singleton h
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ f^[4] 0 = 4

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]
State after:
case intro
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
⊢ (finChainFnOfgood h).iterRangeCompl 4 = range (f^[4] 0)

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
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)

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]
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]

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⟩ ↦ ?_⟩
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

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]
State after:
no goals

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]
State after:
no goals

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]
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

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
State after:
no goals