[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i
[PROOFSTEP]
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ (x : ι), x ∈ Set.Ioi i → i ≤ x
[PROOFSTEP]
exact fun x hx ↦ le_of_lt hx
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k
[PROOFSTEP]
simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1) → x ≤ k
⊢ (∀ (x : ι), x ∈ Set.Ioc i j → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioc i j → x ≤ x_1) → x ≤ k
[PROOFSTEP]
refine' ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x _⟩
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1) → x ≤ k
x : ι
hx : ∀ (x_1 : ι), x_1 ∈ Set.Ioc i j → x ≤ x_1
⊢ ∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1
[PROOFSTEP]
intro y hy
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1) → x ≤ k
x : ι
hx : ∀ (x_1 : ι), x_1 ∈ Set.Ioc i j → x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
⊢ x ≤ y
[PROOFSTEP]
cases' le_or_lt y j with h_le h_lt
[GOAL]
case inl
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1) → x ≤ k
x : ι
hx : ∀ (x_1 : ι), x_1 ∈ Set.Ioc i j → x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y
[PROOFSTEP]
exact hx y ⟨hy, h_le⟩
[GOAL]
case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → k ≤ x) ∧ ∀ (x : ι), (∀ (x_1 : ι), x_1 ∈ Set.Ioi i → x ≤ x_1) → x ≤ k
x : ι
hx : ∀ (x_1 : ι), x_1 ∈ Set.Ioc i j → x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y
[PROOFSTEP]
exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i
[PROOFSTEP]
refine' fun j _ ↦ not_lt.mp fun hij_lt ↦ _
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
⊢ False
[PROOFSTEP]
have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ False
[PROOFSTEP]
have h_glb : IsGLB (Finset.Ioc i j : Set ι) i := by
  rw [Finset.coe_Ioc]
  have h := succFn_spec i
  rw [h_succFn_eq] at h
  exact isGLB_Ioc_of_isGLB_Ioi hij_lt h
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (↑(Finset.Ioc i j)) i
[PROOFSTEP]
rw [Finset.coe_Ioc]
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i
[PROOFSTEP]
have h := succFn_spec i
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioc i j) i
[PROOFSTEP]
rw [h_succFn_eq] at h
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i
[PROOFSTEP]
exact isGLB_Ioc_of_isGLB_Ioi hij_lt h
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ False
[PROOFSTEP]
have hi_mem : i ∈ Finset.Ioc i j := by
  refine' Finset.isGLB_mem _ h_glb _
  exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ i ∈ Finset.Ioc i j
[PROOFSTEP]
refine' Finset.isGLB_mem _ h_glb _
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ Finset.Nonempty (Finset.Ioc i j)
[PROOFSTEP]
exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i ∈ Finset.Ioc i j
⊢ False
[PROOFSTEP]
rw [Finset.mem_Ioc] at hi_mem
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False
[PROOFSTEP]
exact lt_irrefl i hi_mem.1
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
⊢ succFn i ≤ j
[PROOFSTEP]
have h := succFn_spec i
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j
[PROOFSTEP]
rw [IsGLB, IsGreatest, mem_lowerBounds] at h
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j
[PROOFSTEP]
exact h.1 j hij
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i
[PROOFSTEP]
rw [lt_isGLB_iff (succFn_spec i)] at hij
[GOAL]
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c, c ∈ lowerBounds (Set.Ioi i) ∧ j < c
⊢ j ≤ i
[PROOFSTEP]
obtain ⟨k, hk_lb, hk⟩ := hij
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i
[PROOFSTEP]
rw [mem_lowerBounds] at hk_lb
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ (x : ι), x ∈ Set.Ioi i → k ≤ x
hk : j < k
⊢ j ≤ i
[PROOFSTEP]
exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
⊢ ∀ {a b : ι}, a ≤ b → ∃ n, succ^[n] a = b
[PROOFSTEP]
intro i j hij
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ n, succ^[n] i = j
[PROOFSTEP]
rw [le_iff_lt_or_eq] at hij
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j
[PROOFSTEP]
cases' hij with hij hij
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j
case inr ι : Type u_1 inst✝¹ : LinearOrder ι inst✝ : LocallyFiniteOrder ι i j : ι hij : i = j ⊢ ∃ n, succ^[n] i = j
[PROOFSTEP]
swap
[GOAL]
case inr
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i = j
⊢ ∃ n, succ^[n] i = j
[PROOFSTEP]
refine' ⟨0, _⟩
[GOAL]
case inr
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i = j
⊢ succ^[0] i = j
[PROOFSTEP]
simpa only [Function.iterate_zero, id.def] using hij
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j
[PROOFSTEP]
by_contra h
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ¬∃ n, succ^[n] i = j
⊢ False
[PROOFSTEP]
push_neg at h
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ False
[PROOFSTEP]
have h_lt : ∀ n, succ^[n] i < j := by
  intro n
  induction' n with n hn
  · simpa only [Function.iterate_zero, id.def] using hij
  · refine' lt_of_le_of_ne _ (h _)
    rw [Function.iterate_succ', Function.comp_apply]
    exact succ_le_of_lt hn
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ ∀ (n : ℕ), succ^[n] i < j
[PROOFSTEP]
intro n
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
⊢ succ^[n] i < j
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ succ^[Nat.zero] i < j
[PROOFSTEP]
simpa only [Function.iterate_zero, id.def] using hij
[GOAL]
case succ
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ^[Nat.succ n] i < j
[PROOFSTEP]
refine' lt_of_le_of_ne _ (h _)
[GOAL]
case succ
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ^[Nat.succ n] i ≤ j
[PROOFSTEP]
rw [Function.iterate_succ', Function.comp_apply]
[GOAL]
case succ
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j
[PROOFSTEP]
exact succ_le_of_lt hn
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
⊢ False
[PROOFSTEP]
have h_mem : ∀ n, succ^[n] i ∈ Finset.Icc i j := fun n ↦ Finset.mem_Icc.mpr ⟨le_succ_iterate n i, (h_lt n).le⟩
[GOAL]
case inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
⊢ False
[PROOFSTEP]
obtain ⟨n, m, hnm, h_eq⟩ : ∃ n m, n < m ∧ succ^[n] i = succ^[m] i :=
  by
  let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
  obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m
  exact Finite.exists_ne_map_eq_of_infinite f
  have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [Subtype.mk_eq_mk] using hfnm
  cases' le_total n m with h_le h_le
  · exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
  · exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
⊢ ∃ n m, n ≠ m ∧ f n = f m
case intro.intro.intro
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
exact Finite.exists_ne_map_eq_of_infinite f
[GOAL]
case intro.intro.intro
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [Subtype.mk_eq_mk] using hfnm
[GOAL]
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
⊢ succ^[n] i = succ^[m] i
[PROOFSTEP]
simpa only [Subtype.mk_eq_mk] using hfnm
[GOAL]
case intro.intro.intro
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
cases' le_total n m with h_le h_le
[GOAL]
case intro.intro.intro.inl
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : n ≤ m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
[GOAL]
case intro.intro.intro.inr
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → { x // x ∈ Finset.Icc i j } := fun n => { val := succ^[n] i, property := (_ : succ^[n] i ∈ Finset.Icc i j) }
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : m ≤ n
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
[PROOFSTEP]
exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
⊢ False
[PROOFSTEP]
have h_max : IsMax (succ^[n] i) := isMax_iterate_succ_of_eq_of_ne h_eq hnm.ne
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
h_max : IsMax (succ^[n] i)
⊢ False
[PROOFSTEP]
exact not_le.mpr (h_lt n) (h_max (h_lt n).le)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ ∀ {a b : ι}, a ≤ b → ∃ n, pred^[n] b = a
[PROOFSTEP]
intro i j hij
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
⊢ ∃ n, pred^[n] j = i
[PROOFSTEP]
have h_exists := exists_succ_iterate_of_le hij
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
⊢ ∃ n, pred^[n] j = i
[PROOFSTEP]
obtain ⟨n, hn_eq, hn_lt_ne⟩ : ∃ n, succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
⊢ ∃ n, succ^[n] i = j ∧ ∀ (m : ℕ), m < n → succ^[m] i ≠ j
case intro.intro
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ (m : ℕ), m < n → succ^[m] i ≠ j
⊢ ∃ n, pred^[n] j = i
[PROOFSTEP]
exact ⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ (m : ℕ), m < n → succ^[m] i ≠ j
⊢ ∃ n, pred^[n] j = i
[PROOFSTEP]
refine' ⟨n, _⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ (m : ℕ), m < n → succ^[m] i ≠ j
⊢ pred^[n] j = i
[PROOFSTEP]
rw [← hn_eq]
[GOAL]
case intro.intro
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ (m : ℕ), m < n → succ^[m] i ≠ j
⊢ pred^[n] (succ^[n] i) = i
[PROOFSTEP]
induction' n with n
[GOAL]
case intro.intro.zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq✝ : succ^[n] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n → succ^[m] i ≠ j
hn_eq : succ^[Nat.zero] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.zero → succ^[m] i ≠ j
⊢ pred^[Nat.zero] (succ^[Nat.zero] i) = i
[PROOFSTEP]
simp only [Nat.zero_eq, Function.iterate_zero, id.def]
[GOAL]
case intro.intro.succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
[PROOFSTEP]
rw [pred_succ_iterate_of_not_isMax]
[GOAL]
case intro.intro.succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ ¬IsMax (succ^[Nat.succ n - 1] i)
[PROOFSTEP]
rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
[GOAL]
case intro.intro.succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ ¬IsMax (succ^[n] i)
[PROOFSTEP]
suffices : succ^[n] i < succ^[n.succ] i
[GOAL]
case intro.intro.succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
this : succ^[n] i < succ^[Nat.succ n] i
⊢ ¬IsMax (succ^[n] i)
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i < succ^[Nat.succ n] i
[PROOFSTEP]
exact not_isMax_of_lt this
[GOAL]
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i < succ^[Nat.succ n] i
[PROOFSTEP]
refine' lt_of_le_of_ne _ _
[GOAL]
case this.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ^[Nat.succ n] i
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
case this.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i ≤ (succ ∘ succ^[n]) i
[PROOFSTEP]
exact le_succ _
[GOAL]
case this.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i ≠ succ^[Nat.succ n] i
[PROOFSTEP]
rw [hn_eq]
[GOAL]
case this.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n✝ : ℕ
hn_eq✝ : succ^[n✝] i = j
hn_lt_ne✝ : ∀ (m : ℕ), m < n✝ → succ^[m] i ≠ j
n : ℕ
n_ih✝ : succ^[n] i = j → (∀ (m : ℕ), m < n → succ^[m] i ≠ j) → pred^[n] (succ^[n] i) = i
hn_eq : succ^[Nat.succ n] i = j
hn_lt_ne : ∀ (m : ℕ), m < Nat.succ n → succ^[m] i ≠ j
⊢ succ^[n] i ≠ j
[PROOFSTEP]
exact hn_lt_ne _ (Nat.lt_succ_self n)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ toZ i0 i0 = 0
[PROOFSTEP]
rw [toZ_of_ge le_rfl]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ ↑(Nat.find (_ : ∃ n, succ^[n] i0 = i0)) = 0
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ Nat.find (_ : ∃ n, succ^[n] i0 = i0) = 0
[PROOFSTEP]
refine' le_antisymm (Nat.find_le _) (zero_le _)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
⊢ succ^[0] i0 = i0
[PROOFSTEP]
rw [Function.iterate_zero, id.def]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i0 ≤ i
⊢ succ^[Int.toNat (toZ i0 i)] i0 = i
[PROOFSTEP]
rw [toZ_of_ge hi, Int.toNat_coe_nat]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find (_ : ∃ n, succ^[n] i0 = i)] i0 = i
[PROOFSTEP]
exact Nat.find_spec (exists_succ_iterate_of_le hi)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i < i0
⊢ pred^[Int.toNat (-toZ i0 i)] i0 = i
[PROOFSTEP]
rw [toZ_of_lt hi, neg_neg, Int.toNat_coe_nat]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i < i0
⊢ pred^[Nat.find (_ : ∃ n, pred^[n] i0 = i)] i0 = i
[PROOFSTEP]
exact Nat.find_spec (exists_pred_iterate_of_le hi.le)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ toZ i0 i
[PROOFSTEP]
rw [toZ_of_ge hi]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n, succ^[n] i0 = i))
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i < 0
[PROOFSTEP]
refine' lt_of_le_of_ne _ _
[GOAL]
case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0
[PROOFSTEP]
rw [toZ_of_lt hi, neg_nonpos]
[GOAL]
case refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n, pred^[n] i0 = i))
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0
[PROOFSTEP]
by_contra h
[GOAL]
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ False
[PROOFSTEP]
have h_eq := iterate_pred_toZ i hi
[GOAL]
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[Int.toNat (-toZ i0 i)] i0 = i
⊢ False
[PROOFSTEP]
rw [← h_eq, h] at hi
[GOAL]
case refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[Int.toNat (-0)] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[Int.toNat (-toZ i0 i)] i0 = i
⊢ False
[PROOFSTEP]
simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id.def, lt_self_iff_false] at hi
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ ↑n
[PROOFSTEP]
rw [toZ_of_ge (le_succ_iterate _ _)]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ ↑(Nat.find (_ : ∃ n_1, succ^[n_1] i0 = succ^[n] i0)) ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ Nat.find (_ : ∃ n_1, succ^[n_1] i0 = succ^[n] i0) ≤ n
[PROOFSTEP]
exact Nat.find_min' _ rfl
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
⊢ -↑n ≤ toZ i0 (pred^[n] i0)
[PROOFSTEP]
cases' le_or_lt i0 (pred^[n] i0) with h h
[GOAL]
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ pred^[n] i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)
[PROOFSTEP]
have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
[GOAL]
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)
[PROOFSTEP]
rw [h_eq, toZ_of_eq]
[GOAL]
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ 0
[PROOFSTEP]
simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
[GOAL]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)
[PROOFSTEP]
rw [toZ_of_lt h, neg_le_neg_iff]
[GOAL]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ ↑(Nat.find (_ : ∃ n_1, pred^[n_1] i0 = pred^[n] i0)) ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ Nat.find (_ : ∃ n_1, pred^[n_1] i0 = pred^[n] i0) ≤ n
[PROOFSTEP]
exact Nat.find_min' _ rfl
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
⊢ toZ i0 (succ^[n] i0) = ↑n
[PROOFSTEP]
let m := (toZ i0 (succ^[n] i0)).toNat
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
⊢ toZ i0 (succ^[n] i0) = ↑n
[PROOFSTEP]
have h_eq : succ^[m] i0 = succ^[n] i0 := iterate_succ_toZ _ (le_succ_iterate _ _)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
⊢ toZ i0 (succ^[n] i0) = ↑n
[PROOFSTEP]
by_cases hmn : m = n
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑n
[PROOFSTEP]
nth_rw 2 [← hmn]
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m
[PROOFSTEP]
rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, succ^[n_1] i0 = succ^[n] i0))
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ toZ i0 (succ^[n] i0) = ↑n
[PROOFSTEP]
suffices : IsMax (succ^[n] i0)
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
this : IsMax (succ^[n] i0)
⊢ toZ i0 (succ^[n] i0) = ↑n
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)
[PROOFSTEP]
exact absurd this hn
[GOAL]
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := Int.toNat (toZ i0 (succ^[n] i0))
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)
[PROOFSTEP]
exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[n] i0)
⊢ toZ i0 (pred^[n] i0) = -↑n
[PROOFSTEP]
cases' n with n n
[GOAL]
case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hn : ¬IsMin (pred^[Nat.zero] i0)
⊢ toZ i0 (pred^[Nat.zero] i0) = -↑Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, Function.iterate_zero, id.def, toZ_of_eq, Nat.cast_zero, neg_zero]
[GOAL]
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
have : pred^[n.succ] i0 < i0 :=
  by
  refine' lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn _
  have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by rwa [Function.iterate_zero, id.def]
  exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
⊢ pred^[Nat.succ n] i0 < i0
[PROOFSTEP]
refine' lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn _
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
h_pred_iterate_eq : pred^[Nat.succ n] i0 = i0
⊢ IsMin (pred^[Nat.succ n] i0)
[PROOFSTEP]
have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by rwa [Function.iterate_zero, id.def]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
h_pred_iterate_eq : pred^[Nat.succ n] i0 = i0
⊢ pred^[Nat.succ n] i0 = pred^[0] i0
[PROOFSTEP]
rwa [Function.iterate_zero, id.def]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
h_pred_iterate_eq : pred^[Nat.succ n] i0 = i0
h_pred_eq_pred : pred^[Nat.succ n] i0 = pred^[0] i0
⊢ IsMin (pred^[Nat.succ n] i0)
[PROOFSTEP]
exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
[GOAL]
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
let m := (-toZ i0 (pred^[n.succ] i0)).toNat
[GOAL]
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
have h_eq : pred^[m] i0 = pred^[n.succ] i0 := iterate_pred_toZ _ this
[GOAL]
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
by_cases hmn : m = n.succ
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : m = Nat.succ n
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
nth_rw 2 [← hmn]
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : m = Nat.succ n
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑m
[PROOFSTEP]
rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : m = Nat.succ n
⊢ 0 ≤ - -↑(Nat.find (_ : ∃ n_1, pred^[n_1] i0 = pred^[Nat.succ n] i0))
[PROOFSTEP]
rw [neg_neg]
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : m = Nat.succ n
⊢ 0 ≤ ↑(Nat.find (_ : ∃ n_1, pred^[n_1] i0 = pred^[Nat.succ n] i0))
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : ¬m = Nat.succ n
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
[PROOFSTEP]
suffices : IsMin (pred^[n.succ] i0)
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this✝ : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : ¬m = Nat.succ n
this : IsMin (pred^[Nat.succ n] i0)
⊢ toZ i0 (pred^[Nat.succ n] i0) = -↑(Nat.succ n)
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : ¬m = Nat.succ n
⊢ IsMin (pred^[Nat.succ n] i0)
[PROOFSTEP]
exact absurd this hn
[GOAL]
case this
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
n : ℕ
hn : ¬IsMin (pred^[Nat.succ n] i0)
this : pred^[Nat.succ n] i0 < i0
m : ℕ := Int.toNat (-toZ i0 (pred^[Nat.succ n] i0))
h_eq : pred^[m] i0 = pred^[Nat.succ n] i0
hmn : ¬m = Nat.succ n
⊢ IsMin (pred^[Nat.succ n] i0)
[PROOFSTEP]
exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
⊢ i ≤ j
[PROOFSTEP]
cases' le_or_lt i0 i with hi hi
[GOAL]
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
⊢ i ≤ j
[PROOFSTEP]
cases' le_or_lt i0 j with hj hj
[GOAL]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
⊢ i ≤ j
[PROOFSTEP]
cases' le_or_lt i0 j with hj hj
[GOAL]
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ i ≤ j
[PROOFSTEP]
rw [← iterate_succ_toZ i hi, ← iterate_succ_toZ j hj]
[GOAL]
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ succ^[Int.toNat (toZ i0 i)] i0 ≤ succ^[Int.toNat (toZ i0 j)] i0
[PROOFSTEP]
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)
[GOAL]
case inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j
[PROOFSTEP]
exact absurd ((toZ_neg hj).trans_le (toZ_nonneg hi)) (not_lt.mpr h_le)
[GOAL]
case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j
[PROOFSTEP]
exact hi.le.trans hj
[GOAL]
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j
[PROOFSTEP]
rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]
[GOAL]
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ pred^[Int.toNat (-toZ i0 i)] i0 ≤ pred^[Int.toNat (-toZ i0 j)] i0
[PROOFSTEP]
refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat _)
[GOAL]
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i j : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ -toZ i0 j ≤ -toZ i0 i
[PROOFSTEP]
exact neg_le_neg h_le
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
by_cases hi_max : IsMax i
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : IsMax i
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
rw [le_antisymm h_le (hi_max h_le)]
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
by_cases hj_min : IsMin j
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : IsMin j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
rw [le_antisymm h_le (hj_min h_le)]
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
cases' le_or_lt i0 i with hi hi
[GOAL]
case neg.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
cases' le_or_lt i0 j with hj hj
[GOAL]
case neg.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
cases' le_or_lt i0 j with hj hj
[GOAL]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
let m := Nat.find (exists_succ_iterate_of_le h_le)
[GOAL]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
have hm : succ^[m] i = j := Nat.find_spec (exists_succ_iterate_of_le h_le)
[GOAL]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
have hj_eq : j = succ^[(toZ i0 i).toNat + m] i0 :=
  by
  rw [← hm, add_comm]
  nth_rw 1 [← iterate_succ_toZ i hi]
  rw [Function.iterate_add]
  rfl
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
⊢ j = succ^[Int.toNat (toZ i0 i) + m] i0
[PROOFSTEP]
rw [← hm, add_comm]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
⊢ succ^[m] i = succ^[m + Int.toNat (toZ i0 i)] i0
[PROOFSTEP]
nth_rw 1 [← iterate_succ_toZ i hi]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
⊢ succ^[m] (succ^[Int.toNat (toZ i0 i)] i0) = succ^[m + Int.toNat (toZ i0 i)] i0
[PROOFSTEP]
rw [Function.iterate_add]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
⊢ succ^[m] (succ^[Int.toNat (toZ i0 i)] i0) = (succ^[m] ∘ succ^[Int.toNat (toZ i0 i)]) i0
[PROOFSTEP]
rfl
[GOAL]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
by_contra h
[GOAL]
case neg.inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
[PROOFSTEP]
by_cases hm0 : m = 0
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
[PROOFSTEP]
rw [hm0, Function.iterate_zero, id.def] at hm
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
[PROOFSTEP]
rw [hm] at h
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 j ≤ toZ i0 j
hm0 : m = 0
⊢ False
[PROOFSTEP]
exact h (le_of_eq rfl)
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
[PROOFSTEP]
refine' hi_max (max_of_succ_le (le_trans _ (@le_of_toZ_le _ _ _ _ _ i0 j i _)))
[GOAL]
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ succ i ≤ j
[PROOFSTEP]
have h_succ_le : succ^[(toZ i0 i).toNat + 1] i0 ≤ j :=
  by
  rw [hj_eq]
  refine' Monotone.monotone_iterate_of_le_map succ_mono (le_succ i0) (add_le_add_left _ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ succ^[Int.toNat (toZ i0 i) + 1] i0 ≤ j
