awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a b : WithTop α
⊢ a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Tactic:
simp [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Sub α
inst_1 : Bot α
inst_2 : Sub β
inst_3 : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x : WithTop α
⊢ map f (x - ⊤) = map f x - map f ⊤

Tactic:
simp only [sub_top, map_coe, h₀, map_top]

Premises used: WithTop.map_top, WithTop.map_coe, WithTop.sub_top
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Sub α
inst_1 : Bot α
inst_2 : Sub β
inst_3 : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x y : α
⊢ map f ((↑x : WithTop α) - (↑y : WithTop α)) = map f (↑x : WithTop α) - map f (↑y : WithTop α)

Tactic:
simp only [← coe_sub, map_coe, h]

Premises used: WithTop.coe_sub, WithTop.map_coe
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
tsub_le_iff_right : ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b
⊢ OrderedSub.{u_1} (WithTop α)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x y z : WithTop α
tsub_le_iff_right : x - ⊤ ≤ z ↔ x ≤ z + ⊤
tsub_le_iff_right₁ : ∀ (a : α), x - (↑a : WithTop α) ≤ z ↔ x ≤ z + (↑a : WithTop α)
⊢ x - y ≤ z ↔ x ≤ z + y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
tsub_le_iff_right : x - ⊤ ≤ ⊤ ↔ x ≤ HAdd.hAdd (α := WithTop α) ⊤ ⊤
tsub_le_iff_right₁ : ∀ (a : α), x - ⊤ ≤ (↑a : WithTop α) ↔ x ≤ (↑a : WithTop α) + ⊤
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x : WithTop α
⊢ x - ⊤ ≤ ⊤ ↔ x ≤ HAdd.hAdd (α := WithTop α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x : WithTop α
a : α
⊢ x - ⊤ ≤ (↑a : WithTop α) ↔ x ≤ (↑a : WithTop α) + ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
a : α
tsub_le_iff_right : ⊤ - (↑a : WithTop α) ≤ z ↔ ⊤ ≤ z + (↑a : WithTop α)
tsub_le_iff_right₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ z ↔ (↑a_1 : WithTop α) ≤ z + (↑a : WithTop α)
⊢ x - (↑a : WithTop α) ≤ z ↔ x ≤ z + (↑a : WithTop α)

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
z : WithTop α
a : α
⊢ ⊤ - (↑a : WithTop α) ≤ z ↔ ⊤ ≤ z + (↑a : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
z : WithTop α
a a_1 : α
tsub_le_iff_right : (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ ⊤ ↔ (↑a_1 : WithTop α) ≤ ⊤ + (↑a : WithTop α)
tsub_le_iff_right₁ :
  ∀ (a_2 : α),
    (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ (↑a_2 : WithTop α) ↔
      (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) + (↑a : WithTop α)
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ z ↔ (↑a_1 : WithTop α) ≤ z + (↑a : WithTop α)

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
a a_1 : α
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ ⊤ ↔ (↑a_1 : WithTop α) ≤ ⊤ + (↑a : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
a a_1 a_2 : α
tsub_le_iff_right : a_1 - a ≤ a_2 ↔ a_1 ≤ a_2 + a
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ (↑a_2 : WithTop α) ↔
    (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) + (↑a : WithTop α)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
a a_1 a_2 : α
⊢ a_1 - a ≤ a_2 ↔ a_1 ≤ a_2 + a

Tactic:
tsub_le_iff_right

Premises used: tsub_le_iff_right
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
a a_1 a_2 : α
⊢ a_1 - a ≤ a_2 ↔ a_1 ≤ a_2 + a

Tactic:
exact tsub_le_iff_right

Premises used: tsub_le_iff_right
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : Add ι
inst_3 : One ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α) ((partialSups f : (a : ι) → α) i ⊔ f (i + 1) : α)

Tactic:
Order.succ_eq_add_one i ▸ partialSups_succ f i

Premises used: Order.succ_eq_add_one, Eq.rec, partialSups_succ
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i : ι
⊢ (partialSups f : (a : ι) → α) (Order.succ ⊥) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i : ι
refine :
  ∀ (j : ι),
    ⊥ ≤ j →
      ∀ (h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j),
        (partialSups f : (a : ι) → α) (Order.succ (Order.succ j)) =
          f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j)
⊢ (partialSups f : (a : ι) → α) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) i

Tactic:
refine Succ.rec (by simp) (fun j _ h ↦ ?_) (bot_le (a := i))
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i j : ι
h_1 : ⊥ ≤ j
h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j
⊢ Eq.{u_3 + 1} (α := α) ((partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j) : α)
    ((partialSups (f ∘ Order.succ) : (a : ι) → α) j ⊔ (f ∘ Order.succ) (Order.succ j) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i j : ι
h_1 : ⊥ ≤ j
h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j
⊢ Eq.{u_3 + 1} (α := α) ((partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j) : α)
    ((partialSups (f ∘ Order.succ) : (a : ι) → α) j ⊔ (f ∘ Order.succ) (Order.succ j) : α)

Tactic:
have : (partialSups (f ∘ Order.succ)) (Order.succ j) =
      ((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) := by simp
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i j : ι
h_1 : ⊥ ≤ j
h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j
this :
  Eq.{u_3 + 1} (α := α) ((partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j) : α)
    ((partialSups (f ∘ Order.succ) : (a : ι) → α) j ⊔ (f ∘ Order.succ) (Order.succ j) : α)
⊢ (partialSups f : (a : ι) → α) (Order.succ (Order.succ j)) =
    f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j)

Tactic:
simp [this, h, sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Algebra.Order.SuccPred.PartialSups
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : Add ι
inst_3 : One ι
inst_4 : OrderBot ι
inst_5 : LocallyFiniteOrder ι
inst_6 : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f : (a : ι) → α) (i + 1) = f ⊥ ⊔ (partialSups (f ∘ fun (k : ι) ↦ k + 1) : (a : ι) → α) i

Tactic:
simpa [← Order.succ_eq_add_one] using partialSups_succ' f i

Premises used: partialSups_succ', Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
h : IsSuccArchimedean X
⊢ IsSuccArchimedean.{u_1} (Multiplicative X)

Tactic:
h

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
h : IsSuccArchimedean X
⊢ IsSuccArchimedean.{u_1} (Additive X)

Tactic:
h

Premises used: Additive
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
h : IsPredArchimedean X
⊢ IsPredArchimedean.{u_1} (Multiplicative X)

Tactic:
h

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
h : IsPredArchimedean X
⊢ IsPredArchimedean.{u_1} (Additive X)

Tactic:
h

Premises used: Additive
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
x : X
⊢ Eq (α := Additive X) (succ ((ofMul : (a : X) → Additive X) x) : Additive X)
    ((ofMul : (a : X) → Additive X) (succ x) : Additive X)

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
x : Additive X
⊢ Eq (α := X) (succ ((toMul : (a : Additive X) → X) x) : X) ((toMul : (a : Additive X) → X) (succ x) : X)

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
x : X
⊢ Eq (α := Multiplicative X) (succ ((ofAdd : (a : X) → Multiplicative X) x) : Multiplicative X)
    ((ofAdd : (a : X) → Multiplicative X) (succ x) : Multiplicative X)

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : SuccOrder X
x : Multiplicative X
⊢ Eq (α := X) (succ ((toAdd : (a : Multiplicative X) → X) x) : X) ((toAdd : (a : Multiplicative X) → X) (succ x) : X)

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
x : X
⊢ Eq (α := Additive X) (pred ((ofMul : (a : X) → Additive X) x) : Additive X)
    ((ofMul : (a : X) → Additive X) (pred x) : Additive X)

Tactic:
rfl

Premises used: Order.pred, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
x : Additive X
⊢ Eq (α := X) (pred ((toMul : (a : Additive X) → X) x) : X) ((toMul : (a : Additive X) → X) (pred x) : X)

Tactic:
rfl

Premises used: Order.pred, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
x : X
⊢ Eq (α := Multiplicative X) (pred ((ofAdd : (a : X) → Multiplicative X) x) : Multiplicative X)
    ((ofAdd : (a : X) → Multiplicative X) (pred x) : Multiplicative X)

Tactic:
rfl

Premises used: Order.pred, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.TypeTags
Goal:
X : Type u_1
inst : Preorder X
inst_1 : PredOrder X
x : Multiplicative X
⊢ Eq (α := X) (pred ((toAdd : (a : Multiplicative X) → X) x) : X) ((toAdd : (a : Multiplicative X) → X) (pred x) : X)

Tactic:
rfl

Premises used: Order.pred, rfl
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
n : ℕ
rw : succ (↑(↑n : α) : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : Order.succ (↑n : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₂ rw₃ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
⊢ succ (↑n : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]

Premises used: Order.succ_eq_add_one, WithBot.succ_coe, WithBot.coe_natCast
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
⊢ Eq.{u_1 + 1} (α := α) (succ 0) 1

Tactic:
simpa using succ_natCast (α := α) 0

Premises used: WithBot.succ_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
⊢ Eq.{u_1 + 1} (α := α) (succ 1) 2

Tactic:
simpa [one_add_one_eq_two] using succ_natCast (α := α) 1

Premises used: one_add_one_eq_two, WithBot.succ_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ succ (OfNat.ofNat n) = HAdd.hAdd (α := α) (OfNat.ofNat n) 1

Tactic:
succ_natCast n

Premises used: WithBot.succ_natCast
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_2} (R := α) 1
inst_4 : SuccAddOrder α
a : WithBot α
bot : LE.le.{u_2} (α := WithBot α) 1 ⊥ ↔ LT.lt.{u_2} (α := WithBot α) 0 ⊥
coe : ∀ (a : α), 1 ≤ (↑a : WithBot α) ↔ 0 < (↑a : WithBot α)
⊢ 1 ≤ a ↔ 0 < a

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_2} (R := α) 1
inst_4 : SuccAddOrder α
⊢ LE.le.{u_2} (α := WithBot α) 1 ⊥ ↔ LT.lt.{u_2} (α := WithBot α) 0 ⊥

Tactic:
simp [Order.one_le_iff_pos]

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.Algebra.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_2} (R := α) 1
inst_4 : SuccAddOrder α
a : α
⊢ 1 ≤ (↑a : WithBot α) ↔ 0 < (↑a : WithBot α)

Tactic:
simp [Order.one_le_iff_pos]

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
x : α
⊢ succ x = x + 1

Tactic:
SuccAddOrder.succ_eq_add_one x

Premises used: Order.succ, SuccAddOrder.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < y
rw : succ 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 : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < y
⊢ succ x ≤ y

Tactic:
succ_le_of_lt h

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

Tactic:
exact succ_le_of_lt h

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

Tactic:
rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

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

Tactic:
add_one_le_iff_of_not_isMax (not_isMax x)

Premises used: not_isMax, Order.add_one_le_iff_of_not_isMax
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
x : α
rw : x ⩿ succ x
⊢ x ⩿ x + 1

Tactic:
rw [← succ_eq_add_one]

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
x : α
⊢ x ⩿ succ x

Tactic:
wcovBy_succ x

Premises used: Order.wcovBy_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
x : α
⊢ x ⩿ succ x

Tactic:
exact wcovBy_succ x

Premises used: Order.wcovBy_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
x : α
rw : x ⋖ succ x
⊢ x ⋖ x + 1

Tactic:
rw [← succ_eq_add_one]

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

Tactic:
covBy_succ x

Premises used: Order.covBy_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
x : α
⊢ x ⋖ succ x

Tactic:
exact covBy_succ x

Premises used: Order.covBy_succ
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
x : α
⊢ pred x = x - 1

Tactic:
PredSubOrder.pred_eq_sub_one x

Premises used: PredSubOrder.pred_eq_sub_one, Order.pred
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : 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 : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : x < y
⊢ x ≤ pred y

Tactic:
le_pred_of_lt h

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

Tactic:
exact le_pred_of_lt h

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

Tactic:
rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]

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

Tactic:
le_sub_one_iff_of_not_isMin (not_isMin y)

Premises used: not_isMin, Order.le_sub_one_iff_of_not_isMin
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
x : α
rw : pred x ⩿ x
⊢ x - 1 ⩿ x

Tactic:
rw [← pred_eq_sub_one]

Premises used: Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
x : α
⊢ pred x ⩿ x

Tactic:
pred_wcovBy x

Premises used: Order.pred_wcovBy
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
x : α
⊢ pred x ⩿ x

Tactic:
exact pred_wcovBy x

Premises used: Order.pred_wcovBy
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
x : α
rw : pred x ⋖ x
⊢ x - 1 ⋖ x

Tactic:
rw [← pred_eq_sub_one]

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

Tactic:
pred_covBy x

Premises used: Order.pred_covBy
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
x : α
⊢ pred x ⋖ x

Tactic:
exact pred_covBy x

Premises used: Order.pred_covBy
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
zero : x = x + (↑0 : α)
zero₁ : x = x + 0
zero₂ zero₃ : x = x
⊢ succ^[0] x = x + (↑0 : α)

Tactic:
rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, Function.iterate_zero_apply, add_zero
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
succ₂ : Order.succ (x + (↑n : α)) = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₃ : x + (↑n : α) + 1 = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₄ : x + (↑n : α) + 1 = x + HAdd.hAdd (α := α) (↑n : α) 1
succ₅ succ₆ : x + HAdd.hAdd (α := α) (↑n : α) 1 = x + HAdd.hAdd (α := α) (↑n : α) 1
⊢ Order.succ^[n + 1] x = x + (↑(n + 1) : α)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

Premises used: Function.iterate_succ_apply', Order.succ_eq_add_one, add_assoc, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
zero : Order.succ^[0] x = x + (↑0 : α)
succ : ∀ (n : ℕ) (IH : Order.succ^[n] x = x + (↑n : α)), Order.succ^[n + 1] x = x + (↑(n + 1) : α)
⊢ Order.succ^[n] x = x + (↑n : α)

Tactic:
induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

Premises used: Function.iterate_succ_apply', Order.succ, Order.succ_eq_add_one, add_assoc, Nat.cast_add, Nat.cast_zero, Function.iterate_zero_apply, add_zero, Nat.cast_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
zero : x = x - (↑0 : α)
zero₁ : x = x - 0
zero₂ zero₃ : x = x
⊢ pred^[0] x = x - (↑0 : α)

Tactic:
rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]

Premises used: sub_zero, Nat.cast_zero, Function.iterate_zero_apply
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
succ₂ : pred (x - (↑n : α)) = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₃ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₄ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) 1
succ₅ succ₆ : x - HAdd.hAdd (α := α) (↑n : α) 1 = x - HAdd.hAdd (α := α) (↑n : α) 1
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

Premises used: Function.iterate_succ_apply', Order.pred_eq_sub_one, Nat.cast_add, sub_sub, Nat.cast_one
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
zero : pred^[0] x = x - (↑0 : α)
succ : ∀ (n : ℕ) (IH : pred^[n] x = x - (↑n : α)), pred^[n + 1] x = x - (↑(n + 1) : α)
⊢ pred^[n] x = x - (↑n : α)

Tactic:
induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

Premises used: Function.iterate_succ_apply', Order.succ, sub_zero, Order.pred_eq_sub_one, Nat.cast_add, sub_sub, Nat.cast_zero, Function.iterate_zero_apply, Nat.cast_one