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

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
⊢ ↑(h.iterRangeCompl 0) = (Set.range f^[0])ᶜ
Tactic:
rw [iterRangeCompl_zero, coe_empty,
  iterate_zero, Set.range_id, Set.compl_univ]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ ↑(h.iterRangeCompl (n + 1)) = (Set.range f^[n + 1])ᶜ
Tactic:
rw [h.iterRangeCompl_succ, coe_union, iterRangeCompl_spec n,
  h.exactIterRange_spec, Set.diff_eq, Set.inter_union_distrib_right,
  Set.union_compl_self, Set.univ_inter, ← Set.compl_inter]
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (Set.range f^[n + 1] ∩ Set.range f^[n])ᶜ = (Set.range f^[n + 1])ᶜ

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (Set.range f^[n + 1] ∩ Set.range f^[n])ᶜ = (Set.range f^[n + 1])ᶜ
Tactic:
refine congr_arg _ (Set.inter_eq_left.mpr λ x h1 ↦ ?_)
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : x ∈ Set.range f^[n + 1]
⊢ x ∈ Set.range f^[n]

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : x ∈ Set.range f^[n + 1]
⊢ x ∈ Set.range f^[n]
Tactic:
rw [Set.mem_range] at h1 ⊢
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : ∃ y, f^[n + 1] y = x
⊢ ∃ y, f^[n] y = x

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : ∃ y, f^[n + 1] y = x
⊢ ∃ y, f^[n] y = x
Tactic:
rcases h1 with ⟨y, rfl⟩
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
y : α
⊢ ∃ y_1, f^[n] y_1 = f^[n + 1] y

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
y : α
⊢ ∃ y_1, f^[n] y_1 = f^[n + 1] y
Tactic:
exact ⟨f y, rfl⟩
State after:
no goals