mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (prelimitRecOn b succ isSuccPrelimit)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a = succ b ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ limitRecOn b isMin succ isSuccLimit = isMin b hb

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
⊢ ¬IsMin (succ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∀ x ∈ S, x ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ x + 1 ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : ¬IsMax x
⊢ x + 1 ≤ y ↔ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a : ℕ
ha : a ≤ a.pred
⊢ IsMin a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a < b
⊢ a ≤ b.pred

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: a n : ℕ
⊢ pred^[n + 1] a = a - (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hy : ¬IsMax y
⊢ x + 1 ≤ y ↔ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
⊢ ∃ x, IsGreatest S x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ x + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ x + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a < succ b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ y - 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ a < succ b ↔ b = a ∨ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ y - 1 ↔ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
x : α
⊢ x - 1 ⩿ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ x - 1 ⋖ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
x : α
this : a < x → b ≤ x
⊢ x ∈ Ioo a b ↔ x ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a < succ ⊥ ↔ a = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
⊢ ∀ (a b : SuccOrder α), a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
⊢ pred^[n] x = x - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ¬IsMax 0

Tactic:
rw [not_isMax_iff]

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ∃ b, 0 < b
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ¬IsMax 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ x ↔ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : NeZero 1
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
⊢ 1 ≤ x ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ x + 1 = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ y - 1 = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + 1 < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + ↑0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = ⨅ b, ⨅ (_ : b > a), b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑(n + 1) < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : ⟨b, hb⟩ ≤ ⟨c, hc⟩
⊢ ∃ n, pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : PartialOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
hx : IsSuccLimit x
⊢ ∀ (n : ℕ), ↑n < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : WithBot α
⊢ a.succ = 0 ↔ a = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y + 1
⊢ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hy : ¬IsMax y
⊢ x < y + 1 ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hy : ¬IsMax y
⊢ x < y + 1 ↔ x ≤ y

Tactic:
by
  rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : ¬IsMax x
⊢ x < y + 1 ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : LinearOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x + 1 = y + 1 ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x < 2 ↔ x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ x < 1 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ x ≤ 1 ↔ x = 0 ∨ x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ Set.Iio 1 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ Set.Iic 1 = {0, 1}

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ succ^[n.succ] i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iio 2 = {0, 1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iic 2 = {0, 1, 2}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x - 1 < y
⊢ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ x - 1 < y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ ¬IsMax (succ^[n - 1] i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ x < 1 ↔ x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
⊢ MonotoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hin : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a ≤ f (a + 1)) → Monotone f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) ≤ f a) → Antitone f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a < f (a + 1)) → StrictMono f

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
⊢ a ≤
    match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) < f a) → StrictAnti f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    a
⊢ IsMax a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Tactic:
by

Goal state after: