mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
⊢ ∀ ⦃a : Multiplicative αᵒᵈ⦄, 0 < a → ∀ ⦃b c : Multiplicative αᵒᵈ⦄, b < c → a * b < a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x : WithBot α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
⊢ AddLECancellable x → x ≠ ⊥

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) = findGreatest P n

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a : WithZero α
⊢ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ x = ⊥ → ∀ (b : α), x ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
⊢ ↑a < ↑b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ 0 < ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : WithZero α
⊢ ¬a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ x = ⊥ ↔ ∀ (b : α), x ≤ ↑b

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hlt : 0 < n
heq : n = 0
⊢ ¬P n

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), ↑a ≤ x → ↑a ≤ y) ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), y ≤ ↑a → x ≤ ↑a) ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), ↑a < x → p x) ↔ ∀ (b : α), a < b → p ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a < x ∧ p x) ↔ ∃ b, a < b ∧ p ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), ↑a ≤ x → p x) ↔ ∀ (b : α), a ≤ b → p ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
⊢ MulLeftMono (WithZero α)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a ≤ x ∧ p x) ↔ ∃ b, a ≤ b ∧ p ↑b

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
n : ℕ
hlt : k + 1 < n
hle : n ≤ k + 1
⊢ ¬P n

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
x y : WithBot α
⊢ x ≤ y → y ≤ x → x = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ ↑b ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unbotD a y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ → ∀ (a : α), ↑↑a ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ ↔ ∀ (a : α), ↑↑a ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono (WithZero α)

Tactic:
by

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

Goal state before:
pp: m k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

Tactic:
by

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ x ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
by

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ 0 < findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ a + c ≤ b + c ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a✝ b✝ : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithZero α
⊢ a ≤ b → ∃ c, b = a + c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : Monotone ⇑f
⊢ Monotone ⇑(map' f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : StrictMono ⇑f
⊢ StrictMono ⇑(map' f)

Tactic:
by

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
m n : ℕ
hmn : m ≤ n
⊢ findGreatest P m ≤ findGreatest P n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithBot α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝² : Add α
inst✝¹ : Add β
inst✝ : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
by

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

Goal state before:
pp: P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
⊢ findGreatest P n ≤ findGreatest Q n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < ↑(ofAdd b)
⊢ toAdd (unzero ha) < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ y ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
EX : ∃ n, P (b + ↑n)
z : ℤ
h : P z
⊢ b + ↑(Nat.find EX) ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P (- -z)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ a < ↑(ofAdd b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ ↑(ofAdd b)
⊢ toAdd (unzero ha) ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ a ≤ ↑(ofAdd b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y z : WithBot α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : toAdd (unzero h) = b
⊢ a = ↑(ofAdd b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : a = ↑(ofAdd b)
⊢ toAdd (unzero h) = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    x

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
⊢ MulLeftReflectLT (WithZero α)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ x ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithTop α
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ y ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a✝ n✝ : ℕ
x✝ : 0 ≤ a✝
⊢ n✝ ≤ id a✝ ↔ ↑n✝ ≤ a✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
⊢ id n ≤ a ↔ n ≤ ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
k : ℕ
⊢ ↑(n + k) = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ StrictMono Nat.cast

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ ↑a ≤ b ↔ a ≤ id b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ id a ≤ b ↔ a ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ (fun a ↦ -floor (-a)) a ≤ z ↔ a ≤ ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ a ≤ (fun a ↦ -ceil (-a)) z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
⊢ { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_4
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
⊢ ∃ n, ↑n ≤ x

Tactic:
obtain ⟨n, hn⟩ := bounded (-x)

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
n : ℕ
hn : -x ≤ ↑n
⊢ ∃ n, ↑n ≤ x
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
⊢ ∃ n, ↑n ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
⊢ ∃ n, x ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: x : ℤ
⊢ fract x = 0 x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ ≤ z ↔ a < ↑z + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y z : WithZero α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z < ⌊a⌋ ↔ ↑z + 1 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithBot α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ⌊a⌋ < 0 ↔ a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ x ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ < z ↔ a ≤ ↑z - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ ≤ 0 ↔ a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋.toNat ↔ ↑n ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ (fun a ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
⊢ StrictMono Int.cast

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ⌈a⌉

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ⌊a⌋ ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x✝ : WithZero α
⊢ 0 ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLE α
a : α
⊢ ¬↑a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLT α
x✝ : WithZero α
⊢ ¬x✝ < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ 0 < ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithZero α
⊢ x ≤ y ∨ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ≤ max ↑b ↑c ↔ a ≤ max b c

Tactic:
by

Goal state after: