[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle : x ≤ y
z : R
⊢ z + x ≤ z + y
[PROOFSTEP]
rw [StarOrderedRing.le_iff] at hle ⊢
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z : R
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + y = z + x + p
[PROOFSTEP]
refine hle.imp fun s hs ↦ ?_
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + y = z + x + s
[PROOFSTEP]
rw [hs.2, add_assoc]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + (x + s) = z + (x + s)
[PROOFSTEP]
exact ⟨hs.1, rfl⟩
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
obtain ⟨p, hp⟩ := (h_le_iff x y).mp h
[GOAL]
case refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩
[GOAL]
case refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ (∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p) → x ≤ y
[PROOFSTEP]
rintro ⟨p, hp, hpxy⟩
[GOAL]
case refine'_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hpxy : y = x + p
⊢ x ≤ y
[PROOFSTEP]
revert x y hpxy
[GOAL]
case refine'_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x y : R), y = x + p → x ≤ y
[PROOFSTEP]
refine' AddSubmonoid.closure_induction hp _ (fun x y h => add_zero x ▸ h.ge) _
[GOAL]
case refine'_2.intro.intro.refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x : R), (x ∈ Set.range fun s => star s * s) → ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ x y rfl
[GOAL]
case refine'_2.intro.intro.refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
s x : R
⊢ x ≤ x + (fun s => star s * s) s
[PROOFSTEP]
exact (h_le_iff _ _).mpr ⟨s, rfl⟩
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x y : R),
    (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
      (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1
[PROOFSTEP]
rintro a b ha hb x y rfl
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a b : R
ha : ∀ (x y : R), y = x + a → x ≤ y
hb : ∀ (x y : R), y = x + b → x ≤ y
x : R
⊢ x ≤ x + (a + b)
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a b : R
ha : ∀ (x y : R), y = x + a → x ≤ y
hb : ∀ (x y : R), y = x + b → x ≤ y
x : R
⊢ x ≤ x + a + b
[PROOFSTEP]
exact (ha _ _ rfl).trans (hb _ _ rfl)
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
x y : R
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
x y : R
this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
[PROOFSTEP]
haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
[PROOFSTEP]
simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x : R
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
simp only [le_iff, zero_add, exists_eq_right']
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
r : R
⊢ 0 ≤ r * star r
[PROOFSTEP]
simpa only [star_star] using star_mul_self_nonneg (star r)
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c
[PROOFSTEP]
rw [StarOrderedRing.nonneg_iff] at ha 
[GOAL]
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
[PROOFSTEP]
refine' AddSubmonoid.closure_induction ha (fun x hx => _) (by rw [mul_zero, zero_mul]) fun x y hx hy => _
[GOAL]
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
[PROOFSTEP]
rw [mul_zero, zero_mul]
[GOAL]
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
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hx
[GOAL]
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
[PROOFSTEP]
convert star_mul_self_nonneg (x * c) using 1
[GOAL]
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)
[PROOFSTEP]
rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
rw [add_zero]
[GOAL]
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
[PROOFSTEP]
exact hx
[GOAL]
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
[PROOFSTEP]
rw [mul_add, add_mul]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ c * a * star c
[PROOFSTEP]
simpa only [star_star] using conjugate_nonneg ha (star c)
[GOAL]
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
[PROOFSTEP]
rw [StarOrderedRing.le_iff] at hab ⊢
[GOAL]
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
[PROOFSTEP]
obtain ⟨p, hp, rfl⟩ := hab
[GOAL]
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
[PROOFSTEP]
simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
[GOAL]
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
[PROOFSTEP]
exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩
[GOAL]
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
[PROOFSTEP]
simp only [add_mul, mul_add]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c
[PROOFSTEP]
simpa only [star_star] using conjugate_le_conjugate hab (star c)
