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

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

Tactic:
cases x <;> cases y

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ z → ↑a✝ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases x <;> cases y

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

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

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

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: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log ≤ y.log ↔ x ≤ y

Tactic:
rw [log_le_iff_le_exp hx, exp_log hy]

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✝ : DistribLattice α
x y z : WithBot α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ↑a✝ ⊓ z

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊥ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ↑a✝ ⊓ z

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊤ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z
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✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithBot α
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
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
⊢ ⊥ ≤ ⊥ ∨ ⊥ ≤ ⊥

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✝ ≤ ⊥

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✝

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.WithBot

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

Tactic:
cases x <;> cases y

Goal state after:
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
⊢ ⊤ ≤ ⊤ ∨ ⊤ ≤ ⊤

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✝ ≤ ⊤

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✝

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.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
refine eq_tsub_of_add_eq ?_
    rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le hna)

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✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithBot α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊥ < ⊥ ∨ ⊥ = ⊥ ∨ ⊥ < ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊥ < ↑a✝ ∨ ⊥ = ↑a✝ ∨ ↑a✝ < ⊥

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊥ ∨ ↑a✝ = ⊥ ∨ ⊥ < ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithTop α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
cases x <;> cases y

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊤ < ⊤ ∨ ⊤ = ⊤ ∨ ⊤ < ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊤ < ↑a✝ ∨ ⊤ = ↑a✝ ∨ ↑a✝ < ⊤

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊤ ∨ ↑a✝ = ⊤ ∨ ⊤ < ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ⊥ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑a✝¹ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ⊥) ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ↑a✝) ↔ ⊥ ≤ ↑a✝

case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ ⊥) ↔ ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝¹ → ↑z ≤ ↑a✝) ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ⊥

case coe.top
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
cases x <;> cases y

Goal state after:
case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ⊤

case top.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊤ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ⊤

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.ofDual ⊥ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ⊥

case coe.top
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
cases x <;> cases y

Goal state after:
case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ⊤

case top.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ⊤

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + ⅟b * a + (1 + ⅟a * b) ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + ⅟b * a + 1 + ⅟a * b ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x < y ↔ WithTop.ofDual y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.top
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < ⊤ ↔ WithTop.ofDual ⊤ < ⊥

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ⊥

case coe.top
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < ⊤ ↔ WithTop.ofDual ⊤ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
cases x <;> cases y

Goal state after:
case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ⊤

case top.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊤ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ⊤

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ↑a✝¹
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = -2 + (2 + ⅟b * a) + ⅟a * b ↔ -2 + 1 = ⅟b * a + ⅟a * b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ WithBot.toDual x < WithBot.toDual y ↔ y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < WithBot.toDual ⊥ ↔ ⊥ < ⊥

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ⊥ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ⊥

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ↑a✝¹
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = -2 + (2 + ⅟b * a) + ⅟a * b ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = -2 + 2 + ⅟b * a + ⅟a * b ↔ -2 + 1 = ⅟b * a + ⅟a * b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x < y ↔ WithTop.toDual y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.top
α : Type u_1
inst✝ : LT α
⊢ WithBot.ofDual ⊥ < ⊤ ↔ WithTop.toDual ⊤ < ⊥

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.ofDual ⊥ < ↑a✝ ↔ WithTop.toDual ↑a✝ < ⊥

case coe.top
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < ⊤ ↔ WithTop.toDual ⊤ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ < ↑a✝ ↔ WithTop.toDual ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
cases x <;> cases y

Goal state after:
case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ⊤

case top.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ⊤ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ⊤

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ⊥ ↔ ⊥ < ⊥

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ⊥

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ↑a✝¹
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)

Tactic:
← add_assoc,

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)

Tactic:
← add_assoc,

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + y * y ^ n + y * x ^ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1 + 1))) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
add_comm _ (b ^ _),

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1) * a + (b ^ (n + 1 + 1) + a ^ (n + 1) * b)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a ^ n + (c ^ n + d ^ n) = d ^ n

Tactic:
← add_assoc,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a ^ n + c ^ n + d ^ n = d ^ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a < a + (c + b)

Tactic:
← add_assoc,

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a < a + c + b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ |a ^ n| = a ^ n

Tactic:
abs_eq_self

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

pp: case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)

Tactic:
· exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b

Tactic:
← Icc_sdiff_right

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b \ {a}

Tactic:
← Icc_sdiff_right

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
by
  rw [NormNum.IsNat.to_eq h rfl]
  apply Nat.cast_pos.2
  simpa using! w

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
by
  rw [NormNum.IsInt.neg_to_eq h rfl]
  simp only [ne_eq, neg_eq_zero]
  apply ne_of_gt
  simpa using! w

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

Goal state before:
pp: case zero
α : Type u
m : ℕ
xs : List α
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs

Tactic:
cases xs with grind [dropSlice]

Goal state after: