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

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a b : X
⊢ f a ≤ f b ↔ b ≤ a

Tactic:
hf.le_iff_ge

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a b : X
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a ^ 2 ⊔ a⁻¹ * a ⊔ (a ⊔ a⁻¹) * a⁻¹

Tactic:
inv_mul_cancel,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a ^ 2 ⊔ 1 ⊔ (a ⊔ a⁻¹) * a⁻¹
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hb : 1 ≤ b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
  rintro (rfl | rfl) <;> simp only [mabs_inv, mabs_of_one_le hb]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |(-(a / ↑n))| ≤ |a|

Tactic:
abs_neg

Goal state after:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
⊢ False

Tactic:
apply lt_irrefl (n : ℤ)

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
⊢ ↑n < ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : m.Coprime n
⊢ a ^ m = 1 ∧ a ^ n = 1 ↔ a = 1

Tactic:
by
  simp [← pow_gcd_eq_one, hmn]

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a b c : α
⊢ ↑a * ↑b * ↑c = ↑a * (↑b * ↑c)

Tactic:
by simp_rw [← coe_mul, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).log = x.log - y.log

Tactic:
lift x to Multiplicative G using hx; lift y to Multiplicative G using hy; rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
⊢ ⊤ - y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

Tactic:
cases y

Goal state after:
case top.top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

case top.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
a✝ : G
⊢ ↑a✝ - y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤

Tactic:
cases y

Goal state after:
case coe.top
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

case coe.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

Tactic:
cases y

Goal state after:
case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤

Tactic:
cases y

Goal state after:
case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases y

Goal state after:
case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊤

case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ↑a✝ ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases y

Goal state after:
case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ ⊤ ≠ ⊤

case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ ≠ ⊤ ↔ ↑a✝¹ ≠ ⊤ ∧ ↑a✝ ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ z) → (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y

Goal state after:
case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊤ ≤ ↑x + z → ⊤ ≤ z

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

Goal state before:
pp: case top
α : Type u
inst✝² : Add α
y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊤ + ↑z ≤ y + ↑z → ⊤ ≤ y

Tactic:
cases y

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

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

Goal state before:
pp: case coe
α : Type u
inst✝² : Add α
y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ↑a✝ + ↑z ≤ y + ↑z → ↑a✝ ≤ y

Tactic:
cases y

Goal state after:
case coe.top
α : 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: α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Tactic:
cases y

Goal state after:
case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊤ < z → ↑x + ⊤ < ↑x + z

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

Goal state before:
pp: case top
α : Type u
inst✝² : Add α
y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊤ < y → ⊤ + ↑z < y + ↑z

Tactic:
cases y

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

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

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

Tactic:
cases y

Goal state after:
case coe.top
α : 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.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]

Goal state after:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝ : Add α
y : WithBot α
⊢ ⊥ + y = ⊥ ↔ ⊥ = ⊥ ∨ y = ⊥

Tactic:
cases y

Goal state after:
case bot.bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ = ⊥ ↔ ⊥ = ⊥ ∨ ⊥ = ⊥

case bot.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊥ + ↑a✝ = ⊥ ↔ ⊥ = ⊥ ∨ ↑a✝ = ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y = ⊥ ↔ ↑a✝ = ⊥ ∨ y = ⊥

Tactic:
cases y

Goal state after:
case coe.bot
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ = ⊥ ↔ ↑a✝ = ⊥ ∨ ⊥ = ⊥

case coe.coe
α : Type u
inst✝ : Add α
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 α
⊢ ⊥ + y ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ y ≠ ⊥

Tactic:
cases y

Goal state after:
case bot.bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ ⊥ ≠ ⊥

case bot.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊥ + ↑a✝ ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ ↑a✝ ≠ ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y ≠ ⊥ ↔ ↑a✝ ≠ ⊥ ∧ y ≠ ⊥

Tactic:
cases y

Goal state after:
case coe.bot
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ ≠ ⊥ ↔ ↑a✝ ≠ ⊥ ∧ ⊥ ≠ ⊥

case coe.coe
α : Type u
inst✝ : Add α
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✝ : IsRightCancelAdd α
z : α
⊢ ⊥ + ↑z = y + ↑z ↔ ⊥ = y

Tactic:
cases y

Goal state after:
case bot.bot
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z : α
⊢ ⊥ + ↑z = ⊥ + ↑z ↔ ⊥ = ⊥

case bot.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ⊥ + ↑z = ↑a✝ + ↑z ↔ ⊥ = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝¹ : Add α
y : WithBot α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ↑a✝ + ↑z = y + ↑z ↔ ↑a✝ = y

Tactic:
cases y

Goal state after:
case coe.bot
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ↑a✝ + ↑z = ⊥ + ↑z ↔ ↑a✝ = ⊥

case coe.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑z = ↑a✝ + ↑z ↔ ↑a✝¹ = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z

Tactic:
cases y

Goal state after:
case bot
α : Type u
inst✝¹ : Add α
z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + ⊥ = ↑x + z ↔ ⊥ = z

case coe
α : Type u
inst✝¹ : Add α
z : WithBot α
inst✝ : IsLeftCancelAdd α
x a✝ : α
⊢ ↑x + ↑a✝ = ↑x + z ↔ ↑a✝ = z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊥ z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

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

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

Tactic:
cases y

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊥ ≤ ↑a✝ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

Tactic:
cases y

Goal state after:
case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ ⊥ ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ↔ ∀ (a : α), ↑a✝¹ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

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