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

Tactic:
refine AddSubmonoid.closure_induction ?mem ?zero ?add hab

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

case zero
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)
⊢ c • 0 ∈ AddSubmonoid.closure (range fun s => star s * s)

case add
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)

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

Tactic:
simpa only [smul_zero] using zero_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 : 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)

Tactic:
obtain ⟨z, hz⟩ := hc'

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