R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c : R
⊢ 0 ≤ star c * a * c
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c
rw [StarOrderedRing.nonneg_iff] at ha
case refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
hx : x ∈ Set.range fun s => star s * s
⊢ 0 ≤ star c * x * c

case refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * (x + y) * c
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c : R
⊢ 0 ≤ star c * a * c
refine' AddSubmonoid.closure_induction ha (fun x hx => _)
  (by rw [MulZeroClass.mul_zero, MulZeroClass.zero_mul]) fun x y hx hy => _
no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c : R
⊢ 0 ≤ star c * 0 * c
rw [MulZeroClass.mul_zero, MulZeroClass.zero_mul]
case refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ 0 ≤ star c * (fun s => star s * s) x * c
case refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
hx : x ∈ Set.range fun s => star s * s
⊢ 0 ≤ star c * x * c
obtain ⟨x, rfl⟩ := hx
case h.e'_4
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ star c * (fun s => star s * s) x * c = star (x * c) * (x * c)
case refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ 0 ≤ star c * (fun s => star s * s) x * c
convert star_mul_self_nonneg (x * c) using 1
no goals
case h.e'_4
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ star c * (fun s => star s * s) x * c = star (x * c) * (x * c)
rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
no goals
case refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * (x + y) * c
calc
  0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
  _ ≤ star c * x * c + star c * y * c := add_le_add_left hy _
  _ ≤ _ := by rw [mul_add, add_mul]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c + 0
rw [add_zero]
no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c
exact hx
no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c
rw [mul_add, add_mul]