-- 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
⊢ 0 < c • (b - a)

Tactic:
refine lt_of_le_of_ne ?le ?ne

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

case ne
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)
c' d : R
x✝¹ : c' ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ c' • x ∈ AddSubmonoid.closure (range fun s => star s * s) →
    d • x ∈ AddSubmonoid.closure (range fun s => star s * s) →
      (c' + d) • x ∈ AddSubmonoid.closure (range fun s => star s * s)

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

Tactic:
refine AddSubmonoid.closure_induction ?memc ?zeroc ?addc hc

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

Proof state:
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 addc => exact fun c' d _ _ ↦ by simpa only [add_smul] using add_mem

Result:
no goals

Proof state:
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
⊢ (fun s => star s * s) (z • y) = c' • x

Tactic:
simp only [star_smul, smul_mul_smul_comm, hz, hy]

Result:
no goals