mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ * ↑b = Option.bind ⊥ fun a ↦ Option.some (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ↑a * ⊥ = Option.bind ⊥ fun b ↦ Option.some (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ x * a ≤ x * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ a * x ≤ b * x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ x * a < x * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ a * x < b * x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
x✝¹ : WithBot α
x✝ : ⊥ ≤ x✝¹
⊢ ⊥.succ ≤ x✝¹.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : α
hab : ↑a ≤ ⊥
⊢ (↑a).succ ≤ ⊥.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a b : α
hab : ↑a ≤ ↑b
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
hab : ⊥ < ↑b
⊢ ⊥.succ < (↑b).succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
hab : ↑a < ↑b
⊢ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
⊢ a.succ = ⊥ ↔ a = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
x✝¹ : WithTop α
x✝ : x✝¹ ≤ ⊤
⊢ x✝¹.pred ≤ ⊤.pred

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : α
hab : ⊤ ≤ ↑a
⊢ ⊤.pred ≤ (↑a).pred

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : α
hab : ↑a ≤ ↑b
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
hab : ↑b < ⊤
⊢ (↑b).pred < ⊤.pred

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
hab : ↑a < ↑b
⊢ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
⊢ a.pred = ⊤ ↔ a = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : α
hmn : m ≤ n
⊢ P n hmn

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
⊢ p a ↔ p b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ ≤ v₂ ∨ v₂ ≤ v₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : SuccOrder α
⊢ ∀ (a : αᵒᵈ), (⇑toDual ∘ SuccOrder.succ ∘ ⇑ofDual) a ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a✝ : αᵒᵈ
h : a✝ ≤ (⇑toDual ∘ SuccOrder.succ ∘ ⇑ofDual) a✝
⊢ IsMin a✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ¬IsMax a✝
x✝ : α
⊢ a✝ < x✝ ↔ (if h : (Ioi a✝).Nonempty then ⋯.min (Ioi a✝) h else a✝) ≤ x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
⊢ IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsSuccLimit (toDual a) ↔ IsPredLimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : ¬IsMin a
⊢ IsSuccPrelimit a ↔ IsSuccLimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ succ a ≤ b ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : IsSuccPrelimit a
⊢ NoMaxOrder ↑(Iio a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
⊢ IsSuccPrelimit ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
⊢ IsSuccLimit ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
x : WithTop α
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsSuccPrelimit y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsSuccPrelimit x
⊢ IsSuccPrelimit ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ IsSuccPrelimit ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
x : WithTop α
⊢ IsSuccLimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsSuccLimit y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsSuccLimit x
⊢ IsSuccLimit ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ IsSuccLimit ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithTop α
⊢ IsPredPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsPredLimit y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsPredLimit x
⊢ IsPredLimit ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
⊢ IsMax a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ IsMax (succ^[n] a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
b : α
⊢ succ b ≠ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Iic a ⊆ Iio (succ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
⊢ IsMin a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Icc a b ⊆ Ico a (succ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝⁴ : Preorder α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMaxOrder α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioc a b ⊆ Ioo a (succ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
⊢ a ∈ range succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ IsSuccLimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Iic a ⊆ Iio (succ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
⊢ a ≤ b ↔ ∀ c < a, c ≤ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
⊢ IsSuccPrelimit a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsSuccLimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
⊢ IsLUB (Iio a) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = 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 α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
⊢ isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb

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✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
⊢ f (succ a) = succ (f a)

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 α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a = b → a ⋖ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ succ ⊤ = ⊤

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 α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : ¬IsMax b
⊢ isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb

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 ≤ b

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 α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb

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
⊢ b < succ 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 : α
hb : ¬IsMax b
⊢ b < succ 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 : α
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
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
⊢ a ≤ b → ∃ n, pred^[n] b = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedGT α
inst✝ : SuccOrder α
⊢ IsPredArchimedean αᵒᵈ

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 α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ prelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x 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.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc 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 : α
hb : ¬IsMax b
⊢ Ioo a (succ b) = Ioc 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
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ 0 < j

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 α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h✝ : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
a c : α
ha : ¬IsMax a
hc : ¬IsMax c
x : (a : α) → motive a
h : a = c
⊢ cast ⋯ (succ a ha (x a)) = succ c hc (x c)

Tactic:
by

Goal state after: