awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) + (a + b) = 0

Tactic:
simp [neg_add_cancel_of_ne_top, *]

Premises used: LinearOrderedAddCommGroupWithTop.neg_add_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 : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a + b + (-b + -a) = 0

Tactic:
simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *]

Premises used: add_assoc, LinearOrderedAddCommGroupWithTop.add_neg_cancel_left_of_ne_top, 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 : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
exact left_neg_eq_right_neg (a := a + b) (by simp [neg_add_cancel_of_ne_top, *])
        (by simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *])

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

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

Tactic:
have ha : a ≠ ⊤ := by rintro rfl; simp at h
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [neg_add_cancel_of_ne_top, *]

Premises used: LinearOrderedAddCommGroupWithTop.neg_add_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 : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a = b

Tactic:
exact left_neg_eq_right_neg (a := a) (by simp [neg_add_cancel_of_ne_top, *]) h

Premises used: left_neg_eq_right_neg
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ -b ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective (β := α) fun (x : α) ↦ x - b

Tactic:
simpa [sub_eq_add_neg] using add_left_injective_of_ne_top (-b) (by simpa)

Premises used: sub_eq_add_neg, add_left_injective_of_ne_top, Neg.neg
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective (β := α) fun (x : α) ↦ b - x

Tactic:
simpa [sub_eq_add_neg] using (add_right_injective_of_ne_top b h).comp neg_injective

Premises used: add_right_injective_of_ne_top, neg_injective, sub_eq_add_neg, Function.Injective.comp
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b c : α
h : a ≠ ⊤
⊢ b - a = c - a ↔ b = c

Tactic:
(sub_left_injective_of_ne_top h).eq_iff

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

Tactic:
(sub_right_injective_of_ne_top h).eq_iff

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

Tactic:
simpa [sub_eq_add_neg] using add_left_strictMono_of_ne_top (b := -b) (by simpa)

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

Tactic:
(sub_left_strictMono_of_ne_top h).le_iff_le

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

Tactic:
(sub_left_strictMono_of_ne_top h).lt_iff_lt

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

Tactic:
contrapose
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a = ⊤ → ¬a + -a = 0

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
rw : a + -a = 0 ↔ a ≠ ⊤
rw₁ rw₂ : a ≠ ⊤ ↔ a ≠ ⊤
⊢ a - a = 0 ↔ a ≠ ⊤

Tactic:
rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]

Premises used: sub_eq_add_neg, LinearOrderedAddCommGroupWithTop.add_neg_cancel_iff_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
inl : 0 < a - ⊤ ↔ ⊤ < a ∨ Eq.{u_2 + 1} (α := α) ⊤ ⊤
inr : ∀ (hb : b ≠ ⊤), 0 < a - b ↔ b < a ∨ b = ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

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

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
simp [← sub_self_eq_zero_of_ne_top hb, hb]

Premises used: LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < -a ↔ a < 0 ∨ a = ⊤

Tactic:
simpa using sub_pos (a := 0) (b := a)

Premises used: LinearOrderedAddCommGroupWithTop.sub_pos
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
inl : 0 ≤ HSub.hSub (α := α) ⊤ ⊤
inr : ∀ (ha : a ≠ ⊤), 0 ≤ a - a
⊢ 0 ≤ a - a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ HSub.hSub (α := α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
inr inr₁ : LE.le.{u_2} (α := α) 0 0
⊢ 0 ≤ a - a

Tactic:
rw [sub_self_eq_zero_of_ne_top ha]

Premises used: LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
rw : b - a = a - a ↔ b = a
rw₁ rw₂ : b = a ↔ b = a
⊢ b - a = 0 ↔ b = a

Tactic:
rw [← sub_self_eq_zero_of_ne_top ha, sub_left_inj_of_ne_top ha]

Premises used: LinearOrderedAddCommGroupWithTop.sub_left_inj_of_ne_top, LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a : G
⊢ (↑(-a) : WithTop G) = -(↑a : WithTop G)

Tactic:
rfl

Premises used: WithTop.map, WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a b : G
⊢ (↑(a - b) : WithTop G) = (↑a : WithTop G) - (↑b : WithTop G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
⊢ Eq.{u_1 + 1} (α := WithTop G) (-⊤) ⊤

Tactic:
rfl

Premises used: WithTop.map, rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
coe : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤
⊢ ⊤ - x = ⊤

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
⊢ HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a : G
⊢ ⊤ - (↑a : WithTop G) = ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
coe : ∀ (a : G), (↑a : WithTop G) - ⊤ = ⊤
⊢ x - ⊤ = ⊤

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a : G
⊢ (↑a : WithTop G) - ⊤ = ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
x y : WithTop G
top : ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤
coe : ∀ (a : G), (↑a : WithTop G) - y = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ y = ⊤
⊢ x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
top₁ : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ (↑a : WithTop G) = ⊤
⊢ ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
a : G
coe : (↑a : WithTop G) - ⊤ = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
coe₁ : ∀ (a_1 : G), (↑a : WithTop G) - (↑a_1 : WithTop G) = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ (↑a_1 : WithTop G) = ⊤
⊢ (↑a : WithTop G) - y = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ y = ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
⊢ HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤

Tactic:
simp [← coe_sub]

Premises used: WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a : G
⊢ ⊤ - (↑a : WithTop G) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ (↑a : WithTop G) = ⊤

Tactic:
simp [← coe_sub]

Premises used: WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a : G
⊢ (↑a : WithTop G) - ⊤ = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤

Tactic:
simp [← coe_sub]

Premises used: WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
inst : AddCommGroup G
a a_1 : G
⊢ (↑a : WithTop G) - (↑a_1 : WithTop G) = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ (↑a_1 : WithTop G) = ⊤

Tactic:
simp [← coe_sub]

Premises used: WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a b : WithTop G
top : ⊤ - b = ⊤ + -b
coe : ∀ (a : G), (↑a : WithTop G) - b = (↑a : WithTop G) + -b
⊢ a - b = a + -b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = HAdd.hAdd (α := WithTop G) ⊤ (-⊤)
top₁ : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤ + -(↑a : WithTop G)
⊢ ⊤ - b = ⊤ + -b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
a : G
coe : (↑a : WithTop G) - ⊤ = (↑a : WithTop G) + -⊤
coe₁ : ∀ (a_1 : G), (↑a : WithTop G) - (↑a_1 : WithTop G) = (↑a : WithTop G) + -(↑a_1 : WithTop G)
⊢ (↑a : WithTop G) - b = (↑a : WithTop G) + -b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
⊢ HSub.hSub (α := WithTop G) ⊤ ⊤ = HAdd.hAdd (α := WithTop G) ⊤ (-⊤)

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, WithTop.LinearOrderedAddCommGroup.coe_neg, WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a : G
⊢ ⊤ - (↑a : WithTop G) = ⊤ + -(↑a : WithTop G)

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, WithTop.LinearOrderedAddCommGroup.coe_neg, WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a : G
⊢ (↑a : WithTop G) - ⊤ = (↑a : WithTop G) + -⊤

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, WithTop.LinearOrderedAddCommGroup.coe_neg, WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddGroupWithTop
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a a_1 : G
⊢ (↑a : WithTop G) - (↑a_1 : WithTop G) = (↑a : WithTop G) + -(↑a_1 : WithTop G)

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, WithTop.LinearOrderedAddCommGroup.coe_neg, WithTop.LinearOrderedAddCommGroup.coe_sub
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
a b : G
c d : P
hab : a ≤ b
hcd : c ≤ d
⊢ a • c ≤ b • d

Tactic:
(IsOrderedSMul.smul_le_smul_left _ _ hcd _).trans (IsOrderedSMul.smul_le_smul_right _ _ hab _)

Premises used: IsOrderedSMul.smul_le_smul_right, IsOrderedSMul.smul_le_smul_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
γ : Type u_3
inst : Preorder G
inst_1 : Preorder P
inst_2 : Preorder γ
inst_3 : SMul G P
inst_4 : IsOrderedSMul G P
f : γ → G
g : γ → P
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_3, u_2} (β := P) fun (x : γ) ↦ f x • g x

Tactic:
fun _ _ hab => (IsOrderedSMul.smul_le_smul_left _ _ (hg hab) _).trans
    (IsOrderedSMul.smul_le_smul_right _ _ (hf hab) _)

Premises used: Monotone, IsOrderedSMul.smul_le_smul_right, IsOrderedSMul.smul_le_smul_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : LE P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
⊢ ContravariantClass G P (fun (x1 : G) (x2 : P) ↦ x1 • x2) fun (x1 x2 : P) ↦ x1 ≤ x2

Tactic:
⟨IsOrderedCancelSMul.le_of_smul_le_smul_left⟩

Premises used: IsOrderedCancelSMul.le_of_smul_le_smul_left, ContravariantClass.mk
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d

Tactic:
lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_

Premises used: lt_of_le_of_lt, IsOrderedSMul.smul_le_smul_right
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
refine : b • c < b • d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_

Premises used: lt_of_le_of_lt, IsOrderedSMul.smul_le_smul_right
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ b • c < b • d

Tactic:
lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_

Premises used: le_of_lt, lt_of_le_not_ge, IsOrderedSMul.smul_le_smul_left
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
refine : ¬b • d ≤ b • c
⊢ b • c < b • d

Tactic:
refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_

Premises used: le_of_lt, lt_of_le_not_ge, IsOrderedSMul.smul_le_smul_left
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
by_contra : ∀ (hbdc : b • d ≤ b • c), False
⊢ ¬b • d ≤ b • c

Tactic:
by_contra hbdc
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
⊢ d ≤ c

Tactic:
have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ c ≤ d ∧ ¬d ≤ c

Tactic:
rw [@lt_iff_le_not_ge] at h₂

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
h₃ : c ≤ d ∧ ¬d ≤ c
⊢ b • d ≤ b • c

Tactic:
rw [@lt_iff_le_not_ge] at h₂

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
h₃ : c ≤ d ∧ ¬d ≤ c
hbdc₁ : b • d ≤ b • c
⊢ d ≤ c

Tactic:
rw [@lt_iff_le_not_ge] at h₂

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c ≤ d ∧ ¬d ≤ c
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Tactic:
simp_all only [not_true_eq_false, and_false]

Premises used: not_true_eq_false, and_false
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • c < b • d

Tactic:
lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_left c d h₂ a) ?_

Premises used: lt_of_le_of_lt, IsOrderedSMul.smul_le_smul_left
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
refine : a • d < b • d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_left c d h₂ a) ?_

Premises used: lt_of_le_of_lt, IsOrderedSMul.smul_le_smul_left
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • d < b • d

Tactic:
lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_

Premises used: le_of_lt, IsOrderedSMul.smul_le_smul_right, lt_of_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
refine : ¬b • d ≤ a • d
⊢ a • d < b • d

Tactic:
refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_

Premises used: le_of_lt, IsOrderedSMul.smul_le_smul_right, lt_of_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
by_contra : ∀ (hbad : b • d ≤ a • d), False
⊢ ¬b • d ≤ a • d

Tactic:
by_contra hbad
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
⊢ b ≤ a

Tactic:
have h : b ≤ a := IsOrderedCancelSMul.le_of_smul_le_smul_right b a d hbad
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ a ≤ b ∧ ¬b ≤ a

Tactic:
rw [@lt_iff_le_not_ge] at h₁

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
h₃ : a ≤ b ∧ ¬b ≤ a
⊢ c ≤ d

Tactic:
rw [@lt_iff_le_not_ge] at h₁

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
h₃ : a ≤ b ∧ ¬b ≤ a
h₄ : c ≤ d
⊢ b • d ≤ a • d

Tactic:
rw [@lt_iff_le_not_ge] at h₁

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
h₃ : a ≤ b ∧ ¬b ≤ a
h₄ : c ≤ d
hbad₁ : b • d ≤ a • d
⊢ b ≤ a

Tactic:
rw [@lt_iff_le_not_ge] at h₁

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.AddTorsor
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b ∧ ¬b ≤ a
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Tactic:
simp_all only [not_true_eq_false, and_false]

Premises used: not_true_eq_false, and_false
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : PosMulMono β
inst_6 : MulPosMono β
h : Monotone.{u_1, u_2} (α := α) (β := β) (⇑(algebraMap α β) : (a : α) → β)
⊢ Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1

Tactic:
simpa [Algebra.smul_def] using h

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : SMulPosMono α β
⊢ Monotone.{u_1, u_2} (α := α) (β := β) (⇑(algebraMap α β) : (a : α) → β)

Tactic:
simpa [Algebra.smul_def] using smul_one_mono (α := α) β

Premises used: smul_one_mono, Algebra.smul_def
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ LE.le.{u_2} (α := β) (0 : β) ((algebraMap α β : (a : α) → β) a : β)

Tactic:
simpa using algebraMap_mono β ha

Premises used: algebraMap_mono
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
⊢ IsOrderedModule α β ↔ Monotone.{u_1, u_2} (α := α) (β := β) (⇑(algebraMap α β) : (a : α) → β)

Tactic:
simp [isOrderedModule_iff_smul_one_mono, Algebra.smul_def]

Premises used: isOrderedModule_iff_smul_one_mono, Algebra.smul_def