awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
obtain :
  ∀ (e : HahnEmbedding.Partial h.some) (hdomain : (↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤),
    ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
      StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
          (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
        ∀ (a : M),
          Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
            ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
              (orderTop.{u_2, u_3} (R := R)
                ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
                  ((f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
⊢ ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop.{u_2, u_3} (R := R)
              ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))

Tactic:
obtain ⟨e, hdomain⟩ := HahnEmbedding.Partial.exists_domain_eq_top h.some

Premises used: Nonempty.some, HahnEmbedding.Partial.exists_domain_eq_top
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
e : HahnEmbedding.Partial h.some
hdomain : (↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
⊢ ∀ (x : ↥(↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)

Tactic:
obtain harch := e.orderTop_eq_archimedeanClassMk

Premises used: HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ ∀ (c : M), Membership.mem (α := M) (γ := Submodule K M) ⊤ ((LinearMap.id : (a : M) → M) c : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
refine_1 :
  StrictMono (α := M) (β :=
    ↥{ domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }.domain)
    (⇑(LinearMap.codRestrict ⊤ LinearMap.id ⋯) : (a : M) → ↥⊤)
⊢ StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (⇑(f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
apply hpartial.strictMono.comp

Premises used: HahnEmbedding.IsPartial.strictMono, StrictMono.comp
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
a : M
refine_1 :
  ∀ ⦃b : M⦄,
    a < b →
      LT.lt (α :=
        ↥{ domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }.domain)
        ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) a : ↥⊤)
        ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) b : ↥⊤)
⊢ ∀ ⦃b : M⦄,
    a < b →
      LT.lt (α :=
        ↥{ domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }.domain)
        ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) a : ↥⊤)
        ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) b : ↥⊤)

Tactic:
_
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h_1 : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h_1.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h_1.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h_1.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
a b : M
h : a < b
⊢ LT.lt (α := ↥{ domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }.domain)
    ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) a : ↥⊤)
    ((LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → ↥⊤) b : ↥⊤)

Tactic:
simpa [← Subtype.coe_lt_coe] using h

Premises used: Subtype.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥⊤),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((f : (a : ↥⊤) → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ ∀ (a : M),
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (orderTop.{u_2, u_3} (R := R)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))

Tactic:
simp [harch]
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
a : α
s : Set β
ha : 0 ≤ a
⊢ a • lowerBounds s ⊆ lowerBounds (a • s)

Tactic:
(monotone_smul_left_of_nonneg ha).image_lowerBounds_subset_lowerBounds_image

Premises used: monotone_smul_left_of_nonneg, Monotone.image_lowerBounds_subset_lowerBounds_image
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
a : α
s : Set β
ha : 0 ≤ a
⊢ a • upperBounds s ⊆ upperBounds (a • s)

Tactic:
(monotone_smul_left_of_nonneg ha).image_upperBounds_subset_upperBounds_image

Premises used: Monotone.image_upperBounds_subset_upperBounds_image, monotone_smul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
a : α
s : Set β
hs : BddBelow s
ha : 0 ≤ a
⊢ BddBelow (a • s)

Tactic:
(monotone_smul_left_of_nonneg ha).map_bddBelow hs

Premises used: monotone_smul_left_of_nonneg, Monotone.map_bddBelow
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
a : α
s : Set β
hs : BddAbove s
ha : 0 ≤ a
⊢ BddAbove (a • s)

Tactic:
(monotone_smul_left_of_nonneg ha).map_bddAbove hs

Premises used: monotone_smul_left_of_nonneg, Monotone.map_bddAbove
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : GroupWithZero α
inst_3 : Zero β
inst_4 : MulActionWithZero α β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
s : Set β
a : α
ha : 0 < a
⊢ lowerBounds (a • s) = a • lowerBounds s

Tactic:
(OrderIso.smulRight ha).lowerBounds_image

Premises used: OrderIso.lowerBounds_image, OrderIso.smulRight
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : GroupWithZero α
inst_3 : Zero β
inst_4 : MulActionWithZero α β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
s : Set β
a : α
ha : 0 < a
⊢ upperBounds (a • s) = a • upperBounds s

Tactic:
(OrderIso.smulRight ha).upperBounds_image

Premises used: OrderIso.upperBounds_image, OrderIso.smulRight
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : GroupWithZero α
inst_3 : Zero β
inst_4 : MulActionWithZero α β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
s : Set β
a : α
ha : 0 < a
⊢ BddBelow (a • s) ↔ BddBelow s

Tactic:
(OrderIso.smulRight ha).bddBelow_image

Premises used: OrderIso.bddBelow_image, OrderIso.smulRight
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : GroupWithZero α
inst_3 : Zero β
inst_4 : MulActionWithZero α β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
s : Set β
a : α
ha : 0 < a
⊢ BddAbove (a • s) ↔ BddAbove s

Tactic:
(OrderIso.smulRight ha).bddAbove_image

Premises used: OrderIso.bddAbove_image, OrderIso.smulRight
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a ≤ 0
⊢ a • lowerBounds s ⊆ upperBounds (a • s)

Tactic:
(antitone_smul_left ha).image_lowerBounds_subset_upperBounds_image

Premises used: antitone_smul_left, Antitone.image_lowerBounds_subset_upperBounds_image
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a ≤ 0
⊢ a • upperBounds s ⊆ lowerBounds (a • s)

Tactic:
(antitone_smul_left ha).image_upperBounds_subset_lowerBounds_image

Premises used: antitone_smul_left, Antitone.image_upperBounds_subset_lowerBounds_image
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a ≤ 0
hs : BddBelow s
⊢ BddAbove (a • s)

Tactic:
(antitone_smul_left ha).map_bddBelow hs

Premises used: antitone_smul_left, Antitone.map_bddBelow
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a ≤ 0
hs : BddAbove s
⊢ BddBelow (a • s)

Tactic:
(antitone_smul_left ha).map_bddAbove hs

Premises used: antitone_smul_left, Antitone.map_bddAbove
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a < 0
⊢ lowerBounds (a • s) = a • upperBounds s

Tactic:
(OrderIso.smulRightDual β ha).upperBounds_image

Premises used: OrderIso.smulRightDual, lowerBounds, Set.Mem, setOf, OrderIso.upperBounds_image, OrderDual
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a < 0
⊢ upperBounds (a • s) = a • lowerBounds s

Tactic:
(OrderIso.smulRightDual β ha).lowerBounds_image

Premises used: OrderIso.smulRightDual, Set.Mem, setOf, upperBounds, OrderIso.lowerBounds_image, OrderDual
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a < 0
⊢ BddBelow (a • s) ↔ BddAbove s

Tactic:
(OrderIso.smulRightDual β ha).bddAbove_image

Premises used: OrderIso.bddAbove_image, OrderIso.smulRightDual, lowerBounds, Set.Mem, setOf, BddBelow, OrderDual
-- Module: Mathlib.Algebra.Order.Module.Pointwise
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
s : Set β
a : α
ha : a < 0
⊢ BddAbove (a • s) ↔ BddBelow s

Tactic:
(OrderIso.smulRightDual β ha).bddBelow_image

Premises used: OrderIso.smulRightDual, Set.Mem, setOf, upperBounds, BddAbove, OrderDual, OrderIso.bddBelow_image
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ α
inst_2 : MulAction ℚ≥0 α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
rw : HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ ≤ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂
⊢ _q • _a₁ ≤ _q • _a₂

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]

Premises used: Rat, NNRat.cast_smul_eq_nnqsmul
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ α
inst_2 : MulAction ℚ≥0 α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ ≤ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂

Tactic:
smul_le_smul_of_nonneg_left (α := ℚ) ha hq

Premises used: smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ α
inst_2 : MulAction ℚ≥0 α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ ≤ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂

Tactic:
exact smul_le_smul_of_nonneg_left (α := ℚ) ha hq

Premises used: smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ≥0 α
inst_2 : MulAction ℚ α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
rw : HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ < HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂
⊢ _q • _a₁ < _q • _a₂

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]

Premises used: Rat, NNRat.cast_smul_eq_nnqsmul
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ≥0 α
inst_2 : MulAction ℚ α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ < HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂

Tactic:
smul_lt_smul_of_pos_left (α := ℚ) ha hq

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ≥0 α
inst_2 : MulAction ℚ α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ < HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂

Tactic:
exact smul_lt_smul_of_pos_left (α := ℚ) ha hq

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : DistribMulAction ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
inl : ∀ (ha : a ≤ 0), |q • a| = q • |a|
inr : ∀ (ha : 0 ≤ a), |q • a| = q • |a|
⊢ |q • a| = q • |a|

Tactic:
obtain ha | ha := le_total a 0

Premises used: le_total, OfNat.ofNat