-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c

Proof state:
case refine_1.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
⊢ 0 ≤ star c * (fun s => star s * s) x * c

Tactic:
convert star_mul_self_nonneg (x * c) using 1

Result:
case h.e'_4
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
⊢ star c * (fun s => star s * s) x * c = star (x * c) * (x * c)

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
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

Tactic:
rw [mul_add, add_mul]

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c : R
⊢ 0 ≤ star c * 0 * c

Tactic:
rw [mul_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c : R
⊢ 0 ≤ star c * a * c

Tactic:
refine AddSubmonoid.closure_induction (fun x hx => ?_)
  (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha

Result:
case refine_1
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
hx : x ∈ range fun s => star s * s
⊢ 0 ≤ star c * x * c

case refine_2
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * (x + y) * c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c : R
⊢ 0 ≤ star c * a * c

Proof state:
case h.e'_4
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
⊢ star c * (fun s => star s * s) x * c = star (x * c) * (x * c)

Tactic:
rw [star_mul, ← mul_assoc, mul_assoc _ _ c]

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c

Tactic:
exact hx

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * (x + y) * c

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

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c + 0

Tactic:
rw [add_zero]

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s => star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s => star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c

Proof state:
case refine_1
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
hx : x ∈ range fun s => star s * s
⊢ 0 ≤ star c * x * c

Tactic:
obtain ⟨x, rfl⟩ := hx

Result:
case refine_1.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)
c x : R
⊢ 0 ≤ star c * (fun s => star s * s) x * c