awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this_1 : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
this : n • |a| = HSMul.hSMul (β := K) n 1 • |a|
refine_2 : |k| • |a| ≤ HSMul.hSMul (β := K) n 1 • |a|
⊢ |k| • |a| ≤ n • |a|

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this_1 : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
this : n • |a| = HSMul.hSMul (β := K) n 1 • |a|
⊢ 0 ≤ |a|

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this_1 : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
this : n • |a| = HSMul.hSMul (β := K) n 1 • |a|
⊢ |k| • |a| ≤ HSMul.hSMul (β := K) n 1 • |a|

Tactic:
exact smul_le_smul_of_nonneg_right hn (by simp)

Premises used: smul_le_smul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
inl : LE.le (α := ArchimedeanClass M) (mk a) (mk (HSMul.hSMul.{u_2, u_1, u_1} (α := K) 0 a))
inr : ∀ (h : k ≠ 0), LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))
⊢ LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))

Tactic:
obtain rfl | h := eq_or_ne k 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
⊢ LE.le (α := ArchimedeanClass M) (mk a) (mk (HSMul.hSMul.{u_2, u_1, u_1} (α := K) 0 a))

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
⊢ LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
s : UpperSet (ArchimedeanClass M)
k : K
a : M
inl :
  Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) a →
    Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) (k • a)
inr : ∀ (hs : s ≠ ⊤), a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier
⊢ a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier

Tactic:
obtain rfl | hs := eq_or_ne s ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
k : K
a : M
__spread.0 : AddSubgroup M := addSubgroup ⊤
⊢ Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) a →
    Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) (k • a)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
s : UpperSet (ArchimedeanClass M)
k : K
a : M
hs : s ≠ ⊤
⊢ a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier

Tactic:
simpa [mem_addSubgroup_iff hs] using s.upper (mk_le_mk_smul a k)

Premises used: ArchimedeanClass.mk_le_mk_smul, ArchimedeanClass.mem_addSubgroup_iff, UpperSet.upper
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
⊢ Submodule.toAddSubgroup (module_M := inst_7) (ball K c) = c.ballAddSubgroup

Tactic:
rfl

Premises used: dite, rfl, ArchimedeanClass.addSubgroup
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
⊢ Submodule.toAddSubgroup (module_M := inst_7) (closedBall K c) = c.closedBallAddSubgroup

Tactic:
rfl

Premises used: dite, rfl, ArchimedeanClass.addSubgroup
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
c : ArchimedeanClass M
hc : c ≠ ⊤
⊢ Membership.mem (γ := Submodule K M) (ball K c) a ↔ c < mk a

Tactic:
mem_ballAddSubgroup_iff hc

Premises used: Set.Mem, ArchimedeanClass.mem_ballAddSubgroup_iff
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
c : ArchimedeanClass M
⊢ Membership.mem (γ := Submodule K M) (closedBall K c) a ↔ c ≤ mk a

Tactic:
mem_closedBallAddSubgroup_iff

Premises used: Set.Mem, ArchimedeanClass.mem_closedBallAddSubgroup_iff
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
⊢ Eq.{u_1 + 1} (α := Submodule K M) (ball K ⊤) ⊥

Tactic:
(Submodule.toAddSubgroup_inj _ _).mp <| ballAddSubgroup_top M

Premises used: ArchimedeanClass.ballAddSubgroup_top, Iff.mp, Submodule.toAddSubgroup_inj
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
⊢ Eq.{u_1 + 1} (α := Submodule K M) (closedBall K ⊤) ⊥

Tactic:
(Submodule.toAddSubgroup_inj _ _).mp <| closedBallAddSubgroup_top M

Premises used: ArchimedeanClass.closedBallAddSubgroup_top, Iff.mp, Submodule.toAddSubgroup_inj
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : ArchimedeanClass M
_ : ∀ ⦃b : ArchimedeanClass M⦄, a ≤ b → LE.le (α := Submodule K M) (ball K b) (ball K a)
⊢ ∀ ⦃b : ArchimedeanClass M⦄, a ≤ b → LE.le (α := Submodule K M) (ball K b) (ball K a)

Tactic:
_
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a b : ArchimedeanClass M
h : a ≤ b
⊢ LE.le (α := Submodule K M) (ball K b) (ball K a)

Tactic:
(Submodule.toAddSubgroup_le _ _).mp <| ballAddSubgroup_antitone h

Premises used: ArchimedeanClass.ballAddSubgroup_antitone, Iff.mp, Submodule.toAddSubgroup_le
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a b : ArchimedeanClass M
h : a ≤ b
⊢ LE.le (α := Submodule K M) (ball K b) (ball K a)

Tactic:
exact (Submodule.toAddSubgroup_le _ _).mp <| ballAddSubgroup_antitone h

Premises used: ArchimedeanClass.ballAddSubgroup_antitone, Iff.mp, Submodule.toAddSubgroup_le
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
inl : LE.le.{u_1} (α := Submodule K M) (ball K ⊤) (closedBall K ⊤)
inr : ∀ (hc : c ≠ ⊤), LE.le (α := Submodule K M) (ball K c) (closedBall K c)
⊢ LE.le (α := Submodule K M) (ball K c) (closedBall K c)

Tactic:
obtain rfl | hc := eq_or_ne c ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
⊢ LE.le.{u_1} (α := Submodule K M) (ball K ⊤) (closedBall K ⊤)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
hc : c ≠ ⊤
a : M
ha : Membership.mem (γ := Submodule K M) (ball K c) a
⊢ Membership.mem (γ := Submodule K M) (closedBall K c) a

Tactic:
simpa using ((mem_ball_iff K hc).mp ha).le

Premises used: ArchimedeanClass.mem_ball_iff, LT.lt.le, Iff.mp
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
s : UpperSet (FiniteArchimedeanClass M)
k : K
a : M
ha : a ∈ (addSubgroup s).carrier
ne : Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk (k • a)) ⊤
eq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a) ⊤
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (k • a)) ⊤

Tactic:
simp [ArchimedeanClass.mk_eq_top_iff.mp eq]

Premises used: Iff.mp, ArchimedeanClass.mk_eq_top_iff
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
⊢ StrictAnti.{u_1, u_1} (α := UpperSet (FiniteArchimedeanClass M)) (β := Submodule K M) (submodule K)

Tactic:
addSubgroup_strictAnti

Premises used: StrictAnti, FiniteArchimedeanClass.addSubgroup_strictAnti, FiniteArchimedeanClass.submodule, FiniteArchimedeanClass.addSubgroup
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : FiniteArchimedeanClass M
⊢ Submodule.toAddSubgroup (module_M := inst_7) (ball K c) = c.ballAddSubgroup

Tactic:
rfl

Premises used: FiniteArchimedeanClass.addSubgroup, rfl
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : FiniteArchimedeanClass M
⊢ Submodule.toAddSubgroup (module_M := inst_7) (closedBall K c) = c.closedBallAddSubgroup

Tactic:
rfl

Premises used: FiniteArchimedeanClass.addSubgroup, rfl
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
c : FiniteArchimedeanClass M
⊢ Membership.mem (γ := Submodule K M) (ball K c) a ↔ ∀ (h : a ≠ 0), c < mk a h

Tactic:
mem_ballAddSubgroup_iff

Premises used: Set.Mem, FiniteArchimedeanClass.mem_ballAddSubgroup_iff
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
c : FiniteArchimedeanClass M
⊢ Membership.mem (γ := Submodule K M) (closedBall K c) a ↔ ∀ (h : a ≠ 0), c ≤ mk a h

Tactic:
mem_closedBallAddSubgroup_iff

Premises used: Set.Mem, FiniteArchimedeanClass.mem_closedBallAddSubgroup_iff
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
⊢ StrictAnti.{u_1, u_1} (α := FiniteArchimedeanClass M) (β := Submodule K M) (ball K)

Tactic:
ballAddSubgroup_strictAnti

Premises used: StrictAnti, FiniteArchimedeanClass.ballAddSubgroup_strictAnti, FiniteArchimedeanClass.submodule, FiniteArchimedeanClass.addSubgroup
-- Module: Mathlib.Algebra.Order.Module.Archimedean
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : FiniteArchimedeanClass M
⊢ LT.lt (α := Submodule K M) (ball K c) (closedBall K c)

Tactic:
submodule_strictAnti _ Set.Ioi_ssubset_Ici_self

Premises used: FiniteArchimedeanClass.submodule_strictAnti, Set.Ioi_ssubset_Ici_self
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
rw₁ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
rw₂ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊓ y))
rw₃ : x ⊓ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊓ y)
rw₄ : x ⊓ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊓ y)
rw₅ rw₆ : x ⊓ y = x ⊓ y
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)

Tactic:
rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]

Premises used: two_smul, smul_smul, invOf_mul_self, one_smul, two_nsmul_inf_eq_add_sub_abs_sub
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
rw₁ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
rw₂ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊔ y))
rw₃ : x ⊔ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊔ y)
rw₄ : x ⊔ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊔ y)
rw₅ rw₆ : x ⊔ y = x ⊔ y
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)

Tactic:
rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]

Premises used: two_nsmul_sup_eq_add_add_abs_sub, two_smul, smul_smul, invOf_mul_self, one_smul
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
inl : ∀ (ha : a ≤ 0), |a • b| = |a| • |b|
inr : ∀ (ha : 0 ≤ a), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|

Tactic:
obtain ha | ha := le_total a 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
inl : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
inl₁ : ∀ (hb : 0 ≤ b), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|

Tactic:
obtain hb | hb := le_total b 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
inr : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
inr₁ : ∀ (hb : 0 ≤ b), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|

Tactic:
obtain hb | hb := le_total b 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

Premises used: smul_nonneg, smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

Premises used: smul_nonneg, smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

Premises used: smul_nonneg, smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

Premises used: smul_nonneg, smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
𝕜 : Type u_1
M : Type u_3
inst : DivisionSemiring 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
inst_5 : IsOrderedAddMonoid M
x y : M
⊢ x ⊓ y = HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 2⁻¹ (x + y - |y - x|)

Tactic:
let := invertibleOfNonzero (two_ne_zero' 𝕜); inf_eq_half_smul_add_sub_abs_sub 𝕜 x y

Premises used: two_ne_zero', inf_eq_half_smul_add_sub_abs_sub, invertibleOfNonzero
-- Module: Mathlib.Algebra.Order.Module.Basic
Goal:
𝕜 : Type u_1
M : Type u_3
inst : DivisionSemiring 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
inst_5 : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 2⁻¹ (x + y + |y - x|)

Tactic:
let := invertibleOfNonzero (two_ne_zero' 𝕜); sup_eq_half_smul_add_add_abs_sub 𝕜 x y

Premises used: sup_eq_half_smul_add_add_abs_sub, two_ne_zero', invertibleOfNonzero
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
ha : 0 ≤ a
⊢ Monotone (β := β) fun (x : β) ↦ a • x

Tactic:
PosSMulMono.smul_le_smul_of_nonneg_left ha

Premises used: Monotone, PosSMulMono.smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulStrictMono α β
ha : 0 < a
⊢ StrictMono (β := β) fun (x : β) ↦ a • x

Tactic:
PosSMulStrictMono.smul_lt_smul_of_pos_left ha

Premises used: StrictMono, PosSMulStrictMono.smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
hb : b₁ ≤ b₂
ha : 0 ≤ a
⊢ a • b₁ ≤ a • b₂

Tactic:
monotone_smul_left_of_nonneg ha hb

Premises used: monotone_smul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulStrictMono α β
hb : b₁ < b₂
ha : 0 < a
⊢ a • b₁ < a • b₂

Tactic:
strictMono_smul_left_of_pos ha hb

Premises used: strictMono_smul_left_of_pos