mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ 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
⊢ ∃ 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
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
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
⊢ ∃ 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
⊢ ∃ 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
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
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
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_1
α : 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
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
·

Goal state after:
case neg.refine_1
α : 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
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_2
α : 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
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
·

Goal state after:
case neg.refine_2
α : 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
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
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
⊢ ↑n - 1 < ↑n

Tactic:
by lia

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

Goal state before:
pp: case bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ y + ⊥

pp: case coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ y + ↑a✝

Tactic:
·

Goal state after:
case bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ y + ⊥
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ⊥ + ↑a✝

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
·

Goal state after:
case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ⊥ + ↑a✝
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
·

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ ⊥ + y

pp: case coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ ↑a✝ + y

Tactic:
·

Goal state after:
case bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ ⊥ + y
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ↑a✝ + ⊥

pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
·

Goal state after:
case coe.bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ↑a✝ + ⊥
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
·

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

pp: case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
⊢ ∃ a, f a = b

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
⊢ ∃ a, (map' f) a = ↑b

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
⊢ ∃ a, f a = b
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
⊢ ∃ a, (map' f) a = ↑b

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
⊢ ∃ a, (map' f) a = ↑b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b c : α
⊢ - -⊤ = ⊤

pp: case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a

Tactic:
·

Goal state after:
case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b c : α
⊢ - -⊤ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
·

Goal state after:
case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

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

Tactic:
·

Goal state after:
case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
⊢ -(⊤ + b) = -b + -⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
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: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - a = 0 ↔ a ≠ ⊤

Tactic:
rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]

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

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

pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < a - ⊤ ↔ ⊤ < a ∨ ⊤ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ ⊤ - ⊤

pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ ⊤ - ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
⊢ f (1 0) = 1 0

pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x

Tactic:
·

Goal state after:
case inl
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
⊢ f (1 0) = 1 0
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x

Tactic:
·

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = max ↑a ↑b

Tactic:
by
  simp_rw [max_def, val_le_val, ← apply_ite]
  rfl

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

Goal state before:
pp: case none.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ ↑a + none ≤ ↑a + none → none ≤ none

pp: case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c

pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
·

Goal state after:
case none.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ ↑a + none ≤ ↑a + none → none ≤ none
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c

pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
·

Goal state after:
case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
·

Goal state after:
case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
·

Goal state after:
case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + y < z + w

Tactic:
apply (WithTop.add_lt_add_left xz.ne_top yw).trans_le

Goal state after:
α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + w ≤ z + w
Module: Mathlib.Algebra.Order.Sub.Basic

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

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

Tactic:
·

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

Goal state before:
pp: case top
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤

pp: case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝

Tactic:
·

Goal state after:
case top
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝

Tactic:
·

Goal state after:
case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝
Module: Mathlib.Algebra.Order.Sub.Basic

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

Tactic:
·

Goal state after:
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: case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝

Tactic:
· exact (WithTop.add_lt_add_right coe_ne_top xz).le

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
x : WithTop α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
⊢ AddLECancellable x → x ≠ ⊤

Tactic:
rintro h rfl; exact (coe_lt_top <| Classical.arbitrary _).not_ge <| h <| by simp

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

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f) (⊤ + b) = map ⇑f ⊤ + map (⇑f) b

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

Tactic:
·

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

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

Tactic:
·

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

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

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

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

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

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

Tactic:
·

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

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✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝
Module: Mathlib.Algebra.Order.Sub.Basic

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

Tactic:
·

Goal state after:
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: case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

pp: case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)