mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

Tactic:
simp

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

Goal state before:
pp: case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ 0 →
    ↑a✝ ≤ 0 →
      (match 0, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

Tactic:
simp

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

Goal state before:
pp: case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match 0, ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ 0 →
    0 ≤ 0 →
      (match ↑a✝, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

Tactic:
simp

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

Goal state before:
pp: case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match ↑a✝¹, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 →
    ↑a✝ ≤ 0 →
      (match ↑a✝¹, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

Tactic:
simp

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

Tactic:
simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ ⊥ → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

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

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

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

Goal state before:
pp: case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ 0 ≤ 0 → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

Tactic:
simp

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

Goal state before:
pp: case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ 0 → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

Tactic:
simp

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

Goal state before:
pp: case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

Tactic:
simp

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

Goal state before:
pp: case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝¹ → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ 0 → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

Tactic:
simp

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

Goal state before:
pp: case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

Tactic:
simp

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝
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:
simp

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:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ 0 ≤ ↑a✝ ∨ ↑a✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ 0 ∨ 0 ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono (WithZero α)
⊢ ∀ (a b : WithZero α), a ≤ b → ∀ (c : WithZero α), c + a ≤ c + b

Tactic:
simpa [add_comm] using fun _ _ ↦ add_le_add_left

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a < x.log ↔ exp a < x

Tactic:
rw [← log_lt_log exp_ne_zero hx, log_exp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Preorder G
a b : G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
⊢ ∀ {a b : (WithZero (Multiplicative G))ˣ}, logEquiv a ≤ logEquiv b ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: case inl
y : Multiplicative ℤ
⊢ 0 < ↑y * exp 1 ↔ 0 ≤ ↑y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

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

Goal state before:
pp: case zero
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
⊢ 0 ≤ exp (log 0)

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊤ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝¹ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ⊤ ≤ ↑a✝

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝ → a✝¹ ≤ a✝ → a✝² ≤ a✝ ∧ a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
b : α
⊢ 0 ≤ ↑(unzeroD b 0)

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unzeroD b ↑a✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
by simpa using lt_succ_floor a

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ 0 / n = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ ∀ ⦃x y : β⦄, (r on f) x y → r (f x) (f y)

Tactic:
simp

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 α
inst✝ : DecidableLE α
x✝ : WithBot α
⊢ ⊥ ≤ x✝

Tactic:
simp

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 α
inst✝ : DecidableLE α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
simp

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✝¹ : LT α
inst✝ : DecidableLT α
x✝ : WithBot α
⊢ ¬x✝ < ⊥

Tactic:
simp

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✝¹ : LT α
inst✝ : DecidableLT α
a : α
⊢ ⊥ < ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊥ ≤ ⊥ ∨ ⊥ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊥ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊥ ∨ ⊥ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ↔ IsDirectedOrder ↑s

Tactic:
directedOn_iff_directed,

Goal state after:
α : Type u_1
inst✝ : LE α
s : Set α
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val ↔ IsDirectedOrder ↑s
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊤ ≤ ⊤ ∨ ⊤ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊤ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊤ ∨ ⊤ ≤ ↑a✝

Tactic:
simp

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✝¹ : LT α
inst✝ : WellFoundedLT α
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun x1 x2 ↦ x1 < x2) y

Tactic:
simp

Goal state after: