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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑↑n ↔ 0 ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ -↑n ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑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 : α
x✝ : { y // y ≠ ⊥ }
⊢ (fun x ↦ ⟨↑x, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨x, h⟩ => x.unbot h)
        x✝) =
    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 x✝ : α
⊢ (fun x ↦
        match x with
        | ⟨x, h⟩ => x.unbot h)
      ((fun x ↦ ⟨↑x, ⋯⟩) x✝) =
    x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Nonempty α
a : α
ha : ↑a ≠ ⊥
⊢ (↑a).unbotA = (↑a).unbot ha

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ⊥) = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : α
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ↑a✝) = ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ⊥) = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ↑a✝) = ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : WithBot α
⊢ (e₁.trans e₂).withBotCongr x = (e₁.withBotCongr.trans e₂.withBotCongr) x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ ((∃ b, x = ⊥ ∧ y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b) ↔ (x = ⊥ ∧ ∃ b, y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ⊥ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
⊢ ↑a ≤ ⊥ → ⊥ ≤ ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ ↑a ≤ ↑a✝ → ↑a✝ ≤ ↑a

Tactic:
simp

Goal state after:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ a ≤ a✝ → a✝ ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ a ≤ (↑x).unbot hx ↔ ↑a ≤ ↑x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx ≤ a ↔ ↑x ≤ ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx ≤ y.unbot hy ↔ x ≤ y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : LE α
inst✝ : Nonempty α
x : α
⊢ (↑x).unbotA ≤ a ↔ ↑x ≤ ↑a

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
⊢ a * 0 ≤ b * 0

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a c : α
hc : c ≠ 0
hab : a ≤ a
⊢ a * c ≤ a * c

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ x < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ x < ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LT α
x : WithBot α
a✝ : α
⊢ x < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ x < ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ⊥ ≠ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ↑a✝ ≠ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ a < (↑x).unbot hx ↔ ↑a < ↑x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ Additive.toMul (OrderDual.ofDual (⊤ + a)) = Additive.toMul (OrderDual.ofDual ⊤)

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ ⊥ * Additive.toMul (OrderDual.ofDual a) = ⊥
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ (a : α), ¬a = ⊥ → IsRegular a
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx < b ↔ ↑x < ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx < y.unbot hy ↔ x < y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : LT α
inst✝ : Nonempty α
x : α
⊢ (↑x).unbotA < a ↔ ↑x < ↑a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : Additive αᵒᵈ), ⊤ + x = ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : (Additive α)ᵒᵈ), ⊤ + x = ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Additive.toMul (OrderDual.ofDual (-⊤)) = Additive.toMul (OrderDual.ofDual ⊤)

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ⊥⁻¹ = ⊥
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → x + -x = 0

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (a : α), ¬a = ⊥ → OrderDual.toDual (Additive.ofMul a) + -OrderDual.toDual (Additive.ofMul a) = 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ 0 < ↑(y * z⁻¹)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : Preorder α
b : α
⊢ ⊥ ≤ ↑(unbotD b ⊥)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ⊥ < ↑⊥ ↔ ⊥ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
a✝ : α
⊢ ↑a✝ < ↑⊥ ↔ ↑a✝ = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊥
⊢ ⊥ + ↑(Classical.arbitrary α) ≤ ⊥ + ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
simp

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
simp

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:
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✝ : SemilatticeSup α
⊢ ⊥ ≤
    match ⊥, ⊥ 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:
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✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤
    match ⊥, ↑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:
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✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤
    match ↑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:
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✝¹ ≤
    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:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

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✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ : α
⊢ ↑a✝ ≤ 0 → ∃ c, 0 = ↑a✝ + c

Tactic:
simp

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

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

Tactic:
simp

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₂ : β ≃+ γ
x : WithBot α
⊢ (e₁.trans e₂).withBotCongr x = (e₁.withBotCongr.trans e₂.withBotCongr) x

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✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤
    match ⊥, ↑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:
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✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤
    match ↑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:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
· rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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✝ ≤
    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:
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✝ : SemilatticeSup α
⊢ ⊥ ≤ ⊥ →
    ⊥ ≤ ⊥ →
      (match ⊥, ⊥ 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:
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✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤ ↑a✝ →
    ⊥ ≤ ↑a✝ →
      (match ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑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✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤ ⊥ →
    ↑a✝ ≤ ⊥ →
      (match ⊥, ↑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:
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✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ⊥, ↑a✝¹ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑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✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ ⊥ →
    ⊥ ≤ ⊥ →
      (match ↑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:
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✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    ⊥ ≤ ↑a✝ →
      (match ↑a✝¹, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑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✝ : SemilatticeSup α
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:
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✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑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.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ (match ⊤, ⊤ 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:
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✝ : SemilatticeInf α
a✝ : α
⊢ (match ⊤, ↑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:
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✝ : SemilatticeInf α
a✝ : α
⊢ (match ↑a✝, ⊤ with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ↑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✝ : α
⊢ (match ↑a✝¹, ↑a✝ with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ↑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✝ : SemilatticeInf α
a✝ : α
⊢ (match ⊤, ↑a✝ with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ↑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✝ : SemilatticeInf α
a✝ : α
⊢ (match ↑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:
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✝ : α
⊢ (match ↑a✝¹, ↑a✝ with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ↑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✝ : SemilatticeSup α
⊢ 0 ≤
    match 0, 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 zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤
    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✝ : α
⊢ ↑a✝ ≤
    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 top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊤ ≤ ⊤ →
    ⊤ ≤ ⊤ →
      ⊤ ≤
        match ⊤, ⊤ 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:
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✝ : SemilatticeInf α
a✝ : α
⊢ ⊤ ≤ ⊤ →
    ⊤ ≤ ↑a✝ →
      ⊤ ≤
        match ⊤, ↑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:
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✝ : SemilatticeInf α
a✝ : α
⊢ ⊤ ≤ ↑a✝ →
    ⊤ ≤ ⊤ →
      ⊤ ≤
        match ↑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:
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✝ : SemilatticeInf α
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:
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✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊤ →
    ↑a✝ ≤ ⊤ →
      ↑a✝ ≤
        match ⊤, ⊤ 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:
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✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ →
    ↑a✝¹ ≤ ↑a✝ →
      ↑a✝¹ ≤
        match ⊤, ↑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:
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✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    ↑a✝¹ ≤ ⊤ →
      ↑a✝¹ ≤
        match ↑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: