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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ 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
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q + ↑q * 1 + (↑q * -1 + 1 * -1) = ↑p * ↑q - 1

Tactic:
;

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ 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
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q + ↑q * 1 + (↑q * -1 + 1 * -1) = ↑p * ↑q - 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
this : b ^ n = a ^ m
⊢ a = 0 ^ n ∧ b = 0 ^ m

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
this : b ^ n = a ^ m
⊢ a = 0 ^ n ∧ b = 0 ^ m
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ c, a = c ^ n) ↔ ∃ y, y ^ n = a

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ c, a = c ^ n) ↔ ∃ y, y ^ n = a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x

Tactic:
;

Goal state after:
β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ ⊤ ≠ 0

Tactic:
intro h
  obtain ⟨a, ha⟩ := exists_ne (0 : α)
  rw [← zero_add a] at ha
  simp [LinearOrderedAddCommGroupWithTop.top_add', -zero_add, ← h] at ha

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
c : α
hbc : ⊤ + c = 0
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
c : α
hbc : ⊤ + c = 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ 0 ^ ↑n.succ = 0 ^ ↑n * 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ 0 ^ ↑n.succ = 0 ^ ↑n * 0
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ 0 ^ ↑n.succ = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ 0 ^ ↑n.succ = 0
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
x✝¹ x✝ : (WithZero α)ˣ
⊢ ↑(unzero ⋯) = ↑(unzero ⋯ * unzero ⋯)

Tactic:
simp only [Units.val_mul, coe_unzero, coe_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ recZeroCoe 0 Units.val (if h : x✝ = 0 then 0 else ↑(Units.mk0 x✝ h)) = x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ recZeroCoe 0 Units.val (if h : x✝ = 0 then 0 else ↑(Units.mk0 x✝ h)) = x✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Goal state after:
case inr.inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ -(a + ⊤) = -⊤ + -a

case inr.inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
h : ⊤ + b = 0
⊢ False

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
h : ⊤ + b = 0
⊢ False
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a = ⊤ → ¬a + -a = 0

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a = ⊤ → ¬a + -a = 0
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : α
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : α
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : β
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : β
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : α
⊢ ∀ (y : α),
    { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝ * y) =
      { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x✝ *
        { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : α
⊢ ∀ (y : α),
    { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝ * y) =
      { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x✝ *
        { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < a - ⊤ ↔ ⊤ < a ∨ ⊤ = ⊤

case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝¹ : α ≃* β
x✝ : α
⊢ ((fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝¹ : α ≃* β
x✝ : α
⊢ ((fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝¹))
      x✝ =
    x✝¹ x✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
x : WithZero α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      x =
    x✝ x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
x : WithZero α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      x =
    x✝ x
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : Multiplicative M
⊢ exp (↑x).log = ↑x

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x : Multiplicative M
⊢ exp (↑x).log = ↑x
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
⊢ (↑x * y).log = (↑x).log + y.log

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
⊢ (↑x * y).log = (↑x).log + y.log
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : Multiplicative M
⊢ (↑x * ↑y).log = (↑x).log + (↑y).log

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x y : Multiplicative M
⊢ (↑x * ↑y).log = (↑x).log + (↑y).log
Module: Mathlib.Algebra.GroupWithZero.WithZero

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

Tactic:
;

Goal state after:
G : Type u_5
inst✝ : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ (↑x / y).log = (↑x).log - y.log
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x y : Multiplicative G
⊢ (↑x / ↑y).log = (↑x).log - (↑y).log

Tactic:
;

Goal state after:
G : Type u_5
inst✝ : AddGroup G
x y : Multiplicative G
⊢ (↑x / ↑y).log = (↑x).log - (↑y).log
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c

Tactic:
;

Goal state after:
α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : Add α
y z : WithTop α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝
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:
;

Goal state after:
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝

Tactic:
;

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

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

Tactic:
;

Goal state after:
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
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 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:
;

Goal state after:
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
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 coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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

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

Tactic:
;

Goal state after:
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
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 coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b = a - min a b

Tactic:
rcases le_total a b with h | h

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - min a b

case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - min a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊤
⊢ False

Tactic:
;

Goal state after:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊤
⊢ False
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + b = max a b

Tactic:
rcases le_total a b with h | h

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = max a b

case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = max a b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + b = max a b

Tactic:
by
  rcases le_total a b with h | h
  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
  · rw [max_eq_left h, tsub_add_cancel_of_le h]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c

Tactic:
;

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c

Tactic:
;

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y
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:
;

Goal state after:
α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
;

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²