[PROOFSTEP]
rw [hj_eq]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ succ^[Int.toNat (toZ i0 i) + 1] i0 ≤ succ^[Int.toNat (toZ i0 i) + m] i0
[PROOFSTEP]
refine' Monotone.monotone_iterate_of_le_map succ_mono (le_succ i0) (add_le_add_left _ _)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
[PROOFSTEP]
exact Nat.one_le_iff_ne_zero.mpr hm0
[GOAL]
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_succ_le : succ^[Int.toNat (toZ i0 i) + 1] i0 ≤ j
⊢ succ i ≤ j
[PROOFSTEP]
rwa [Function.iterate_succ', Function.comp_apply, iterate_succ_toZ i hi] at h_succ_le
[GOAL]
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : i0 ≤ j
m : ℕ := Nat.find (_ : ∃ n, succ^[n] i = j)
hm : succ^[m] i = j
hj_eq : j = succ^[Int.toNat (toZ i0 i) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i
[PROOFSTEP]
exact le_of_not_le h
[GOAL]
case neg.inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i0 ≤ i
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
exact absurd h_le (not_le.mpr (hj.trans_le hi))
[GOAL]
case neg.inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : i0 ≤ j
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
exact (toZ_neg hi).le.trans (toZ_nonneg hj)
[GOAL]
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
let m := Nat.find (exists_pred_iterate_of_le h_le)
[GOAL]
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
have hm : pred^[m] j = i := Nat.find_spec (exists_pred_iterate_of_le h_le)
[GOAL]
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
have hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0 :=
  by
  rw [← hm, add_comm]
  nth_rw 1 [← iterate_pred_toZ j hj]
  rw [Function.iterate_add]
  rfl
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
⊢ i = pred^[Int.toNat (-toZ i0 j) + m] i0
[PROOFSTEP]
rw [← hm, add_comm]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
⊢ pred^[m] j = pred^[m + Int.toNat (-toZ i0 j)] i0
[PROOFSTEP]
nth_rw 1 [← iterate_pred_toZ j hj]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
⊢ pred^[m] (pred^[Int.toNat (-toZ i0 j)] i0) = pred^[m + Int.toNat (-toZ i0 j)] i0
[PROOFSTEP]
rw [Function.iterate_add]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
⊢ pred^[m] (pred^[Int.toNat (-toZ i0 j)] i0) = (pred^[m] ∘ pred^[Int.toNat (-toZ i0 j)]) i0
[PROOFSTEP]
rfl
[GOAL]
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
⊢ toZ i0 i ≤ toZ i0 j
[PROOFSTEP]
by_contra h
[GOAL]
case neg.inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
⊢ False
[PROOFSTEP]
by_cases hm0 : m = 0
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
[PROOFSTEP]
rw [hm0, Function.iterate_zero, id.def] at hm
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : m = 0
⊢ False
[PROOFSTEP]
rw [hm] at h
[GOAL]
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 i
hm0 : m = 0
⊢ False
[PROOFSTEP]
exact h (le_of_eq rfl)
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ False
[PROOFSTEP]
refine' hj_min (min_of_le_pred _)
[GOAL]
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ j ≤ pred j
[PROOFSTEP]
refine' (@le_of_toZ_le _ _ _ _ _ i0 j i _).trans _
[GOAL]
case neg.refine'_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ toZ i0 j ≤ toZ i0 i
[PROOFSTEP]
exact le_of_not_le h
[GOAL]
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ i ≤ pred j
[PROOFSTEP]
have h_le_pred : i ≤ pred^[(-toZ i0 j).toNat + 1] i0 :=
  by
  rw [hj_eq]
  refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left _ _)
  exact Nat.one_le_iff_ne_zero.mpr hm0
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ i ≤ pred^[Int.toNat (-toZ i0 j) + 1] i0
[PROOFSTEP]
rw [hj_eq]
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ pred^[Int.toNat (-toZ i0 j) + m] i0 ≤ pred^[Int.toNat (-toZ i0 j) + 1] i0
[PROOFSTEP]
refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le i0) (add_le_add_left _ _)
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
⊢ 1 ≤ m
[PROOFSTEP]
exact Nat.one_le_iff_ne_zero.mpr hm0
[GOAL]
case neg.refine'_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i j : ι
h_le : i ≤ j
hi_max : ¬IsMax i
hj_min : ¬IsMin j
hi : i < i0
hj : j < i0
m : ℕ := Nat.find (_ : ∃ n, pred^[n] j = i)
hm : pred^[m] j = i
hj_eq : i = pred^[Int.toNat (-toZ i0 j) + m] i0
h : ¬toZ i0 i ≤ toZ i0 j
hm0 : ¬m = 0
h_le_pred : i ≤ pred^[Int.toNat (-toZ i0 j) + 1] i0
⊢ i ≤ pred j
[PROOFSTEP]
rwa [Function.iterate_succ', Function.comp_apply, iterate_pred_toZ j hj] at h_le_pred
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
⊢ ∀ {a b : ι},
    ↑(Equiv.ofInjective (toZ (Nonempty.some hι)) (_ : Function.Injective (toZ (Nonempty.some hι)))) a ≤
        ↑(Equiv.ofInjective (toZ (Nonempty.some hι)) (_ : Function.Injective (toZ (Nonempty.some hι)))) b ↔
      a ≤ b
[PROOFSTEP]
intro i j
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
i j : ι
⊢ ↑(Equiv.ofInjective (toZ (Nonempty.some hι)) (_ : Function.Injective (toZ (Nonempty.some hι)))) i ≤
      ↑(Equiv.ofInjective (toZ (Nonempty.some hι)) (_ : Function.Injective (toZ (Nonempty.some hι)))) j ↔
    i ≤ j
[PROOFSTEP]
exact toZ_le_iff i j
[GOAL]
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ Countable ι
[PROOFSTEP]
cases' isEmpty_or_nonempty ι with _ hι
[GOAL]
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
h✝ : IsEmpty ι
⊢ Countable ι
[PROOFSTEP]
infer_instance
[GOAL]
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
⊢ Countable ι
[PROOFSTEP]
exact Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι))
      (toZ (Nonempty.some hι) i) =
    i
[PROOFSTEP]
cases' le_or_lt hι.some i with hi hi
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : Nonempty.some hι ≤ i
⊢ (fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι))
      (toZ (Nonempty.some hι) i) =
    i
[PROOFSTEP]
have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : Nonempty.some hι ≤ i
h_nonneg : 0 ≤ toZ (Nonempty.some hι) i
⊢ (fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι))
      (toZ (Nonempty.some hι) i) =
    i
[PROOFSTEP]
simp_rw [if_pos h_nonneg]
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : Nonempty.some hι ≤ i
h_nonneg : 0 ≤ toZ (Nonempty.some hι) i
⊢ succ^[Int.toNat (toZ (Nonempty.some hι) i)] (Nonempty.some hι) = i
[PROOFSTEP]
exact iterate_succ_toZ i hi
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < Nonempty.some hι
⊢ (fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι))
      (toZ (Nonempty.some hι) i) =
    i
[PROOFSTEP]
have h_neg : toZ hι.some i < 0 := toZ_neg hi
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < Nonempty.some hι
h_neg : toZ (Nonempty.some hι) i < 0
⊢ (fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι))
      (toZ (Nonempty.some hι) i) =
    i
[PROOFSTEP]
simp_rw [if_neg (not_le.mpr h_neg)]
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < Nonempty.some hι
h_neg : toZ (Nonempty.some hι) i < 0
⊢ pred^[Int.toNat (-toZ (Nonempty.some hι) i)] (Nonempty.some hι) = i
[PROOFSTEP]
exact iterate_pred_toZ i hi
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ (Nonempty.some hι)
      ((fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι)) n) =
    n
[PROOFSTEP]
cases' le_or_lt 0 n with hn hn
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ (Nonempty.some hι)
      ((fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι)) n) =
    n
[PROOFSTEP]
simp_rw [if_pos hn]
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ (Nonempty.some hι) (succ^[Int.toNat n] (Nonempty.some hι)) = n
[PROOFSTEP]
rw [toZ_iterate_succ]
[GOAL]
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ ↑(Int.toNat n) = n
[PROOFSTEP]
exact Int.toNat_of_nonneg hn
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ (Nonempty.some hι)
      ((fun n => if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι)) n) =
    n
[PROOFSTEP]
simp_rw [if_neg (not_le.mpr hn)]
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ (Nonempty.some hι) (pred^[Int.toNat (-n)] (Nonempty.some hι)) = n
[PROOFSTEP]
rw [toZ_iterate_pred]
[GOAL]
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ -↑(Int.toNat (-n)) = n
[PROOFSTEP]
simp only [hn.le, Int.toNat_of_nonneg, Right.nonneg_neg_iff, neg_neg]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
⊢ ∀ {a b : ι},
    ↑{ toFun := toZ (Nonempty.some hι),
              invFun := fun n =>
                if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι),
              left_inv :=
                (_ :
                  ∀ (i : ι),
                    (fun n =>
                          if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                          else pred^[Int.toNat (-n)] (Nonempty.some hι))
                        (toZ (Nonempty.some hι) i) =
                      i),
              right_inv :=
                (_ :
                  ∀ (n : ℤ),
                    toZ (Nonempty.some hι)
                        ((fun n =>
                            if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                            else pred^[Int.toNat (-n)] (Nonempty.some hι))
                          n) =
                      n) }
          a ≤
        ↑{ toFun := toZ (Nonempty.some hι),
              invFun := fun n =>
                if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι),
              left_inv :=
                (_ :
                  ∀ (i : ι),
                    (fun n =>
                          if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                          else pred^[Int.toNat (-n)] (Nonempty.some hι))
                        (toZ (Nonempty.some hι) i) =
                      i),
              right_inv :=
                (_ :
                  ∀ (n : ℤ),
                    toZ (Nonempty.some hι)
                        ((fun n =>
                            if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                            else pred^[Int.toNat (-n)] (Nonempty.some hι))
                          n) =
                      n) }
          b ↔
      a ≤ b
