-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_le_star_iff {x y : R} : star x ≤ star y ↔ x ≤ y

Proof state:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ (range fun s => star s * s) ⊆ ⇑starAddEquiv ⁻¹' range fun s => star s * s

Tactic:
rintro - ⟨s, rfl⟩

Result:
case intro.intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
s : R
⊢ (fun s => star s * s) s ∈ ⇑starAddEquiv ⁻¹' range fun s => star s * s

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ ∀ (x y : R), x ≤ y → star x ≤ star y

Tactic:
intro x y h

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : x ≤ y
⊢ star x ≤ star y

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
s : R
⊢ (fun s => star s * s) s = starAddEquiv ((fun s => star s * s) s)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : x ≤ y
⊢ star x ≤ star y

Tactic:
rw [StarOrderedRing.le_iff] at h ⊢

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star y = star x + p

Proof state:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ starAddEquiv d ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd

Result:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ (range fun s => star s * s) ⊆ ⇑starAddEquiv ⁻¹' range fun s => star s * s

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star y = star x + p

Tactic:
obtain ⟨d, hd, rfl⟩ := h

Result:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star (x + d) = star x + p

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ star x ≤ star y ↔ x ≤ y

Tactic:
suffices ∀ x y, x ≤ y → star x ≤ star y from
  ⟨by simpa only [star_star] using this (star x) (star y), this x y⟩

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ ∀ (x y : R), x ≤ y → star x ≤ star y

Proof state:
case intro.intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
s : R
⊢ (fun s => star s * s) s ∈ ⇑starAddEquiv ⁻¹' range fun s => star s * s

Tactic:
exact ⟨s, by simp⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star (x + d) = star x + p

Tactic:
refine ⟨starAddEquiv d, ?_, star_add _ _⟩

Result:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ starAddEquiv d ∈ AddSubmonoid.closure (range fun s => star s * s)

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
this : ∀ (x y : R), x ≤ y → star x ≤ star y
⊢ star x ≤ star y → x ≤ y

Tactic:
simpa only [star_star] using this (star x) (star y)

Result:
no goals