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

State before:
f : ℕ → ℕ
h : good f
⊢ (finChainFnOfgood h).iterRangeCompl 3 ⊆ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl
Tactic:
intro x h0
State after:
f : ℕ → ℕ
h : good f
x : ℕ
h0 : x ∈ (finChainFnOfgood h).iterRangeCompl 3
⊢ x ∈ {0, (f 0).succ} ∪ image Nat.succ (finChainFnOfgood h).rangeCompl

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

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

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

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

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

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

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

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

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

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

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