R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab✝ : a ≤ b
hab : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ b = a + p
c : R
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * b * c = star c * a * c + p
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ star c * a * c ≤ star c * b * c
rw [StarOrderedRing.le_iff] at hab ⊢
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hab : a ≤ a + p
⊢ ∃ p_1, p_1 ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * (a + p) * c = star c * a * c + p_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab✝ : a ≤ b
hab : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ b = a + p
c : R
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * b * c = star c * a * c + p
obtain ⟨p, hp, rfl⟩ := hab
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hab : a ≤ a + p
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hab : a ≤ a + p
⊢ ∃ p_1, p_1 ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * (a + p) * c = star c * a * c + p_1
simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
no goals
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hab : a ≤ a + p
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩
no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hab : a ≤ a + p
hp : 0 ≤ p
⊢ star c * (a + p) * c = star c * a * c + star c * p * c
simp only [add_mul, mul_add]