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

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ Disjoint (h.exactIterRange m) (h.exactIterRange n)
Tactic:
rw [disjoint_iff_ne]
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ ∀ a ∈ h.exactIterRange m, ∀ b ∈ h.exactIterRange n, a ≠ b

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ ∀ a ∈ h.exactIterRange m, ∀ b ∈ h.exactIterRange n, a ≠ b
Tactic:
intro a h1 b h2
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.exactIterRange m
b : α
h2 : b ∈ h.exactIterRange n
⊢ a ≠ b

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.exactIterRange m
b : α
h2 : b ∈ h.exactIterRange n
⊢ a ≠ b
Tactic:
rw [h.mem_exactIterRange_iff] at h1 h2
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : ∃ b ∈ h.rangeCompl, f^[m] b = a
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
⊢ a ≠ b

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : ∃ b ∈ h.rangeCompl, f^[m] b = a
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
⊢ a ≠ b
Tactic:
rcases h1 with ⟨a, h1, rfl⟩
State after:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
a : α
h1 : a ∈ h.rangeCompl
⊢ f^[m] a ≠ b

State before:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
a : α
h1 : a ∈ h.rangeCompl
⊢ f^[m] a ≠ b
Tactic:
rcases h2 with ⟨b, h2, rfl⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.rangeCompl
b : α
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.rangeCompl
b : α
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b
Tactic:
exact h.iter_apply_ne_of_mem_rangeCompl_iter_ne h0 h1 h2
State after:
no goals