awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Zero α
inst_2 : One α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
rw : ∃ (b : α), 0 < b
⊢ ¬IsMax.{u_1} (α := α) 0

Tactic:
rw [not_isMax_iff]

Premises used: not_isMax_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Zero α
inst_2 : One α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ ∃ (b : α), 0 < b

Tactic:
⟨1, one_pos⟩

Premises used: Exists.intro, OfNat.ofNat, one_pos
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Zero α
inst_2 : One α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ ∃ (b : α), 0 < b

Tactic:
exact ⟨1, one_pos⟩
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : 1 ≤ x ↔ succ 0 ≤ x
rw₁ : 1 ≤ x ↔ HAdd.hAdd (α := α) 0 1 ≤ x
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ 1 ≤ x ↔ 0 < x

Tactic:
rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Premises used: Order.succ_eq_add_one, Order.succ_le_iff_of_not_isMax, Order.not_isMax_zero, zero_add
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NeZero.{u_1} (R := α) 1
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : 0 < x ↔ x ≠ 0
rw₁ rw₂ : x ≠ 0 ↔ x ≠ 0
⊢ 1 ≤ x ↔ x ≠ 0

Tactic:
rw [Order.one_le_iff_pos, pos_iff_ne_zero]

Premises used: pos_iff_ne_zero, Order.one_le_iff_pos
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
rw : x ⋖ y ↔ succ x = y
⊢ x ⋖ y ↔ x + 1 = y

Tactic:
rw [← succ_eq_add_one]

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ x ⋖ y ↔ succ x = y

Tactic:
succ_eq_iff_covBy.symm

Premises used: Order.succ_eq_iff_covBy, Iff.symm
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ x ⋖ y ↔ succ x = y

Tactic:
exact succ_eq_iff_covBy.symm

Premises used: Order.succ_eq_iff_covBy, Iff.symm
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
rw : x ⋖ y ↔ pred y = x
⊢ x ⋖ y ↔ y - 1 = x

Tactic:
rw [← pred_eq_sub_one]

Premises used: Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
⊢ x ⋖ y ↔ pred y = x

Tactic:
pred_eq_iff_covBy.symm

Premises used: Order.pred_eq_iff_covBy, Iff.symm
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
⊢ x ⋖ y ↔ pred y = x

Tactic:
exact pred_eq_iff_covBy.symm

Premises used: Order.pred_eq_iff_covBy, Iff.symm
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
rw : succ y < x
⊢ y + 1 < x

Tactic:
rw [← succ_eq_add_one]

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x

Tactic:
hx.succ_lt hy

Premises used: Order.IsSuccPrelimit.succ_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x

Tactic:
exact hx.succ_lt hy

Premises used: Order.IsSuccPrelimit.succ_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
rw : x < pred y
⊢ x < y - 1

Tactic:
rw [← pred_eq_sub_one]

Premises used: Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < pred y

Tactic:
hx.lt_pred hy

Premises used: Order.IsPredPrelimit.lt_pred
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < pred y

Tactic:
exact hx.lt_pred hy

Premises used: Order.IsPredPrelimit.lt_pred
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : IsSuccLimit x
hy : y < x
⊢ y + 1 < x

Tactic:
hx.isSuccPrelimit.add_one_lt hy

Premises used: Order.IsSuccPrelimit.add_one_lt, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : IsPredLimit x
hy : x < y
⊢ x < y - 1

Tactic:
hx.isPredPrelimit.lt_sub_one hy

Premises used: Order.IsPredLimit.isPredPrelimit, Order.IsPredPrelimit.lt_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + (↑0 : α) < x

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
rw : y + (↑n : α) + 1 < x
⊢ y + (↑(n + 1) : α) < x

Tactic:
rw [Nat.cast_add_one, ← add_assoc]

Premises used: add_assoc, Nat.cast_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + (↑n : α) + 1 < x

Tactic:
hx.add_one_lt (hx.add_natCast_lt hy n)

Premises used: Order.IsSuccPrelimit.add_one_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + (↑n : α) + 1 < x

Tactic:
exact hx.add_one_lt (hx.add_natCast_lt hy n)

Premises used: Order.IsSuccPrelimit.add_one_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - (↑0 : α)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
rw : x < y - (↑n : α) - 1
⊢ x < y - (↑(n + 1) : α)

Tactic:
rw [Nat.cast_add_one, ← sub_sub]

Premises used: sub_sub, Nat.cast_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - (↑n : α) - 1

Tactic:
hx.lt_sub_one (hx.lt_sub_natCast hy n)

Premises used: Order.IsPredPrelimit.lt_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - (↑n : α) - 1

Tactic:
exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

Premises used: Order.IsPredPrelimit.lt_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccLimit x
hy : y < x
⊢ ∀ (n : ℕ), y + (↑n : α) < x

Tactic:
hx.isSuccPrelimit.add_natCast_lt hy

Premises used: Order.IsSuccPrelimit.add_natCast_lt, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredLimit x
hy : x < y
⊢ ∀ (n : ℕ), x < y - (↑n : α)

Tactic:
hx.isPredPrelimit.lt_sub_natCast hy

Premises used: Order.IsPredLimit.isPredPrelimit, Order.IsPredPrelimit.lt_sub_natCast
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
inst_3 : IsBotZeroClass α
hx : IsSuccLimit x
⊢ ∀ (n : ℕ), (↑n : α) < x

Tactic:
simpa using hx.add_natCast_lt hx.pos

Premises used: Order.IsSuccLimit.add_natCast_lt, Order.IsSuccLimit.pos
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
inst_3 : IsBotZeroClass α
n : ℕ
⊢ ¬IsSuccLimit.{u_1} (α := α) (↑n : α)

Tactic:
fun h ↦ (h.natCast_lt n).false

Premises used: Order.IsSuccLimit.natCast_lt, LT.lt.false, Not
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ ¬IsSuccPrelimit (a + 1)

Tactic:
succ_eq_add_one a ▸ not_isSuccPrelimit_succ a

Premises used: Order.succ_eq_add_one, Eq.rec, Order.not_isSuccPrelimit_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ ¬IsSuccLimit (a + 1)

Tactic:
succ_eq_add_one a ▸ not_isSuccLimit_succ a

Premises used: Order.succ_eq_add_one, Eq.rec, Order.not_isSuccLimit_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : WithBot α
bot : Eq.{u_1 + 1} (α := α) (WithBot.succ ⊥) 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
coe : ∀ (a : α), (↑a : WithBot α).succ = 0 ↔ (↑a : WithBot α) = ⊥
⊢ a.succ = 0 ↔ a = ⊥

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
⊢ Eq.{u_1 + 1} (α := α) (WithBot.succ ⊥) 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [bot_eq_zero]

Premises used: bot_eq_zero
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : α
coe : ¬a + 1 = 0
⊢ (↑a : WithBot α).succ = 0 ↔ (↑a : WithBot α) = ⊥

Tactic:
simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false, succ_eq_add_one]

Premises used: Order.succ_eq_add_one, iff_false, WithBot.succ_coe, WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : α
coe : ∀ (h : a + 1 = 0), False
⊢ ¬a + 1 = 0

Tactic:
by_contra h
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : α
h : a + 1 = 0
⊢ False

Tactic:
simpa [h] using max_of_succ_le (a := a)

Premises used: Order.max_of_succ_le
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < y + 1
⊢ x < succ y

Tactic:
rw [← succ_eq_add_one] at h

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < succ y
⊢ x ≤ y

Tactic:
le_of_lt_succ h

Premises used: Order.le_of_lt_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < succ y
⊢ x ≤ y

Tactic:
exact le_of_lt_succ h

Premises used: Order.le_of_lt_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hy : ¬IsMax y
rw : x < succ y ↔ x ≤ y
rw₁ rw₂ : x ≤ y ↔ x ≤ y
⊢ x < y + 1 ↔ x ≤ y

Tactic:
rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]

Premises used: Order.succ_eq_add_one, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ x < y + 1 ↔ x ≤ y

Tactic:
lt_add_one_iff_of_not_isMax (not_isMax y)

Premises used: not_isMax, Order.lt_add_one_iff_of_not_isMax
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ x + 1 = y + 1 ↔ x = y

Tactic:
simp [← succ_eq_add_one]

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < HAdd.hAdd (α := α) 0 1 ↔ x = 0
rw₁ : x ≤ 0 ↔ x = 0
rw₂ rw₃ : x = 0 ↔ x = 0
⊢ x < 1 ↔ x = 0

Tactic:
rw [← zero_add 1, lt_add_one_iff, nonpos_iff_eq_zero]

Premises used: zero_add, Order.lt_add_one_iff, OfNat.ofNat, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 1 ∨ x = 1 ↔ x = 0 ∨ x = 1
rw₁ rw₂ : x = 0 ∨ x = 1 ↔ x = 0 ∨ x = 1
⊢ x ≤ 1 ↔ x = 0 ∨ x = 1

Tactic:
rw [le_iff_lt_or_eq, lt_one_iff]

Premises used: le_iff_lt_or_eq, Order.lt_one_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iio 1) x ↔ Membership.mem (γ := Set α) {0} x
⊢ Eq (α := Set α) (Set.Iio 1) {0}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
x : α
⊢ Membership.mem (γ := Set α) (Set.Iio 1) x ↔ Membership.mem (γ := Set α) {0} x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iic 1) x ↔ Membership.mem (γ := Set α) {0, 1} x
⊢ Eq (α := Set α) (Set.Iic 1) {0, 1}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
x : α
⊢ Membership.mem (γ := Set α) (Set.Iic 1) x ↔ Membership.mem (γ := Set α) {0, 1} x

Tactic:
simp [le_one_iff]

Premises used: Order.le_one_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
rw : x < HAdd.hAdd (α := α) 1 1 ↔ x ≤ 1
rw₁ rw₂ : x ≤ 1 ↔ x ≤ 1
⊢ x < 2 ↔ x ≤ 1

Tactic:
rw [← one_add_one_eq_two, lt_add_one_iff]

Premises used: one_add_one_eq_two, Order.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₁ : x ≤ 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₂ : (x = 0 ∨ x = 1) ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₃ rw₄ : x = 0 ∨ x = 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]

Premises used: Order.lt_two_iff, le_iff_lt_or_eq, Order.le_one_iff, or_assoc
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iio 2) x ↔ Membership.mem (γ := Set α) {0, 1} x
⊢ Eq (α := Set α) (Set.Iio 2) {0, 1}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
x : α
⊢ Membership.mem (γ := Set α) (Set.Iio 2) x ↔ Membership.mem (γ := Set α) {0, 1} x

Tactic:
simp [le_one_iff]

Premises used: Order.le_one_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iic 2) x ↔ Membership.mem (γ := Set α) {0, 1, 2} x
⊢ Eq (α := Set α) (Set.Iic 2) {0, 1, 2}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
x : α
⊢ Membership.mem (γ := Set α) (Set.Iic 2) x ↔ Membership.mem (γ := Set α) {0, 1, 2} x

Tactic:
simp [le_two_iff]

Premises used: Order.le_two_iff
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : x - 1 < y
⊢ pred x < y

Tactic:
rw [← pred_eq_sub_one] at h

Premises used: Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : pred x < y
⊢ x ≤ y

Tactic:
le_of_pred_lt h

Premises used: Order.le_of_pred_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : pred x < y
⊢ x ≤ y

Tactic:
exact le_of_pred_lt h

Premises used: Order.le_of_pred_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : ¬IsMin x
rw : pred x < y ↔ x ≤ y
rw₁ rw₂ : x ≤ y ↔ x ≤ y
⊢ x - 1 < y ↔ x ≤ y

Tactic:
rw [← pred_eq_sub_one, pred_lt_iff_of_not_isMin hx]

Premises used: Order.pred_eq_sub_one, Order.pred_lt_iff_of_not_isMin
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
⊢ x - 1 < y ↔ x ≤ y

Tactic:
sub_one_lt_iff_of_not_isMin (not_isMin x)

Premises used: not_isMin, Order.sub_one_lt_iff_of_not_isMin
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : x < 1 ↔ x < succ 0
rw₁ : x < 1 ↔ x < HAdd.hAdd (α := α) 0 1
rw₂ rw₃ : x < 1 ↔ x < 1
⊢ x < 1 ↔ x ≤ 0

Tactic:
rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Premises used: Order.succ_eq_add_one, Order.not_isMax_zero, zero_add, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)

Premises used: Order.succ_eq_add_one, monotoneOn_of_le_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

Premises used: Order.succ_eq_add_one, antitoneOn_of_succ_le
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Tactic:
simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)

Premises used: Order.succ_eq_add_one, strictMonoOn_of_lt_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s

Tactic:
simpa [Order.succ_eq_add_one] using strictAntiOn_of_succ_lt hs (f := f)

Premises used: Order.succ_eq_add_one, strictAntiOn_of_succ_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a ≤ f (a + 1)) → Monotone f

Tactic:
simpa [Order.succ_eq_add_one] using monotone_of_le_succ (f := f)

Premises used: Order.succ_eq_add_one, monotone_of_le_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) ≤ f a) → Antitone f

Tactic:
simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)

Premises used: Order.succ_eq_add_one, antitone_of_succ_le
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a < f (a + 1)) → StrictMono f

Tactic:
simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)

Premises used: Order.succ_eq_add_one, strictMono_of_lt_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Add α
inst_3 : One α
inst_4 : SuccAddOrder α
inst_5 : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) < f a) → StrictAnti f

Tactic:
simpa [Order.succ_eq_add_one] using strictAnti_of_succ_lt (f := f)

Premises used: Order.succ_eq_add_one, strictAnti_of_succ_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using monotoneOn_of_pred_le hs (f := f)

Premises used: Order.pred_eq_sub_one, monotoneOn_of_pred_le
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)

Premises used: antitoneOn_of_le_pred, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using strictMonoOn_of_pred_lt hs (f := f)

Premises used: Order.pred_eq_sub_one, strictMonoOn_of_pred_lt