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

Goal state before:
pp: case coe.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ⊤ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊤ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝¹ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝)

Tactic:
simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) → (fun x1 x2 ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊤ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊤

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case top.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) →
    (fun x1 x2 ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊤ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊤

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

Tactic:
simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = 0

Tactic:
tsub_eq_zero_of_le h

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ 0 = 0
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ 0 = ↑m - ↑n

Tactic:
tsub_eq_zero_of_le

Goal state after:
case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ 0 = 0

case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ ⊥ → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊥ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝¹ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ ⊥ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊥ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥)

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝¹ ↑a✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝)

Tactic:
simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²
Module: Mathlib.Order.WithBot

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

Tactic:
by simp [le_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
by simp [le_def]

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✝ : LE α
x y : WithBot α
⊢ ∀ (a : WithBot α), ⊥ ≤ a

Tactic:
by simp [le_def]

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

Goal state before:
pp: case bot.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) → (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case bot.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

Tactic:
simp [← coe_add, swap]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

Tactic:
simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
z : α
hz : ↑x < z ∧ z < ↑y
⊢ x < Units.mk0 z ⋯ ∧ Units.mk0 z ⋯ < y

Tactic:
simp [← Units.val_lt_val, hz]

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
  simpa using natCast_mono n.zero_le

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:
le_neg,

Goal state after:
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 ↔ ceil (-z) ≤ -a
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:
rw [le_floor, Int.cast_zero]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ DirectedOn (r on f) s ↔ DirectedOn r (f '' s)

Tactic:
refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
this : ∀ (m n : α), f m ≤ f n
⊢ f a = f b

Tactic:
exact le_antisymm (this a b) (this b a)

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

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
H₁.floor_of_neg,

Goal state after:
case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ 0 = FloorSemiring.floor a

case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:

Tactic:
_ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u * ↑u⁻¹).natAbs = 1

Tactic:
Units.mul_inv

Goal state after:
u : ℤˣ
⊢ natAbs 1 = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl
⊢ IsUnit 1

Tactic:
exact isUnit_one

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈ ↑((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) ((fun x ↦ Subtype.val ⁻¹' ↑x) x)) ↔ y ∈ ↑x

Tactic:
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds (s ∪ t)).Nonempty

Tactic:
upperBounds_union

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iio True = {False}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Ioi False = {True}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}

Tactic:
rw [isGreatest_univ.upperBounds_eq, Ici_top]

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]
  exact Nat.cast_nonneg' n

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ -(b / -c) ↔ b ≤ -(a * -c)

Tactic:
le_neg,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / -c ≤ -a ↔ b ≤ -(a * -c)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
by
  simpa using one_div_le_one_div_of_neg_of_le (one_div b ▸ inv_lt_zero'.2 hb) h

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []

Tactic:
cases H

Goal state after:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
⊢ l = []

Tactic:
cases H

Goal state after:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁ ~ l₂[n] :: l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rel_congr_right (getElem_cons_eraseIdx_perm ..)

Goal state after:
case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a

Tactic:
rw [replicate_append_replicate]

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
by
    rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]
    congr
    exact dropLast_append_getLast (cons_ne_nil b l)

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp [zpow']
  · simp [zpow', zpow_eq_zero_iff hn]
    tauto

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
by
  constructor
  · rintro rfl
    exact ⟨rfl, fun _ _ _ ↦ rfl⟩
  · intro ⟨h₁, h₂⟩
    exact ext_get h₁ h₂

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval

Tactic:
simp only [eval_cons, h, div_eq_mul_inv]
  ac_rfl

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ f (g x) :: map f (map g xs) = x :: xs

Tactic:
h x,

Goal state after:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ x :: map f (map g xs) = x :: xs
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: n : ℕ
⊢ ↑n = ↑n /. 1

Tactic:
rw [← Int.cast_natCast, intCast_eq_divInt]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ den ⟨Rat.divInt ↑q.den ↑q.num, ⋯⟩ = q.num

Tactic:
den,

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑⟨Rat.divInt ↑q.den ↑q.num, ⋯⟩).den = q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.num / ↑q.den = q

Tactic:
by
  ext1
  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]
  exact (cast_def _).symm

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q

Tactic:
by rw [← q.num_divNat_den]; exact H _ _ q.den_ne_zero q.coprime_num_den

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩
  rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e
  refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_
  have := congr_arg Int.natAbs e
  simp only [Int.natAbs_mul, Int.natAbs_natCast] at this; simp [this]

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: z : ℤ
⊢ IsSquare z ∧ True ↔ IsSquare z

Tactic:
and_true

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsNNRat (↑n.succ * ⅟↑d)⁻¹ d n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))

Goal state after:
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsNNRat (↑n.succ * ⅟↑d)⁻¹ d n.succ