-- Mathlib/Algebra/Order/Star/Basic.lean
lemma StarModule.smul_lt_smul_of_pos {a b : A} {c : R} (hab : a < b) (hc : 0 < c) :
    c • a < c • b

Proof state:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x y : A),
    x ∈ AddSubmonoid.closure (range fun s => star s * s) →
      y ∈ AddSubmonoid.closure (range fun s => star s * s) →
        c • x ∈ AddSubmonoid.closure (range fun s => star s * s) →
          c • y ∈ AddSubmonoid.closure (range fun s => star s * s) →
            c • (x + y) ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
exact fun x y _ _ ↦ by simpa only [smul_add] using add_mem

Result:
no goals

Proof state:
case intro.intro
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc✝ : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
x : A
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
c' z : R
hz : (fun s => star s * s) z = c'
y : A
hy : (fun s => star s * s) y = x
⊢ c' • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
apply AddSubmonoid.subset_closure

Result:
case intro.intro.a
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc✝ : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
x : A
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
c' z : R
hz : (fun s => star s * s) z = c'
y : A
hy : (fun s => star s * s) y = x
⊢ c' • x ∈ range fun s => star s * s

Proof state:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab : 0 < b - a
hc : 0 < c
⊢ 0 < c • b - c • a

Tactic:
rw [← smul_sub]

Result:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab : 0 < b - a
hc : 0 < c
⊢ 0 < c • (b - a)

Proof state:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc✝ : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
x : A
hx : x ∈ range fun s => star s * s
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ (x_1 y : R),
    x_1 ∈ AddSubmonoid.closure (range fun s => star s * s) →
      y ∈ AddSubmonoid.closure (range fun s => star s * s) →
        x_1 • x ∈ AddSubmonoid.closure (range fun s => star s * s) →
          y • x ∈ AddSubmonoid.closure (range fun s => star s * s) →
            (x_1 + y) • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
exact fun c' d _ _ ↦ by simpa only [add_smul] using add_mem

Result:
no goals

Proof state:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∀ x ∈ range fun s => star s * s, c • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
intro x hx

Result:
R : Type u
A : Type u_1
inst✝¹² : Semiring R
inst✝¹¹ : PartialOrder R
inst✝¹⁰ : StarRing R
inst✝⁹ : StarOrderedRing R
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : NoZeroSMulDivisors R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
c : R
hab✝ : 0 < b - a
hc : 0 < c
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
x : A
hx : x ∈ range fun s => star s * s
⊢ c • x ∈ AddSubmonoid.closure (range fun s => star s * s)