-- Mathlib/Algebra/Order/Ring/Star.lean
private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrder R]
    [StarRing R] [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b

Proof state:
case mem.intro
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x : R
⊢ star x * a * x ≤ star x * b * x

Tactic:
exact conjugate_le_conjugate hab x

Result:
no goals

Proof state:
case mem.intro
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x : R
⊢ (fun s => star s * s) x * a ≤ (fun s => star s * s) x * b

Tactic:
simp_rw [mul_assoc, mul_comm x, ← mul_assoc]

Result:
case mem.intro
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x : R
⊢ star x * a * x ≤ star x * b * x

Proof state:
case one
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
⊢ 0 * a ≤ 0 * b

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
hc : 0 ≤ c
⊢ c * a ≤ c * b

Tactic:
rw [StarOrderedRing.nonneg_iff] at hc

Result:
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
hc : c ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ c * a ≤ c * b

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
hc : c ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ c * a ≤ c * b

Tactic:
induction hc using AddSubmonoid.closure_induction with
| mem _ h =>
  obtain ⟨x, rfl⟩ := h
  simp_rw [mul_assoc, mul_comm x, ← mul_assoc]
  exact conjugate_le_conjugate hab x
| one => simp
| mul x hx y hy =>
  simp only [← nonneg_iff, add_mul] at hx hy ⊢
  apply add_le_add <;> aesop

Result:
no goals

Proof state:
case mem
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x✝ : R
h : x✝ ∈ Set.range fun s => star s * s
⊢ x✝ * a ≤ x✝ * b

Tactic:
obtain ⟨x, rfl⟩ := h

Result:
case mem.intro
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x : R
⊢ (fun s => star s * s) x * a ≤ (fun s => star s * s) x * b

Proof state:
case mul
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x hx : R
y : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hy : hx ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a✝¹ : x * a ≤ x * b
a✝ : hx * a ≤ hx * b
⊢ (x + hx) * a ≤ (x + hx) * b

Tactic:
simp only [← nonneg_iff, add_mul] at hx hy ⊢

Result:
case mul
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x hx : R
y : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a✝¹ : x * a ≤ x * b
a✝ : hx * a ≤ hx * b
hy : 0 ≤ hx
⊢ x * a + hx * a ≤ x * b + hx * b

Proof state:
case mul
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b c : R
hab : a ≤ b
x hx : R
y : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a✝¹ : x * a ≤ x * b
a✝ : hx * a ≤ hx * b
hy : 0 ≤ hx
⊢ x * a + hx * a ≤ x * b + hx * b

Tactic:
apply add_le_add <;> aesop

Result:
no goals