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

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊥ + ↑z ≤ ⊥ + ↑z → ⊥ ≤ ⊥

pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ⊥ + ↑z ≤ ↑a✝ + ↑z → ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ↑a✝ + ↑z ≤ ⊥ + ↑z → ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑z ≤ ↑a✝ + ↑z → ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊥ + ↑z ≤ ⊥ + ↑z → ⊥ ≤ ⊥

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ⊥ + ↑z ≤ ↑a✝ + ↑z → ⊥ ≤ ↑a✝

case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ↑a✝ + ↑z ≤ ⊥ + ↑z → ↑a✝ ≤ ⊥

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑z ≤ ↑a✝ + ↑z → ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊥ < z → ↑x + ⊥ < ↑x + z

pp: case coe
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < z → ↑x + ↑a✝ < ↑x + z

Tactic:
<;>

Goal state after:
case bot
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊥ < z → ↑x + ⊥ < ↑x + z

case coe
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < z → ↑x + ↑a✝ < ↑x + z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊥ < ⊥ → ↑x + ⊥ < ↑x + ⊥

pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ⊥ < ↑a✝ → ↑x + ⊥ < ↑x + ↑a✝

pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < ⊥ → ↑x + ↑a✝ < ↑x + ⊥

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ → ↑x + ↑a✝¹ < ↑x + ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊥ < ⊥ → ↑x + ⊥ < ↑x + ⊥

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ⊥ < ↑a✝ → ↑x + ⊥ < ↑x + ↑a✝

case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < ⊥ → ↑x + ↑a✝ < ↑x + ⊥

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ → ↑x + ↑a✝¹ < ↑x + ↑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✝ : Preorder α
⊢ ⊥ < ⊥ ↔ ⊥ ≤ ⊥ ∧ ¬⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ⊥ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ⊥

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ↑a✝ ≤ ⊥ ∧ ¬⊥ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ⊥ < ⊥ ↔ ⊥ ≤ ⊥ ∧ ¬⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ⊥ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ↑a✝ ≤ ⊥ ∧ ¬⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ↑a✝¹
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < y → ⊥ + ↑z < y + ↑z

pp: case coe
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < y → ↑a✝ + ↑z < y + ↑z

Tactic:
<;>

Goal state after:
case bot
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < y → ⊥ + ↑z < y + ↑z

case coe
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < y → ↑a✝ + ↑z < y + ↑z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y

pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ↑a✝ ≤ map f y ↔ ↑a✝ ≤ y

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y

case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ↑a✝ ≤ map f y ↔ ↑a✝ ≤ y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < ⊥ → ⊥ + ↑z < ⊥ + ↑z

pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ⊥ < ↑a✝ → ⊥ + ↑z < ↑a✝ + ↑z

pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < ⊥ → ↑a✝ + ↑z < ⊥ + ↑z

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ → ↑a✝¹ + ↑z < ↑a✝ + ↑z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < ⊥ → ⊥ + ↑z < ⊥ + ↑z

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ⊥ < ↑a✝ → ⊥ + ↑z < ↑a✝ + ↑z

case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < ⊥ → ↑a✝ + ↑z < ⊥ + ↑z

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ → ↑a✝¹ + ↑z < ↑a✝ + ↑z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f ⊥ ↔ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ⊥ ≤ map f ↑a✝ ↔ ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ↑a✝ ≤ map f ⊥ ↔ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝¹ a✝ : α
⊢ map f ↑a✝¹ ≤ map f ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ⊥ ≤ map f ↑a✝ ↔ ⊥ ≤ ↑a✝

case coe.bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ↑a✝ ≤ map f ⊥ ↔ ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝¹ a✝ : α
⊢ map f ↑a✝¹ ≤ map f ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

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

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

Tactic:
<;>

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

case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unbotD b ↑a✝)
Module: Mathlib.Order.WithBot

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

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

Tactic:
<;>

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

case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
a✝ : α
⊢ ↑a✝ < ↑⊥ ↔ ↑a✝ = ⊥
Module: Mathlib.Order.WithBot

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

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

Tactic:
<;>

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

case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ = ⊥ ↔ ∀ (b : α), ↑a✝ < ↑b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

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

Tactic:
<;>

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

case coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ b + c ↔ ↑a✝ ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

pp: case bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ⊥ + c ≤ ↑a✝ + c ↔ ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ ⊥ + c ↔ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝¹ a✝ : WithTop α
⊢ ↑a✝¹ + c ≤ ↑a✝ + c ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ ⊥ + c ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ⊥ + c ≤ ↑a✝ + c ↔ ⊥ ≤ ↑a✝

case coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ ⊥ + c ↔ ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝¹ a✝ : WithTop α
⊢ ↑a✝¹ + c ≤ ↑a✝ + c ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

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

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → y ≤ ↑a✝ → ↑a✝ = y

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
y : WithBot α
⊢ ⊥ ≤ y → y ≤ ⊥ → ⊥ = y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → y ≤ ↑a✝ → ↑a✝ = y
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✝ : PartialOrder α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ = ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ⊥ = ↑a✝

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ ↑a✝ → ↑a✝ = ⊥

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ ↑a✝¹ → ↑a✝¹ = ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ = ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ⊥ = ↑a✝

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ ↑a✝ → ↑a✝ = ⊥

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ ↑a✝¹ → ↑a✝¹ = ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝

Tactic:
exact le_add_of_nonneg_right (h _)

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

Goal state before:
pp: case bot.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ⊥ + ⊥ ↔ ⊥ ≤ ⊥

pp: case bot.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ⊥ ≤ ⊥

pp: case bot.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ↑a✝ + ⊥ ↔ ⊥ ≤ ↑a✝

pp: case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ⊥ ≤ ↑a✝¹

pp: case coe.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝ + ⊥ ≤ ⊥ + ⊥ ↔ ↑a✝ ≤ ⊥

pp: case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝¹ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

pp: case coe.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝¹ + ⊥ ≤ ↑a✝ + ⊥ ↔ ↑a✝¹ ≤ ↑a✝

pp: case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝² + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ↑a✝² ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ⊥ + ⊥ ↔ ⊥ ≤ ⊥

case bot.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ⊥ ≤ ⊥

case bot.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ↑a✝ + ⊥ ↔ ⊥ ≤ ↑a✝

case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ⊥ ≤ ↑a✝¹

case coe.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝ + ⊥ ≤ ⊥ + ⊥ ↔ ↑a✝ ≤ ⊥

case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝¹ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

case coe.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝¹ + ⊥ ≤ ↑a✝ + ⊥ ↔ ↑a✝¹ ≤ ↑a✝

case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝² + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ↑a✝² ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

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

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

Tactic:
<;>

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

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤
    match ↑a✝, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)
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)

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)

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)

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

Goal state after:
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)

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)

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)

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)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ⊥ + ↑a✝ ≤ ↑(a✝¹ + a✝) ↔ ⊥ ≤ ↑a✝¹

pp: case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ↑(a✝¹ + a✝) ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

pp: case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ a✝² + a✝ ≤ a✝¹ + a✝ ↔ a✝² ≤ a✝¹

Tactic:
<;>

Goal state after:
case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ⊥ + ↑a✝ ≤ ↑(a✝¹ + a✝) ↔ ⊥ ≤ ↑a✝¹

case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ ↑(a✝¹ + a✝) ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ¬↑a✝ = ⊥
hc' : ¬a✝ = ⊤
⊢ a✝² + a✝ ≤ a✝¹ + a✝ ↔ a✝² ≤ a✝¹
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
  rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]; push Not; rfl

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

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

Tactic:
<;>

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

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