[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ ↑(⨅ (i : ι), f i) x = iInf (fun i => ↑(f i)) x
[PROOFSTEP]
simp [iInf_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ ↑(⨆ (i : ι), f i) x = iSup (fun i => ↑(f i)) x
[PROOFSTEP]
simp [iSup_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
src✝² : Lattice (α →o β) := lattice
src✝¹ : OrderTop (α →o β) := orderTop
src✝ : OrderBot (α →o β) := orderBot
s : Set (α →o β)
f : α →o β
hf : f ∈ s
x : α
⊢ toFun f x ≤ ⨆ (_ : f ∈ s), ↑f x
[PROOFSTEP]
apply le_iSup _ hf
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
⊢ ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
[PROOFSTEP]
exact h 1 0
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
[PROOFSTEP]
intro n₁ n₂ a₁ a₂
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
[PROOFSTEP]
have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
  intro n
  induction' n with n ih <;> intro a₁ a₂
  · rfl
  ·
    calc
      f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
      _ ≤ f^[n] (f a₁ ⊔ a₂) := (f.mono.iterate n (h a₁ a₂))
      _ ≤ f^[n] (f a₁) ⊔ a₂ := (ih _ _)
      _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (n : ℕ) (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
[PROOFSTEP]
intro n
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
⊢ ∀ (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (a₁ a₂ : α), (↑f)^[Nat.zero] (a₁ ⊔ a₂) ≤ (↑f)^[Nat.zero] a₁ ⊔ a₂
[PROOFSTEP]
intro a₁ a₂
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
⊢ ∀ (a₁ a₂ : α), (↑f)^[Nat.succ n] (a₁ ⊔ a₂) ≤ (↑f)^[Nat.succ n] a₁ ⊔ a₂
[PROOFSTEP]
intro a₁ a₂
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ a₁ a₂ : α
⊢ (↑f)^[Nat.zero] (a₁ ⊔ a₂) ≤ (↑f)^[Nat.zero] a₁ ⊔ a₂
[PROOFSTEP]
rfl
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (↑f)^[Nat.succ n] (a₁ ⊔ a₂) ≤ (↑f)^[Nat.succ n] a₁ ⊔ a₂
[PROOFSTEP]
calc
  f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
  _ ≤ f^[n] (f a₁ ⊔ a₂) := (f.mono.iterate n (h a₁ a₂))
  _ ≤ f^[n] (f a₁) ⊔ a₂ := (ih _ _)
  _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (↑f)^[n] (↑f a₁) ⊔ a₂ = (↑f)^[n + 1] a₁ ⊔ a₂
[PROOFSTEP]
rw [← Function.iterate_succ_apply]
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
⊢ (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
[PROOFSTEP]
calc
  f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) := Function.iterate_add_apply f n₁ n₂ _
  _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
  _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := (f.mono.iterate n₁ (h' n₂ _ _))
  _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
  _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
⊢ (↑f)^[n₁] ((↑f)^[n₂] (a₁ ⊔ a₂)) = (↑f)^[n₁] ((↑f)^[n₂] (a₂ ⊔ a₁))
[PROOFSTEP]
rw [sup_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f)^[n] (a₁ ⊔ a₂) ≤ (↑f)^[n] a₁ ⊔ a₂
⊢ (↑f)^[n₁] ((↑f)^[n₂] a₂ ⊔ a₁) = (↑f)^[n₁] (a₁ ⊔ (↑f)^[n₂] a₂)
[PROOFSTEP]
rw [sup_comm]


[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
⊢ ∀ (a : αᵒᵈ), (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual) a ≤ a
[PROOFSTEP]
simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual, SuccOrder.le_succ, implies_true]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a✝ : αᵒᵈ
h : a✝ ≤ (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual) a✝
⊢ IsMin a✝
[PROOFSTEP]
apply SuccOrder.max_of_succ_le h
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
⊢ ∀ {a b : αᵒᵈ}, a < b → a ≤ (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual) b
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : αᵒᵈ
h : a < b
⊢ a ≤ (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual) b
[PROOFSTEP]
exact SuccOrder.succ_le_of_lt h
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ ∀ (a : αᵒᵈ), a ≤ (↑toDual ∘ PredOrder.pred ∘ ↑ofDual) a
[PROOFSTEP]
simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual, PredOrder.pred_le, implies_true]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a✝ : αᵒᵈ
h : (↑toDual ∘ PredOrder.pred ∘ ↑ofDual) a✝ ≤ a✝
⊢ IsMax a✝
[PROOFSTEP]
apply PredOrder.min_of_le_pred h
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ ∀ {a b : αᵒᵈ}, a < b → (↑toDual ∘ PredOrder.pred ∘ ↑ofDual) a ≤ b
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : αᵒᵈ
h : a < b
⊢ (↑toDual ∘ PredOrder.pred ∘ ↑ofDual) a ≤ b
[PROOFSTEP]
exact PredOrder.le_pred_of_lt h
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ a < succ a
[PROOFSTEP]
simpa using (hn h a).not
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ ¬succ a ≤ a
[PROOFSTEP]
simpa using (hn h a).not
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a b : α
hab : a < succ b
h : ¬IsMax b
⊢ a ≤ b
[PROOFSTEP]
simpa [hab] using (hn h a).not
[GOAL]
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
α : Type ?u.4579
inst✝ : LinearOrder α
pred : α → α
hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a
hm : ∀ (a : α), IsMin a → pred a = a
a : α
h : ¬IsMin a
⊢ pred a < a
[PROOFSTEP]
simpa using (hn h a).not
[GOAL]
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
α : Type ?u.4579
inst✝ : LinearOrder α
pred : α → α
hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a
hm : ∀ (a : α), IsMin a → pred a = a
a : α
h : ¬IsMin a
⊢ ¬a ≤ pred a
[PROOFSTEP]
simpa using (hn h a).not
[GOAL]
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
α : Type ?u.4579
inst✝ : LinearOrder α
pred : α → α
hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a
hm : ∀ (a : α), IsMin a → pred a = a
a b : α
hab : pred a < b
h : ¬IsMin a
⊢ a ≤ b
[PROOFSTEP]
simpa [hab] using (hn h b).not
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a < succ b ↔ a < b
[PROOFSTEP]
rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ succ b ↔ a ≤ b
[PROOFSTEP]
rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b
[PROOFSTEP]
by_cases hb : IsMax b
[GOAL]
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b
[PROOFSTEP]
by_cases hba : b ≤ a
[GOAL]
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b
[PROOFSTEP]
exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
[GOAL]
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b
[PROOFSTEP]
exact succ_le_of_lt ((h.lt_of_not_le hba).trans_le <| le_succ b)
[GOAL]
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
[PROOFSTEP]
rwa [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h, lt_succ_iff_of_not_isMax hb]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ x ≤ succ^[k] x
[PROOFSTEP]
conv_lhs => rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ x = id^[k] x
[PROOFSTEP]
simp only [Function.iterate_id, id.def]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ id^[k] x ≤ succ^[k] x
[PROOFSTEP]
exact Monotone.le_iterate_of_le succ_mono le_succ k x
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ IsMax (succ^[n] a)
[PROOFSTEP]
refine' max_of_succ_le (le_trans _ h_eq.symm.le)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a
[PROOFSTEP]
have : succ (succ^[n] a) = succ^[n + 1] a := by rw [Function.iterate_succ', comp]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) = succ^[n + 1] a
[PROOFSTEP]
rw [Function.iterate_succ', comp]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
this : succ (succ^[n] a) = succ^[n + 1] a
⊢ succ (succ^[n] a) ≤ succ^[m] a
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
this : succ (succ^[n] a) = succ^[n + 1] a
⊢ succ^[n + 1] a ≤ succ^[m] a
[PROOFSTEP]
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
this : succ (succ^[n] a) = succ^[n + 1] a
h_le : n + 1 ≤ m
⊢ succ^[n + 1] a ≤ succ^[m] a
[PROOFSTEP]
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)
[PROOFSTEP]
cases' le_total n m with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax (succ^[n] a)
[PROOFSTEP]
exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
[GOAL]
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)
[PROOFSTEP]
rw [h_eq]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[m] a)
[PROOFSTEP]
exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b
[PROOFSTEP]
rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioo a (succ b) = Ioc a b
[PROOFSTEP]
rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b
[PROOFSTEP]
rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
[PROOFSTEP]
rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a < succ b ↔ a < b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a = succ b ↔ a = b
[PROOFSTEP]
rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb, succ_lt_succ_iff_of_not_isMax ha hb]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
[PROOFSTEP]
refine' ⟨fun h => or_iff_not_imp_left.2 fun hba : b ≠ a => h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), _⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b
[PROOFSTEP]
exact ⟨le_rfl, le_succ b⟩
[GOAL]
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a
[PROOFSTEP]
exact ⟨le_succ a, le_rfl⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a
[PROOFSTEP]
obtain h | rfl := h.covby_or_eq
[GOAL]
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h✝ : a ⩿ b
h : a ⋖ b
⊢ b ≤ succ a
[PROOFSTEP]
exact (Covby.succ_eq h).ge
[GOAL]
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
h : a ⩿ a
⊢ a ≤ succ a
[PROOFSTEP]
exact le_succ _
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
[PROOFSTEP]
by_cases hb : IsMax b
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
[PROOFSTEP]
rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
[PROOFSTEP]
rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)
[PROOFSTEP]
simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)
[PROOFSTEP]
simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)
[PROOFSTEP]
simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)
[PROOFSTEP]
simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a = b → a ⋖ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a
[PROOFSTEP]
exact covby_succ _
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : OrderTop α
⊢ succ ⊤ = ⊤
[PROOFSTEP]
rw [succ_eq_iff_isMax, isMax_iff_eq_top]
[GOAL]
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
a b : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a < succ ⊥ ↔ a = ⊥
[PROOFSTEP]
rw [lt_succ_iff, le_bot_iff]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : OrderBot α
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
[PROOFSTEP]
rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
⊢ ∀ (a b : SuccOrder α), a = b
[PROOFSTEP]
intro h₀ h₁
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
⊢ h₀ = h₁
[PROOFSTEP]
ext a
[GOAL]
case succ.h
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
⊢ SuccOrder.succ a = SuccOrder.succ a
[PROOFSTEP]
by_cases ha : IsMax a
[GOAL]
case pos
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a
[PROOFSTEP]
exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm
[GOAL]
case neg
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a
[PROOFSTEP]
exact @Covby.succ_eq _ _ h₀ _ _ (covby_succ_of_not_isMax ha)
[GOAL]
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = ⨅ (b : α) (_ : a < b), b
[PROOFSTEP]
refine' le_antisymm (le_iInf fun b => le_iInf succ_le_of_lt) _
[GOAL]
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ ⨅ (b : α) (_ : a < b), b ≤ succ a
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a ⊤
[GOAL]
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ ⨅ (b : α) (_ : ⊤ < b), b ≤ succ ⊤
[PROOFSTEP]
rw [succ_top]
[GOAL]
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ ⨅ (b : α) (_ : ⊤ < b), b ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ ⨅ (b : α) (_ : a < b), b ≤ succ a
[PROOFSTEP]
exact iInf₂_le _ (lt_succ_iff_ne_top.2 ha)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ pred^[k] x ≤ x
[PROOFSTEP]
conv_rhs => rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
| x
[PROOFSTEP]
rw [(by simp only [Function.iterate_id, id.def] : x = id^[k] x)]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ x = id^[k] x
[PROOFSTEP]
simp only [Function.iterate_id, id.def]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ pred^[k] x ≤ id^[k] x
[PROOFSTEP]
exact Monotone.iterate_le_of_le pred_mono pred_le k x
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioc (pred a) b = Icc a b
[PROOFSTEP]
rw [← Ioi_inter_Iic, Ioi_pred_of_not_isMin ha, Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioo (pred a) b = Ico a b
[PROOFSTEP]
rw [← Ioi_inter_Iio, Ioi_pred_of_not_isMin ha, Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin b
⊢ Icc a (pred b) = Ico a b
[PROOFSTEP]
rw [← Ici_inter_Iic, Iic_pred_of_not_isMin ha, Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b
[PROOFSTEP]
rw [← Ioi_inter_Iic, Iic_pred_of_not_isMin ha, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a ≤ pred b ↔ a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a < pred b ↔ a < b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a✝ b✝ a b : α
⊢ pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a
[PROOFSTEP]
refine' ⟨fun h => or_iff_not_imp_left.2 fun hba : b ≠ a => (le_pred_of_lt <| h.2.lt_of_ne hba).antisymm h.1, _⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a✝ b✝ a b : α
⊢ b = a ∨ b = pred a → pred a ≤ b ∧ b ≤ a
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b✝ b : α
⊢ pred b ≤ b ∧ b ≤ b
[PROOFSTEP]
exact ⟨pred_le b, le_rfl⟩
[GOAL]
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a✝ b a : α
⊢ pred a ≤ pred a ∧ pred a ≤ a
[PROOFSTEP]
exact ⟨le_rfl, pred_le a⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
⊢ pred b ≤ a
[PROOFSTEP]
obtain h | rfl := h.covby_or_eq
[GOAL]
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h✝ : a ⩿ b
h : a ⋖ b
⊢ pred b ≤ a
[PROOFSTEP]
exact (Covby.pred_eq h).le
[GOAL]
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a : α
h : a ⩿ a
⊢ pred a ≤ a
[PROOFSTEP]
exact pred_le _
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
[PROOFSTEP]
by_cases ha : IsMin a
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
[PROOFSTEP]
rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
[PROOFSTEP]
rw [← pred_lt_iff_of_not_isMin ha, le_iff_eq_or_lt, eq_comm]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioi (pred a) = insert a (Ioi a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)
[PROOFSTEP]
simp only [insert, mem_setOf, @eq_comm _ x a, mem_Ioi, Set.insert]
[GOAL]
case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a = x ∨ a < x
[PROOFSTEP]
exact pred_lt_iff_eq_or_lt_of_not_isMin ha
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
⊢ Icc (pred a) b = insert (pred a) (Icc a b)
[PROOFSTEP]
simp_rw [← Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
⊢ Ico (pred a) b = insert (pred a) (Ico a b)
[PROOFSTEP]
simp_rw [← Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a = pred b ↔ a = b
[PROOFSTEP]
simp_rw [eq_iff_le_not_lt, pred_le_pred_iff, pred_lt_pred_iff]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred b = a → a ⋖ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
b : α
inst✝ : NoMinOrder α
⊢ pred b ⋖ b
[PROOFSTEP]
exact pred_covby _
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ Ioc (pred a) b = insert a (Ioc a b)
[PROOFSTEP]
simp_rw [← Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a < b
⊢ Ioo (pred a) b = insert a (Ioo a b)
[PROOFSTEP]
simp_rw [← Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
⊢ ∀ (a b : PredOrder α), a = b
[PROOFSTEP]
intro h₀ h₁
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : PredOrder α
⊢ h₀ = h₁
[PROOFSTEP]
ext a
[GOAL]
case pred.h
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : PredOrder α
a : α
⊢ PredOrder.pred a = PredOrder.pred a
[PROOFSTEP]
by_cases ha : IsMin a
[GOAL]
case pos
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : PredOrder α
a : α
ha : IsMin a
⊢ PredOrder.pred a = PredOrder.pred a
[PROOFSTEP]
exact (@IsMin.pred_eq _ _ h₀ _ ha).trans ha.pred_eq.symm
[GOAL]
case neg
α : Type u_1
inst✝ : PartialOrder α
h₀ h₁ : PredOrder α
a : α
ha : ¬IsMin a
⊢ PredOrder.pred a = PredOrder.pred a
[PROOFSTEP]
exact @Covby.pred_eq _ _ h₀ _ _ (pred_covby_of_not_isMin ha)
[GOAL]
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
⊢ pred a = ⨆ (b : α) (_ : b < a), b
[PROOFSTEP]
refine' le_antisymm _ (iSup_le fun b => iSup_le le_pred_of_lt)
[GOAL]
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a ⊥
[GOAL]
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ pred ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b
[PROOFSTEP]
rw [pred_bot]
[GOAL]
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b
[PROOFSTEP]
exact bot_le
[GOAL]
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
ha : a ≠ ⊥
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
[PROOFSTEP]
exact @le_iSup₂ _ _ (fun b => b < a) _ (fun a _ => a) (pred a) (pred_lt_iff_ne_bot.2 ha)
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax (succ^[n - 1] i)
hin : ¬IsMax (succ^[Nat.zero - 1] i)
⊢ pred^[Nat.zero] (succ^[Nat.zero] i) = i
[PROOFSTEP]
simp only [Nat.zero_eq, Function.iterate_zero, id.def]
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[Nat.succ n - 1] i)
⊢ pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
[PROOFSTEP]
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
[PROOFSTEP]
have h_not_max : ¬IsMax (succ^[n - 1] i) := by
  cases' n with n
  · simpa using hin
  rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
  have h_sub_le : succ^[n] i ≤ succ^[n.succ] i :=
    by
    rw [Function.iterate_succ']
    exact le_succ _
  refine' fun h_max => hin fun j hj => _
  have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
  exact hj_le.trans h_sub_le
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ ¬IsMax (succ^[n - 1] i)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax (succ^[n - 1] i)
hn : ¬IsMax (succ^[Nat.zero - 1] i) → pred^[Nat.zero] (succ^[Nat.zero] i) = i
hin : ¬IsMax (succ^[Nat.zero] i)
⊢ ¬IsMax (succ^[Nat.zero - 1] i)
[PROOFSTEP]
simpa using hin
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[Nat.succ n - 1] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
⊢ ¬IsMax (succ^[Nat.succ n - 1] i)
[PROOFSTEP]
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
⊢ ¬IsMax (succ^[n] i)
[PROOFSTEP]
have h_sub_le : succ^[n] i ≤ succ^[n.succ] i :=
  by
  rw [Function.iterate_succ']
  exact le_succ _
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
⊢ succ^[n] i ≤ succ^[Nat.succ n] i
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
⊢ succ^[n] i ≤ (succ ∘ succ^[n]) i
[PROOFSTEP]
exact le_succ _
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
h_sub_le : succ^[n] i ≤ succ^[Nat.succ n] i
⊢ ¬IsMax (succ^[n] i)
[PROOFSTEP]
refine' fun h_max => hin fun j hj => _
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
h_sub_le : succ^[n] i ≤ succ^[Nat.succ n] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[Nat.succ n] i ≤ j
⊢ j ≤ succ^[Nat.succ n] i
[PROOFSTEP]
have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
hin : ¬IsMax (succ^[Nat.succ n] i)
h_sub_le : succ^[n] i ≤ succ^[Nat.succ n] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[Nat.succ n] i ≤ j
hj_le : j ≤ succ^[n] i
⊢ j ≤ succ^[Nat.succ n] i
[PROOFSTEP]
exact hj_le.trans h_sub_le
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[Nat.succ n] (succ^[Nat.succ n] i) = i
[PROOFSTEP]
rw [Function.iterate_succ, Function.iterate_succ']
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (pred (succ (succ^[n] i))) = i
[PROOFSTEP]
rw [pred_succ_of_not_isMax hin]
[GOAL]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax (succ^[n✝ - 1] i)
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i
[PROOFSTEP]
exact hn h_not_max
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : WithTop α
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      a
[PROOFSTEP]
cases' a with a a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
⊢ none ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      none
[PROOFSTEP]
exact le_top
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : α
⊢ Option.some a ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      (Option.some a)
[PROOFSTEP]
change _ ≤ ite _ _ _
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : α
⊢ Option.some a ≤ if a = ⊤ then ⊤ else ↑(succ a)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : α
h✝ : a = ⊤
⊢ Option.some a ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : α
h✝ : ¬a = ⊤
⊢ Option.some a ≤ ↑(succ a)
[PROOFSTEP]
exact some_le_some.2 (le_succ a)
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : WithTop α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      a ≤
    a
⊢ IsMax a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      none ≤
    none
⊢ IsMax none
[PROOFSTEP]
exact isMax_top
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
dsimp only at ha
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
ha : (if val✝ = ⊤ then ⊤ else ↑(succ val✝)) ≤ Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
split_ifs at ha  with ha'
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
ha' : val✝ = ⊤
ha : ⊤ ≤ Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
exact (not_top_le_coe _ ha).elim
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
ha' : ¬val✝ = ⊤
ha : ↑(succ val✝) ≤ Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
rw [some_eq_coe, coe_le_coe, succ_le_iff_eq_top] at ha
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
ha' : ¬val✝ = ⊤
ha✝ : succ val✝ ≤ val✝
ha : val✝ = ⊤
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
exact (ha' ha).elim
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a b : WithTop α
h : a < b
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      a ≤
    b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : WithTop α
h : a < none
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      a ≤
    none
[PROOFSTEP]
exact le_top
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a : WithTop α
val✝ : α
h : a < Option.some val✝
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      a ≤
    Option.some val✝
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
h : none < Option.some val✝
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      none ≤
    Option.some val✝
[PROOFSTEP]
exact (not_top_lt h).elim
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : Option.some val✝ < Option.some val✝¹
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝¹
[PROOFSTEP]
rw [some_lt_some] at h
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : val✝ < val✝¹
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝¹
[PROOFSTEP]
change ite _ _ _ ≤ _
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : val✝ < val✝¹
⊢ (if val✝ = ⊤ then ⊤ else ↑(succ val✝)) ≤ Option.some val✝¹
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : val✝ < val✝¹
ha : val✝ = ⊤
⊢ ⊤ ≤ Option.some val✝¹
[PROOFSTEP]
rw [ha] at h
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : ⊤ < val✝¹
ha : val✝ = ⊤
⊢ ⊤ ≤ Option.some val✝¹
[PROOFSTEP]
exact (not_top_lt h).elim
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : val✝ < val✝¹
ha : ¬val✝ = ⊤
⊢ ↑(succ val✝) ≤ Option.some val✝¹
[PROOFSTEP]
exact some_le_some.2 (succ_le_of_lt h)
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
a b : WithTop α
h :
  a <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      b
⊢ a ≤ b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
b : WithTop α
h :
  none <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      b
⊢ none ≤ b
[PROOFSTEP]
exact (not_top_lt h).elim
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
b : WithTop α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      b
⊢ Option.some val✝ ≤ b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      none
⊢ Option.some val✝ ≤ none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h :
  Option.some val✝¹ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => if a = ⊤ then ⊤ else ↑(succ a))
      (Option.some val✝)
⊢ Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
dsimp only at h
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : Option.some val✝¹ < if val✝ = ⊤ then ⊤ else ↑(succ val✝)
⊢ Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
rw [some_le_some]
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : Option.some val✝¹ < if val✝ = ⊤ then ⊤ else ↑(succ val✝)
⊢ val✝¹ ≤ val✝
[PROOFSTEP]
split_ifs at h  with hb
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
hb : val✝ = ⊤
h : Option.some val✝¹ < ⊤
⊢ val✝¹ ≤ val✝
[PROOFSTEP]
rw [hb]
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
hb : val✝ = ⊤
h : Option.some val✝¹ < ⊤
⊢ val✝¹ ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : SuccOrder α
val✝¹ val✝ : α
hb : ¬val✝ = ⊤
h : Option.some val✝¹ < ↑(succ val✝)
⊢ val✝¹ ≤ val✝
[PROOFSTEP]
exact le_of_lt_succ (some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha :
  a ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      a
⊢ IsMin a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha :
  none ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      none
⊢ IsMin none
[PROOFSTEP]
exact ((coe_lt_top (⊤ : α)).not_le ha).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
val✝ : α
ha :
  Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      (Option.some val✝)
⊢ IsMin (Option.some val✝)
[PROOFSTEP]
exact (min_of_le_pred <| some_le_some.1 ha).withTop
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : WithTop α
h : a < b
⊢ a ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
b : WithTop α
h : none < b
⊢ none ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      b
[PROOFSTEP]
exact (le_top.not_lt h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
b : WithTop α
val✝ : α
h : Option.some val✝ < b
⊢ Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
val✝ : α
h : Option.some val✝ < none
⊢ Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      none
[PROOFSTEP]
exact some_le_some.2 le_top
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : Option.some val✝¹ < Option.some val✝
⊢ Option.some val✝¹ ≤
    (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      (Option.some val✝)
[PROOFSTEP]
exact some_le_some.2 (le_pred_of_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : WithTop α
h :
  (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      a <
    b
⊢ a ≤ b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
h :
  (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      a <
    none
⊢ a ≤ none
[PROOFSTEP]
exact le_top
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      a <
    Option.some val✝
⊢ a ≤ Option.some val✝
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      none <
    Option.some val✝
⊢ none ≤ Option.some val✝
[PROOFSTEP]
exact (not_top_lt <| some_lt_some.1 h).elim
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
val✝¹ val✝ : α
h :
  (fun a =>
        match a with
        | none => ↑⊤
        | Option.some a => ↑(pred a))
      (Option.some val✝) <
    Option.some val✝¹
⊢ Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
exact some_le_some.2 (le_of_pred_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha : a ≠ ⊤
⊢ pred a ≠ ⊤
[PROOFSTEP]
induction a using WithTop.recTopCoe
[GOAL]
case top
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha : ⊤ ≠ ⊤
⊢ pred ⊤ ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
case coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha : ↑a✝ ≠ ⊤
⊢ pred ↑a✝ ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
a : WithTop α
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      a
[PROOFSTEP]
cases' a with a a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
⊢ none ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      none
[PROOFSTEP]
exact le_top
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
a : α
⊢ Option.some a ≤
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some a)
[PROOFSTEP]
exact some_le_some.2 (le_succ a)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
a : WithTop α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      a ≤
    a
⊢ IsMax a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      none ≤
    none
⊢ IsMax none
[PROOFSTEP]
exact isMax_top
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
val✝ : α
ha :
  (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
exact (not_isMax _ <| max_of_succ_le <| some_le_some.1 ha).elim
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
a b : WithTop α
h : a < b
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      a ≤
    b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
b : WithTop α
h : none < b
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      none ≤
    b
[PROOFSTEP]
exact (not_top_lt h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
b : WithTop α
val✝ : α
h : Option.some val✝ < b
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some val✝) ≤
    b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
val✝ : α
h : Option.some val✝ < none
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some val✝) ≤
    none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : Option.some val✝¹ < Option.some val✝
⊢ (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some val✝¹) ≤
    Option.some val✝
[PROOFSTEP]
exact some_le_some.2 (succ_le_of_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
a b : WithTop α
h :
  a <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      b
⊢ a ≤ b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
b : WithTop α
h :
  none <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      b
⊢ none ≤ b
[PROOFSTEP]
exact (not_top_lt h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
b : WithTop α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      b
⊢ Option.some val✝ ≤ b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      none
⊢ Option.some val✝ ≤ none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h :
  Option.some val✝¹ <
    (fun a =>
        match a with
        | none => ⊤
        | Option.some a => ↑(succ a))
      (Option.some val✝)
⊢ Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
exact some_le_some.2 (le_of_lt_succ <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
⊢ PredOrder (WithTop α) → False
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
⊢ False
[PROOFSTEP]
cases' h : pred (⊤ : WithTop α) with a ha
[GOAL]
case none
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
h : pred ⊤ = none
⊢ False
[PROOFSTEP]
exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a
[GOAL]
case some
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = Option.some a
⊢ False
[PROOFSTEP]
obtain ⟨c, hc⟩ := exists_gt a
[GOAL]
case some.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = Option.some a
c : α
hc : a < c
⊢ False
[PROOFSTEP]
rw [← some_lt_some, ← h] at hc
[GOAL]
case some.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = Option.some a
c : α
hc : pred ⊤ < Option.some c
⊢ False
[PROOFSTEP]
exact (le_of_pred_lt hc).not_lt (some_lt_none _)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
ha :
  (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      a ≤
    a
⊢ IsMax a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
ha :
  (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      none ≤
    none
⊢ IsMax none
[PROOFSTEP]
exact ((none_lt_some (⊥ : α)).not_le ha).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
val✝ : α
ha :
  (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝
⊢ IsMax (Option.some val✝)
[PROOFSTEP]
exact (max_of_succ_le <| some_le_some.1 ha).withBot
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a b : WithBot α
h : a < b
⊢ (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      a ≤
    b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
h : a < none
⊢ (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      a ≤
    none
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
val✝ : α
h : a < Option.some val✝
⊢ (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      a ≤
    Option.some val✝
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
val✝ : α
h : none < Option.some val✝
⊢ (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      none ≤
    Option.some val✝
[PROOFSTEP]
exact some_le_some.2 bot_le
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h : Option.some val✝ < Option.some val✝¹
⊢ (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      (Option.some val✝) ≤
    Option.some val✝¹
[PROOFSTEP]
exact some_le_some.2 (succ_le_of_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a b : WithBot α
h :
  a <
    (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      b
⊢ a ≤ b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
b : WithBot α
h :
  none <
    (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      b
⊢ none ≤ b
[PROOFSTEP]
exact bot_le
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
b : WithBot α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      b
⊢ Option.some val✝ ≤ b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
val✝ : α
h :
  Option.some val✝ <
    (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      none
⊢ Option.some val✝ ≤ none
[PROOFSTEP]
exact (not_lt_bot <| some_lt_some.1 h).elim
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
val✝¹ val✝ : α
h :
  Option.some val✝¹ <
    (fun a =>
        match a with
        | none => ↑⊥
        | Option.some a => ↑(succ a))
      (Option.some val✝)
⊢ Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
exact some_le_some.2 (le_of_lt_succ <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
ha : a ≠ ⊥
⊢ succ a ≠ ⊥
[PROOFSTEP]
induction a using WithBot.recBotCoe
[GOAL]
case bot
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
ha : ⊥ ≠ ⊥
⊢ succ ⊥ ≠ ⊥
[PROOFSTEP]
simp
[GOAL]
case coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
ha : ↑a✝ ≠ ⊥
⊢ succ ↑a✝ ≠ ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : WithBot α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      a ≤
    a
[PROOFSTEP]
cases' a with a a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      none ≤
    none
[PROOFSTEP]
exact bot_le
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      (Option.some a) ≤
    Option.some a
[PROOFSTEP]
change ite _ _ _ ≤ _
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
⊢ (if a = ⊥ then ⊥ else ↑(pred a)) ≤ Option.some a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
h✝ : a = ⊥
⊢ ⊥ ≤ Option.some a
[PROOFSTEP]
exact bot_le
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
h✝ : ¬a = ⊥
⊢ ↑(pred a) ≤ Option.some a
[PROOFSTEP]
exact some_le_some.2 (pred_le a)
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : WithBot α
ha :
  a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      a
⊢ IsMin a
[PROOFSTEP]
cases' a with a a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
ha :
  none ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      none
⊢ IsMin none
[PROOFSTEP]
exact isMin_bot
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
ha :
  Option.some a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      (Option.some a)
⊢ IsMin (Option.some a)
[PROOFSTEP]
dsimp only at ha
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
ha : Option.some a ≤ if a = ⊥ then ⊥ else ↑(pred a)
⊢ IsMin (Option.some a)
[PROOFSTEP]
split_ifs at ha  with ha'
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
ha' : a = ⊥
ha : Option.some a ≤ ⊥
⊢ IsMin (Option.some a)
[PROOFSTEP]
exact (not_coe_le_bot _ ha).elim
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
ha' : ¬a = ⊥
ha : Option.some a ≤ ↑(pred a)
⊢ IsMin (Option.some a)
[PROOFSTEP]
rw [some_eq_coe, coe_le_coe, le_pred_iff_eq_bot] at ha
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : α
ha' : ¬a = ⊥
ha✝ : a ≤ pred a
ha : a = ⊥
⊢ IsMin (Option.some a)
[PROOFSTEP]
exact (ha' ha).elim
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a b : WithBot α
h : a < b
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
b : WithBot α
h : none < b
⊢ none ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      b
[PROOFSTEP]
exact bot_le
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
b : WithBot α
val✝ : α
h : Option.some val✝ < b
⊢ Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      b
[PROOFSTEP]
cases b
[GOAL]
case some.none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝ : α
h : Option.some val✝ < none
⊢ Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      none
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : Option.some val✝¹ < Option.some val✝
⊢ Option.some val✝¹ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      (Option.some val✝)
[PROOFSTEP]
rw [some_lt_some] at h
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : val✝¹ < val✝
⊢ Option.some val✝¹ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      (Option.some val✝)
[PROOFSTEP]
change _ ≤ ite _ _ _
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : val✝¹ < val✝
⊢ Option.some val✝¹ ≤ if val✝ = ⊥ then ⊥ else ↑(pred val✝)
[PROOFSTEP]
split_ifs with hb
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : val✝¹ < val✝
hb : val✝ = ⊥
⊢ Option.some val✝¹ ≤ ⊥
[PROOFSTEP]
rw [hb] at h
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : val✝¹ < ⊥
hb : val✝ = ⊥
⊢ Option.some val✝¹ ≤ ⊥
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : val✝¹ < val✝
hb : ¬val✝ = ⊥
⊢ Option.some val✝¹ ≤ ↑(pred val✝)
[PROOFSTEP]
exact some_le_some.2 (le_pred_of_lt h)
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a b : WithBot α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      a <
    b
⊢ a ≤ b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : WithBot α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      a <
    none
⊢ a ≤ none
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
a : WithBot α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      a <
    Option.some val✝
⊢ a ≤ Option.some val✝
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      none <
    Option.some val✝
⊢ none ≤ Option.some val✝
[PROOFSTEP]
exact bot_le
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => if a = ⊥ then ⊥ else ↑(pred a))
      (Option.some val✝) <
    Option.some val✝¹
⊢ Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
dsimp only at h
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : (if val✝ = ⊥ then ⊥ else ↑(pred val✝)) < Option.some val✝¹
⊢ Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
rw [some_le_some]
[GOAL]
case some.some
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : (if val✝ = ⊥ then ⊥ else ↑(pred val✝)) < Option.some val✝¹
⊢ val✝ ≤ val✝¹
[PROOFSTEP]
split_ifs at h  with ha
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
ha : val✝ = ⊥
h : ⊥ < Option.some val✝¹
⊢ val✝ ≤ val✝¹
[PROOFSTEP]
rw [ha]
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
ha : val✝ = ⊥
h : ⊥ < Option.some val✝¹
⊢ ⊥ ≤ val✝¹
[PROOFSTEP]
exact bot_le
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : PredOrder α
val✝¹ val✝ : α
ha : ¬val✝ = ⊥
h : ↑(pred val✝) < Option.some val✝¹
⊢ val✝ ≤ val✝¹
[PROOFSTEP]
exact le_of_pred_lt (some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
⊢ SuccOrder (WithBot α) → False
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
a✝ : SuccOrder (WithBot α)
⊢ False
[PROOFSTEP]
cases' h : succ (⊥ : WithBot α) with a ha
[GOAL]
case none
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
a✝ : SuccOrder (WithBot α)
h : succ ⊥ = none
⊢ False
[PROOFSTEP]
exact hα.elim fun a => (max_of_succ_le h.le).not_lt <| bot_lt_coe a
[GOAL]
case some
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
a✝ : SuccOrder (WithBot α)
a : α
h : succ ⊥ = Option.some a
⊢ False
[PROOFSTEP]
obtain ⟨c, hc⟩ := exists_lt a
[GOAL]
case some.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
a✝ : SuccOrder (WithBot α)
a : α
h : succ ⊥ = Option.some a
c : α
hc : c < a
⊢ False
[PROOFSTEP]
rw [← some_lt_some, ← h] at hc
[GOAL]
case some.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
hα : Nonempty α
a✝ : SuccOrder (WithBot α)
a : α
h : succ ⊥ = Option.some a
c : α
hc : Option.some c < succ ⊥
⊢ False
[PROOFSTEP]
exact (le_of_lt_succ hc).not_lt (none_lt_some _)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      a ≤
    a
[PROOFSTEP]
cases' a with a a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      none ≤
    none
[PROOFSTEP]
exact bot_le
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : α
⊢ (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some a) ≤
    Option.some a
[PROOFSTEP]
exact some_le_some.2 (pred_le a)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
ha :
  a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      a
⊢ IsMin a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
ha :
  none ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      none
⊢ IsMin none
[PROOFSTEP]
exact isMin_bot
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
val✝ : α
ha :
  Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some val✝)
⊢ IsMin (Option.some val✝)
[PROOFSTEP]
exact (not_isMin _ <| min_of_le_pred <| some_le_some.1 ha).elim
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a b : WithBot α
h : a < b
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
h : a < none
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      none
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
val✝ : α
h : a < Option.some val✝
⊢ a ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some val✝)
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
val✝ : α
h : none < Option.some val✝
⊢ none ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some val✝)
[PROOFSTEP]
exact bot_le
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
val✝¹ val✝ : α
h : Option.some val✝ < Option.some val✝¹
⊢ Option.some val✝ ≤
    (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some val✝¹)
[PROOFSTEP]
exact some_le_some.2 (le_pred_of_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a b : WithBot α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      a <
    b
⊢ a ≤ b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      a <
    none
⊢ a ≤ none
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
a : WithBot α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      a <
    Option.some val✝
⊢ a ≤ Option.some val✝
[PROOFSTEP]
cases a
[GOAL]
case some.none
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      none <
    Option.some val✝
⊢ none ≤ Option.some val✝
[PROOFSTEP]
exact bot_le
[GOAL]
case some.some
α : Type u_1
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : PredOrder α
val✝¹ val✝ : α
h :
  (fun a =>
        match a with
        | none => ⊥
        | Option.some a => ↑(pred a))
      (Option.some val✝) <
    Option.some val✝¹
⊢ Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
exact some_le_some.2 (le_of_pred_lt <| some_lt_some.1 h)
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a✝ b✝ : α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
convert exists_succ_iterate_of_le h.ofDual
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b
[PROOFSTEP]
refine' ⟨_, exists_succ_iterate_of_le⟩
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) → a ≤ b
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a
[PROOFSTEP]
exact id_le_iterate_of_id_le le_succ n a
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : α
hmn : m ≤ n
⊢ P n
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
hmn : m ≤ succ^[n] m
⊢ P (succ^[n] m)
[PROOFSTEP]
clear hmn
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
⊢ P (succ^[n] m)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case intro.zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
⊢ P (succ^[Nat.zero] m)
[PROOFSTEP]
exact h0
[GOAL]
case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ^[Nat.succ n] m)
[PROOFSTEP]
rw [Function.iterate_succ_apply']
[GOAL]
case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ (succ^[n] m))
[PROOFSTEP]
exact h1 _ (id_le_iterate_of_id_le le_succ n m) ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a✝ b✝ : α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
⊢ p a ↔ p b
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h.exists_succ_iterate
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a✝ b : α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)
[PROOFSTEP]
exact Iterate.rec (fun b => p a ↔ p b) (fun c hc => hc.trans (hsucc _)) Iff.rfl n
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a✝ b✝ : α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, succ^[n] a = b
[PROOFSTEP]
convert exists_pred_iterate_of_le h.ofDual
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b : α
⊢ a ≤ b → ∃ n, pred^[n] b = a
[PROOFSTEP]
refine' WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a) h.wf _ b
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b : α
⊢ ∀ (x : α), (∀ (y : α), y < x → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y) → (fun b => a ≤ b → ∃ n, pred^[n] b = a) x
[PROOFSTEP]
intros b ih hab
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
hab : a ≤ b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
replace hab := eq_or_lt_of_le hab
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
hab : a = b ∨ a < b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
rcases hab with (rfl | hab)
[GOAL]
case inl
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b : α
ih : ∀ (y : α), y < a → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
⊢ ∃ n, pred^[n] a = a
[PROOFSTEP]
exact ⟨0, rfl⟩
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
hab : a < b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
cases' le_or_lt b (pred b) with hb hb
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
hab : a < b
hb : b ≤ pred b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
cases (min_of_le_pred hb).not_lt hab
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → (fun b => a ≤ b → ∃ n, pred^[n] b = a) y
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
dsimp at ih
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)
[GOAL]
case inr.inr.intro
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ ∃ n, pred^[n] b = a
[PROOFSTEP]
refine' ⟨k + 1, _⟩
[GOAL]
case inr.inr.intro
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x < x_1
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ (y : α), y < b → a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k + 1] b = a
[PROOFSTEP]
rw [iterate_add_apply, iterate_one, hk]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
h : IsWellOrder α fun x x_1 => x > x_1
inst✝ : SuccOrder α
⊢ IsPredArchimedean αᵒᵈ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)
[PROOFSTEP]
refine' ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ _⟩
[GOAL]
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
i : α
hi : i ≠ ⊥
⊢ P i
[PROOFSTEP]
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
[GOAL]
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ P (Order.succ^[j] ⊥)
[PROOFSTEP]
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
[GOAL]
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ 0 < j
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ j ≠ 0
[PROOFSTEP]
contrapose! hi
[GOAL]
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : j = 0
⊢ Order.succ^[j] ⊥ = ⊥
[PROOFSTEP]
simp [hi]
[GOAL]
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos hj]
[GOAL]
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[Nat.succ (Nat.pred j)] ⊥)
[PROOFSTEP]
simp only [Function.iterate_succ', Function.comp_apply]
[GOAL]
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ (Order.succ^[Nat.pred j] ⊥))
[PROOFSTEP]
apply h