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

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
State after:
f : ℕ → ℕ
h : good f
h0 : ((finChainFnOfgood h).iterRangeCompl 3).card ≤ 2 + (finChainFnOfgood h).rangeCompl.card
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}

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
State after:
f : ℕ → ℕ
h : good f
h0 : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}

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 ↦ ?_)
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}

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
State after:
f : ℕ → ℕ
h : good f
h0✝ : (finChainFnOfgood h).rangeCompl.card ≤ 2 / Nat.succ 1
h0 : Function.Surjective f
⊢ ∃ a, (finChainFnOfgood h).rangeCompl = {a}

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

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