awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
inl : LT.lt.{u_4} (α := S) (1 : S) (((v : (a : R) → S) x)⁻¹ : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x⁻¹ : S)

Tactic:
rw [map_inv₀]

Premises used: map_inv₀
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) (((v : (a : R) → S) x)⁻¹ : S)

Tactic:
(one_lt_inv₀ <| v.pos hx₀).mpr h

Premises used: Iff.mpr, AbsoluteValue.pos, one_lt_inv₀
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) (((v : (a : R) → S) x)⁻¹ : S)

Tactic:
exact (one_lt_inv₀ <| v.pos hx₀).mpr h

Premises used: Iff.mpr, AbsoluteValue.pos, one_lt_inv₀
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)

Tactic:
⟨x, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)

Tactic:
exact ⟨x, h⟩
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
obtain :
  ∀ (y : R) (hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)),
    ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)

Tactic:
obtain ⟨y, hy⟩ := h.exists_abv_gt_one

Premises used: AbsoluteValue.IsNontrivial.exists_abv_gt_one
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
⊢ y ≠ 0

Tactic:
have hy₀ := v.ne_zero_iff.mp <| (zero_lt_one.trans hy).ne'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)

Tactic:
⟨y⁻¹, inv_ne_zero hy₀, ?_⟩

Premises used: Inv.inv, And.intro, Exists.intro, inv_ne_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
refine : LT.lt.{u_4} (α := S) ((v : (a : R) → S) y⁻¹ : S) (1 : S)
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)

Tactic:
refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
rw : LT.lt.{u_4} (α := S) (((v : (a : R) → S) y)⁻¹ : S) (1 : S)
⊢ LT.lt.{u_4} (α := S) ((v : (a : R) → S) y⁻¹ : S) (1 : S)

Tactic:
rw [map_inv₀]

Premises used: map_inv₀
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
⊢ LT.lt.{u_4} (α := S) (((v : (a : R) → S) y)⁻¹ : S) (1 : S)

Tactic:
(inv_lt_one₀ <| v.pos hy₀).mpr hy

Premises used: Iff.mpr, inv_lt_one₀, AbsoluteValue.pos
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
⊢ LT.lt.{u_4} (α := S) (((v : (a : R) → S) y)⁻¹ : S) (1 : S)

Tactic:
exact (inv_lt_one₀ <| v.pos hy₀).mpr hy

Premises used: Iff.mpr, inv_lt_one₀, AbsoluteValue.pos
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
x : R
⊢ 0 ≤ abv x

Tactic:
abv_nonneg' x

Premises used: IsAbsoluteValue.abv_nonneg'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
x : R
⊢ abv x = 0 ↔ x = 0

Tactic:
abv_eq_zero'

Premises used: IsAbsoluteValue.abv_eq_zero'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
x y : R
⊢ abv (x + y) ≤ abv x + abv y

Tactic:
abv_add' x y

Premises used: IsAbsoluteValue.abv_add'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
x y : R
⊢ abv (x * y) = abv x * abv y

Tactic:
abv_mul' x y

Premises used: IsAbsoluteValue.abv_mul'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
⊢ abv 0 = 0

Tactic:
(toAbsoluteValue abv).map_zero

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.map_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
a : R
⊢ 0 < abv a ↔ a ≠ 0

Tactic:
(toAbsoluteValue abv).pos_iff

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.pos_iff
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
S_1 : Type u_4
S : Type u_5
inst : Ring S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
⊢ IsAbsoluteValue.{u_5, u_5} (S := S) abs

Tactic:
AbsoluteValue.abs.isAbsoluteValue

Premises used: abs, AbsoluteValue.abs, AbsoluteValue.isAbsoluteValue
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Ring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
inst_4 : IsDomain S
inst_5 : Nontrivial R
⊢ abv 1 = 1

Tactic:
(toAbsoluteValue abv).map_one

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.map_one
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Ring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Semiring R
inst_3 : IsDomain S
inst_4 : Nontrivial R
abv : R → S
inst_5 : IsAbsoluteValue abv
a : R
n : ℕ
⊢ abv (a ^ n) = abv a ^ n

Tactic:
(toAbsoluteValue abv).map_pow a n

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.map_pow
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Ring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Ring R
abv : R → S
inst_3 : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

Premises used: add_assoc, sub_eq_add_neg, HSub.hSub, IsAbsoluteValue.abv_add
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Ring S
inst_1 : PartialOrder S
R : Type u_6
inst_2 : Ring R
abv : R → S
inst_3 : IsAbsoluteValue abv
inst_4 : IsOrderedRing S
a b : R
⊢ abv a - abv b ≤ abv (a - b)

Tactic:
(toAbsoluteValue abv).le_sub a b

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.le_sub
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : NoZeroDivisors S
inst_4 : Ring R
abv : R → S
inst_5 : IsAbsoluteValue abv
a : R
⊢ abv (-a) = abv a

Tactic:
(toAbsoluteValue abv).map_neg a

Premises used: AbsoluteValue.map_neg, IsAbsoluteValue.toAbsoluteValue
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : NoZeroDivisors S
inst_4 : Ring R
abv : R → S
inst_5 : IsAbsoluteValue abv
a b : R
⊢ abv (a - b) = abv (b - a)

Tactic:
(toAbsoluteValue abv).map_sub a b

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.map_sub
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
R : Type u_6
inst_3 : Ring R
abv : R → S
inst_4 : IsAbsoluteValue abv
a b : R
⊢ |abv a - abv b| ≤ abv (a - b)

Tactic:
(toAbsoluteValue abv).abs_abv_sub_le_abv_sub a b

Premises used: AbsoluteValue.abs_abv_sub_le_abv_sub, IsAbsoluteValue.toAbsoluteValue
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsCancelMulZero S
R : Type u_6
inst_3 : Semiring R
inst_4 : Nontrivial R
abv : R → S
inst_5 : IsAbsoluteValue abv
⊢ abv 1 = 1

Tactic:
(toAbsoluteValue abv).map_one_of_isLeftRegular <|
    (IsRegular.of_ne_zero <| (toAbsoluteValue abv).ne_zero one_ne_zero).left

Premises used: AbsoluteValue.map_one_of_isLeftRegular, IsRegular.of_ne_zero, IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.ne_zero, IsRegular.left, one_ne_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semifield S
inst_1 : LinearOrder S
R : Type u_6
inst_2 : DivisionSemiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
a : R
⊢ abv a⁻¹ = (abv a)⁻¹

Tactic:
map_inv₀ (abvHom' abv) a

Premises used: map_inv₀, IsAbsoluteValue.abvHom'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
S : Type u_5
inst : Semifield S
inst_1 : LinearOrder S
R : Type u_6
inst_2 : DivisionSemiring R
abv : R → S
inst_3 : IsAbsoluteValue abv
a b : R
⊢ abv (a / b) = abv a / abv b

Tactic:
map_div₀ (abvHom' abv) a b

Premises used: IsAbsoluteValue.abvHom', map_div₀
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x y : R
h : abv.IsEuclidean
⊢ LT.lt.{u_2} (α := S) ((abv : (a : R) → S) x : S) ((abv : (a : R) → S) y : S) ↔ x ≺ y

Tactic:
map_lt_map_iff' h

Premises used: AbsoluteValue.IsEuclidean.map_lt_map_iff'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
h : abv.IsEuclidean
a b : R
hb : b ≠ 0
⊢ LT.lt.{u_2} (α := S) ((abv : (a : R) → S) (a % b) : S) ((abv : (a : R) → S) b : S)

Tactic:
h.map_lt_map_iff.mpr (EuclideanDomain.mod_lt a hb)

Premises used: Iff.mpr, EuclideanDomain.mod_lt, AbsoluteValue.IsEuclidean.map_lt_map_iff
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean
Goal:
x y : ℤ
rw : (↑x.natAbs : ℤ) < |y| ↔ x.natAbs < y.natAbs
rw₁ : LT.lt (α := ℤ) (↑x.natAbs : ℤ) (↑y.natAbs : ℤ) ↔ x.natAbs < y.natAbs
rw₂ rw₃ : x.natAbs < y.natAbs ↔ x.natAbs < y.natAbs
⊢ |x| < |y| ↔ x.natAbs < y.natAbs

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]

Premises used: Int.ofNat_lt, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a : α
⊢ ⊤ + a = ⊤

Tactic:
LinearOrderedAddCommMonoidWithTop.top_add' a

Premises used: LinearOrderedAddCommMonoidWithTop.top_add'
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a : α
⊢ a + ⊤ = ⊤

Tactic:
Trans.trans (add_comm _ _) (top_add _)

Premises used: Trans.trans, add_comm, top_add
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a : α
ha : a ≠ ⊤
⊢ IsAddRegular a

Tactic:
simpa using LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top ha

Premises used: LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective (β := α) fun (x : α) ↦ x + b

Tactic:
(IsAddRegular.of_ne_top h).2

Premises used: IsAddRegular.right, IsAddRegular.of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective (β := α) fun (x : α) ↦ b + x

Tactic:
(IsAddRegular.of_ne_top h).1

Premises used: IsAddRegular.of_ne_top, IsAddRegular.left
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ b + a = c + a ↔ b = c

Tactic:
(add_left_injective_of_ne_top _ h).eq_iff

Premises used: Function.Injective.eq_iff, add_left_injective_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ a + b = a + c ↔ b = c

Tactic:
(add_right_injective_of_ne_top _ h).eq_iff

Premises used: add_right_injective_of_ne_top, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono (β := α) fun (x : α) ↦ x + b

Tactic:
add_left_mono.strictMono_of_injective <| add_left_injective_of_ne_top _ h

Premises used: add_left_injective_of_ne_top, Monotone.strictMono_of_injective, add_left_mono
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono (β := α) fun (x : α) ↦ b + x

Tactic:
add_right_mono.strictMono_of_injective <| add_right_injective_of_ne_top _ h

Premises used: add_right_injective_of_ne_top, Monotone.strictMono_of_injective, add_right_mono
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ b + a ≤ c + a ↔ b ≤ c

Tactic:
(add_left_strictMono_of_ne_top h).le_iff_le

Premises used: add_left_strictMono_of_ne_top, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ a + b ≤ a + c ↔ b ≤ c

Tactic:
(add_right_strictMono_of_ne_top h).le_iff_le

Premises used: add_right_strictMono_of_ne_top, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ b + a < c + a ↔ b < c

Tactic:
(add_left_strictMono_of_ne_top h).lt_iff_lt

Premises used: add_left_strictMono_of_ne_top, StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a b c : α
h : a ≠ ⊤
⊢ a + b < a + c ↔ b < c

Tactic:
(add_right_strictMono_of_ne_top h).lt_iff_lt

Premises used: add_right_strictMono_of_ne_top, StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top ha]

Premises used: add_comm, LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
b : α
⊢ a + (-a + b) = b

Tactic:
simp [← add_assoc, add_neg_cancel_of_ne_top ha]

Premises used: add_assoc, LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
b : α
⊢ -a + (a + b) = b

Tactic:
simp [← add_assoc, neg_add_cancel_of_ne_top ha]

Premises used: LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top, add_assoc
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + b + -b = a

Tactic:
simp [add_assoc, add_neg_cancel_of_ne_top hb]

Premises used: add_assoc, LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + -b + b = a

Tactic:
simp [add_assoc, neg_add_cancel_of_ne_top hb]

Premises used: LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top, add_assoc
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
h : Eq.{u_2 + 1} (α := α) ⊤ 0
obtain : ∀ (a : α) (ha : a ≠ 0), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := exists_ne (0 : α)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
h : Eq.{u_2 + 1} (α := α) ⊤ 0
a : α
ha : a ≠ 0
⊢ 0 + a ≠ 0

Tactic:
rw [← zero_add a] at ha

Premises used: zero_add
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
h : Eq.{u_2 + 1} (α := α) ⊤ 0
a : α
ha : 0 + a ≠ 0
⊢ False

Tactic:
simp [LinearOrderedAddCommGroupWithTop.top_add', -zero_add, ← h] at ha

Premises used: zero_add, LinearOrderedAddCommGroupWithTop.top_add'
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
⊢ Ne.{u_2 + 1} (α := α) 0 ⊤

Tactic:
top_ne_zero.symm

Premises used: Ne.symm, LinearOrderedAddCommGroupWithTop.top_ne_zero
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
⊢ LT.lt.{u_2} (α := α) 0 ⊤

Tactic:
lt_top_iff_ne_top.2 top_ne_zero.symm

Premises used: Iff.mpr, Ne.symm, lt_top_iff_ne_top, LinearOrderedAddCommGroupWithTop.top_ne_zero
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
c : α
hbc : ⊤ + c = 0
⊢ False

Tactic:
simp [LinearOrderedAddCommGroupWithTop.top_add'] at hbc

Premises used: LinearOrderedAddCommGroupWithTop.top_add'
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ a + -a = 0

Tactic:
simp [ha, add_neg_cancel_of_ne_top]

Premises used: LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

Tactic:
simp [← isAddUnit_iff]

Premises used: LinearOrderedAddCommGroupWithTop.isAddUnit_iff
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
rw : ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
rw [← not_iff_not, not_or]

Premises used: not_iff_not, not_or
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤

Tactic:
add_ne_top

Premises used: LinearOrderedAddCommGroupWithTop.add_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤

Tactic:
exact add_ne_top

Premises used: LinearOrderedAddCommGroupWithTop.add_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

Tactic:
simp [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
⊢ a = ⊤

Tactic:
simpa [h] using add_neg_cancel_of_ne_top (x := a)

Premises used: LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
h : a = ⊤
⊢ -a = ⊤

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - ⊤ = ⊤

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
inl : Eq.{u_2 + 1} (α := α) (- -⊤) ⊤
inr : ∀ (ha : a ≠ ⊤), - -a = a
⊢ - -a = a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b c : α
⊢ Eq.{u_2 + 1} (α := α) (- -⊤) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
inr : - -a + -a = 0
inr₁ : -a + a = 0
⊢ - -a = a

Tactic:
apply left_neg_eq_right_neg (a := -a)

Premises used: left_neg_eq_right_neg
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
⊢ - -a + -a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top, ha]

Premises used: add_comm, LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top, ha]

Premises used: add_comm, LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
inl : -(⊤ + b) = -b + -⊤
inr : ∀ (ha : a ≠ ⊤), -(a + b) = -b + -a
⊢ -(a + b) = -b + -a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b_1 c b : α
⊢ -(⊤ + b) = -b + -⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
ha : a ≠ ⊤
inr : -(a + ⊤) = -⊤ + -a
inr₁ : ∀ (hb : b ≠ ⊤), -(a + b) = -b + -a
⊢ -(a + b) = -b + -a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
⊢ -(a + ⊤) = -⊤ + -a

Tactic:
simp