-- 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 : A
hx : x ∈ range fun s => star s * s
hc : 0 ≤ c
⊢ c • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
rw [StarOrderedRing.nonneg_iff] at hc

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
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ c • x ∈ AddSubmonoid.closure (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 - a)

Tactic:
refine (smul_ne_zero ?_ ?_).symm

Result:
case refine_1
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
⊢ c ≠ 0

case refine_2
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
⊢ b - a ≠ 0

Proof state:
case 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
hx : x ∈ range fun s => star s * s
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
c' z : R
hz : (fun s => star s * s) z = c'
⊢ c' • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
obtain ⟨y, hy⟩ := hx

Result:
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)

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 - a)

Tactic:
have hab := le_of_lt hab

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 : 0 ≤ b - a
⊢ 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 ∈ range fun s => star s * s, x_1 • x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
intro c' hc'

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
hc : c ∈ AddSubmonoid.closure (range fun s => star s * s)
c' : R
hc' : c' ∈ range fun s => star s * s
⊢ c' • x ∈ AddSubmonoid.closure (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
hab : b - a ∈ AddSubmonoid.closure (range fun s => star s * s)
x y : A
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : 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:
simpa only [smul_add] using add_mem

Result:
no goals