[PROOFSTEP]
intro i j
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i j : ι
⊢ ↑{ toFun := toZ (Nonempty.some hι),
            invFun := fun n =>
              if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι),
            left_inv :=
              (_ :
                ∀ (i : ι),
                  (fun n =>
                        if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                        else pred^[Int.toNat (-n)] (Nonempty.some hι))
                      (toZ (Nonempty.some hι) i) =
                    i),
            right_inv :=
              (_ :
                ∀ (n : ℤ),
                  toZ (Nonempty.some hι)
                      ((fun n =>
                          if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                          else pred^[Int.toNat (-n)] (Nonempty.some hι))
                        n) =
                    n) }
        i ≤
      ↑{ toFun := toZ (Nonempty.some hι),
            invFun := fun n =>
              if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι) else pred^[Int.toNat (-n)] (Nonempty.some hι),
            left_inv :=
              (_ :
                ∀ (i : ι),
                  (fun n =>
                        if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                        else pred^[Int.toNat (-n)] (Nonempty.some hι))
                      (toZ (Nonempty.some hι) i) =
                    i),
            right_inv :=
              (_ :
                ∀ (n : ℤ),
                  toZ (Nonempty.some hι)
                      ((fun n =>
                          if 0 ≤ n then succ^[Int.toNat n] (Nonempty.some hι)
                          else pred^[Int.toNat (-n)] (Nonempty.some hι))
                        n) =
                    n) }
        j ↔
    i ≤ j
[PROOFSTEP]
exact toZ_le_iff i j
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i : ι
⊢ (fun n => succ^[n] ⊥) ((fun i => Int.toNat (toZ ⊥ i)) i) = i
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i : ι
⊢ succ^[Int.toNat (toZ ⊥ i)] ⊥ = i
[PROOFSTEP]
exact iterate_succ_toZ i bot_le
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (fun i => Int.toNat (toZ ⊥ i)) ((fun n => succ^[n] ⊥) n) = n
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ Int.toNat (toZ ⊥ (succ^[n] ⊥)) = n
[PROOFSTEP]
rw [toZ_iterate_succ]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ Int.toNat ↑n = n
[PROOFSTEP]
exact Int.toNat_coe_nat n
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
⊢ ∀ {a b : ι},
    ↑{ toFun := fun i => Int.toNat (toZ ⊥ i), invFun := fun n => succ^[n] ⊥,
              left_inv := (_ : ∀ (i : ι), (fun n => succ^[n] ⊥) ((fun i => Int.toNat (toZ ⊥ i)) i) = i),
              right_inv := (_ : ∀ (n : ℕ), (fun i => Int.toNat (toZ ⊥ i)) ((fun n => succ^[n] ⊥) n) = n) }
          a ≤
        ↑{ toFun := fun i => Int.toNat (toZ ⊥ i), invFun := fun n => succ^[n] ⊥,
              left_inv := (_ : ∀ (i : ι), (fun n => succ^[n] ⊥) ((fun i => Int.toNat (toZ ⊥ i)) i) = i),
              right_inv := (_ : ∀ (n : ℕ), (fun i => Int.toNat (toZ ⊥ i)) ((fun n => succ^[n] ⊥) n) = n) }
          b ↔
      a ≤ b
