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

State before:
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b
Tactic:
wlog h3 : m < n
State after:
case inr
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
this :
  ∀ {α : Type u_1} {f : α → α} (h : FinChainFn f) {m n : ℕ} {a b : α},
    m ≠ n → a ∈ h.rangeCompl → b ∈ h.rangeCompl → m < n → f^[m] a ≠ f^[n] b
h3 : ¬m < n
⊢ f^[m] a ≠ f^[n] b

α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b

State before:
case inr
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
this :
  ∀ {α : Type u_1} {f : α → α} (h : FinChainFn f) {m n : ℕ} {a b : α},
    m ≠ n → a ∈ h.rangeCompl → b ∈ h.rangeCompl → m < n → f^[m] a ≠ f^[n] b
h3 : ¬m < n
⊢ f^[m] a ≠ f^[n] b

α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Tactic:
exact (this h h0.symm h2 h1 <| (le_of_not_lt h3).lt_of_ne h0.symm).symm
State after:
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b

State before:
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Tactic:
rcases Nat.exists_eq_add_of_le h3.le with ⟨k, rfl⟩
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : m < m + k
⊢ f^[m] a ≠ f^[m + k] b

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : m < m + k
⊢ f^[m] a ≠ f^[m + k] b
Tactic:
rw [Nat.lt_add_right_iff_pos] at h3
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ f^[m] a ≠ f^[m + k] b

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ f^[m] a ≠ f^[m + k] b
Tactic:
rw [f.iterate_add_apply m k b, (h.injective.iterate m).ne_iff]
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ a ≠ f^[k] b

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ a ≠ f^[k] b
Tactic:
rintro rfl
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : f^[k] b ∈ h.rangeCompl
⊢ False

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : f^[k] b ∈ h.rangeCompl
⊢ False
Tactic:
rw [mem_rangeCompl_iff, Set.mem_range] at h1
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ False

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ False
Tactic:
refine h1 ⟨f^[k.pred] b, ?_⟩
State after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ f (f^[k.pred] b) = f^[k] b

State before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ f (f^[k.pred] b) = f^[k] b
Tactic:
rw [← f.iterate_succ_apply', Nat.succ_pred_eq_of_pos h3]
State after:
no goals