-- 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:
case memc
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)

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

case addc
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:
case memc =>
  intro c' hc'
  obtain ⟨z, hz⟩ := hc'
  obtain ⟨y, hy⟩ := hx
  apply AddSubmonoid.subset_closure
  refine ⟨z • y, ?_⟩
  simp only [star_smul, smul_mul_smul_comm, hz, hy]

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

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

Proof state:
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)

Tactic:
case mem =>
  intro x hx
  have hc := le_of_lt hc
  rw [StarOrderedRing.nonneg_iff] at hc
  refine AddSubmonoid.closure_induction ?memc ?zeroc ?addc hc
  case memc =>
    intro c' hc'
    obtain ⟨z, hz⟩ := hc'
    obtain ⟨y, hy⟩ := hx
    apply AddSubmonoid.subset_closure
    refine ⟨z • y, ?_⟩
    simp only [star_smul, smul_mul_smul_comm, hz, hy]
  case zeroc => simpa only [zero_smul] using zero_mem _
  case addc => exact fun c' d _ _ ↦ by simpa only [add_smul] using add_mem

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