[PROOFSTEP]
intro i j
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ ↑{ toFun := fun i => Int.toNat (toZ ⊥ i), invFun := fun n => succ^[n] ⊥,
            left_inv := (_ : ∀ (i : ι), (fun n => succ^[n] ⊥) ((fun i => Int.toNat (toZ ⊥ i)) i) = i),
            right_inv := (_ : ∀ (n : ℕ), (fun i => Int.toNat (toZ ⊥ i)) ((fun n => succ^[n] ⊥) n) = n) }
        i ≤
      ↑{ toFun := fun i => Int.toNat (toZ ⊥ i), invFun := fun n => succ^[n] ⊥,
            left_inv := (_ : ∀ (i : ι), (fun n => succ^[n] ⊥) ((fun i => Int.toNat (toZ ⊥ i)) i) = i),
            right_inv := (_ : ∀ (n : ℕ), (fun i => Int.toNat (toZ ⊥ i)) ((fun n => succ^[n] ⊥) n) = n) }
        j ↔
    i ≤ j
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, Int.toNat_le]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(Int.toNat (toZ ⊥ j)) ↔ i ≤ j
[PROOFSTEP]
rw [← @toZ_le_iff ι _ _ _ _ ⊥, Int.toNat_of_nonneg (toZ_nonneg bot_le)]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ (fun i =>
        { val := Int.toNat (toZ ⊥ i),
          property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
      ((fun n => succ^[↑n] ⊥) n) =
    n
[PROOFSTEP]
ext1
[GOAL]
case a
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ ↑((fun i =>
          { val := Int.toNat (toZ ⊥ i),
            property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
        ((fun n => succ^[↑n] ⊥) n)) =
    ↑n
[PROOFSTEP]
simp only [Subtype.coe_mk]
[GOAL]
case a
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ Int.toNat (toZ ⊥ (succ^[↑n] ⊥)) = ↑n
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case a.refine'_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ Int.toNat (toZ ⊥ (succ^[↑n] ⊥)) ≤ ↑n
[PROOFSTEP]
rw [Int.toNat_le]
[GOAL]
case a.refine'_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ toZ ⊥ (succ^[↑n] ⊥) ≤ ↑↑n
[PROOFSTEP]
exact toZ_iterate_succ_le _
[GOAL]
case a.refine'_2
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
⊢ ↑n ≤ Int.toNat (toZ ⊥ (succ^[↑n] ⊥))
[PROOFSTEP]
by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))
[GOAL]
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
hn_max : IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ Int.toNat (toZ ⊥ (succ^[↑n] ⊥))
[PROOFSTEP]
rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max
[GOAL]
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
hn_max✝ : IsTop (succ^[↑n] ⊥)
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ Int.toNat (toZ ⊥ (succ^[↑n] ⊥))
[PROOFSTEP]
rw [hn_max]
[GOAL]
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
hn_max✝ : IsTop (succ^[↑n] ⊥)
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ Int.toNat (toZ ⊥ ⊤)
[PROOFSTEP]
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)
[GOAL]
case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ Int.toNat (toZ ⊥ (succ^[↑n] ⊥))
[PROOFSTEP]
rw [toZ_iterate_succ_of_not_isMax _ hn_max]
[GOAL]
case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ Int.toNat ↑↑n
[PROOFSTEP]
simp only [Int.toNat_coe_nat, le_refl]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
⊢ ∀ {a b : ι},
    ↑{
              toFun := fun i =>
                { val := Int.toNat (toZ ⊥ i),
                  property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) },
              invFun := fun n => succ^[↑n] ⊥, left_inv := (_ : ∀ (i : ι), succ^[Int.toNat (toZ ⊥ i)] ⊥ = i),
              right_inv :=
                (_ :
                  ∀ (n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }),
                    (fun i =>
                          { val := Int.toNat (toZ ⊥ i),
                            property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
                        ((fun n => succ^[↑n] ⊥) n) =
                      n) }
          a ≤
        ↑{
              toFun := fun i =>
                { val := Int.toNat (toZ ⊥ i),
                  property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) },
              invFun := fun n => succ^[↑n] ⊥, left_inv := (_ : ∀ (i : ι), succ^[Int.toNat (toZ ⊥ i)] ⊥ = i),
              right_inv :=
                (_ :
                  ∀ (n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }),
                    (fun i =>
                          { val := Int.toNat (toZ ⊥ i),
                            property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
                        ((fun n => succ^[↑n] ⊥) n) =
                      n) }
          b ↔
      a ≤ b
[PROOFSTEP]
intro i j
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ ↑{
            toFun := fun i =>
              { val := Int.toNat (toZ ⊥ i),
                property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) },
            invFun := fun n => succ^[↑n] ⊥, left_inv := (_ : ∀ (i : ι), succ^[Int.toNat (toZ ⊥ i)] ⊥ = i),
            right_inv :=
              (_ :
                ∀ (n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }),
                  (fun i =>
                        { val := Int.toNat (toZ ⊥ i),
                          property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
                      ((fun n => succ^[↑n] ⊥) n) =
                    n) }
        i ≤
      ↑{
            toFun := fun i =>
              { val := Int.toNat (toZ ⊥ i),
                property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) },
            invFun := fun n => succ^[↑n] ⊥, left_inv := (_ : ∀ (i : ι), succ^[Int.toNat (toZ ⊥ i)] ⊥ = i),
            right_inv :=
              (_ :
                ∀ (n : { x // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }),
                  (fun i =>
                        { val := Int.toNat (toZ ⊥ i),
                          property := (_ : Int.toNat (toZ ⊥ i) ∈ Finset.range (Nat.succ (Int.toNat (toZ ⊥ ⊤)))) })
                      ((fun n => succ^[↑n] ⊥) n) =
                    n) }
        j ↔
    i ≤ j
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]
[GOAL]
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(Int.toNat (toZ ⊥ j)) ↔ i ≤ j
[PROOFSTEP]
rw [← @toZ_le_iff ι _ _ _ _ ⊥, Int.toNat_of_nonneg (toZ_nonneg bot_le)]


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.univ = {⊤, ⊥}
[PROOFSTEP]
change Finset.map _ (Finset.univ : Finset Bool) = _
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      Finset.univ =
    {⊤, ⊥}
[PROOFSTEP]
rw [Fintype.univ_bool]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ↑IsSimpleOrder.equivBool.symm, inj' := (_ : Function.Injective ↑IsSimpleOrder.equivBool.symm) }
      {true, false} =
    {⊤, ⊥}
[PROOFSTEP]
simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {↑IsSimpleOrder.equivBool.symm true, ↑IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤
[PROOFSTEP]
rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ← Fintype.univ_bool]
[GOAL]
α : Type u_1
β : Type u_2
a : Bool
⊢ a ∈ Finset.univ
[PROOFSTEP]
apply Finset.mem_univ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
⊢ IsCoatomic α
[PROOFSTEP]
refine' IsCoatomic.mk fun b => or_iff_not_imp_left.2 fun ht => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
⊢ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
obtain ⟨c, hc, hmax⟩ := Set.Finite.exists_maximal_wrt id {x : α | b ≤ x ∧ x ≠ ⊤} (Set.toFinite _) ⟨b, le_rfl, ht⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
⊢ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
refine' ⟨c, ⟨hc.2, fun y hcy => _⟩, hc.1⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
y : α
hcy : c < y
⊢ y = ⊤
[PROOFSTEP]
by_contra hyt
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
y : α
hcy : c < y
hyt : ¬y = ⊤
⊢ False
[PROOFSTEP]
obtain rfl : c = y := hmax y ⟨hc.1.trans hcy.le, hyt⟩ hcy.le
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : Finite α
b : α
ht : ¬b = ⊤
c : α
hc : c ∈ {x | b ≤ x ∧ x ≠ ⊤}
hmax : ∀ (a' : α), a' ∈ {x | b ≤ x ∧ x ≠ ⊤} → id c ≤ id a' → id c = id a'
hcy : c < c
hyt : ¬c = ⊤
⊢ False
[PROOFSTEP]
exact (lt_self_iff_false _).mp hcy