-- Mathlib/Algebra/Order/Star/Basic.lean
lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y

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

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 : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ IsSelfAdjoint (x + d)

Proof state:
case intro.intro.e_a.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
s : R
⊢ ↑starAddEquiv ((fun s => star s * s) s) = (AddMonoidHom.id R) ((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 : R
h : x ≤ y
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint 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 : R
h : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint y

Proof state:
case intro.intro.e_a
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ EqOn (⇑↑starAddEquiv) (⇑(AddMonoidHom.id R)) (range fun s => star s * s)

Tactic:
rintro - ⟨s, rfl⟩

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

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

Tactic:
rw [IsSelfAdjoint, star_add, hx.star_eq]

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

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

Tactic:
congr

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

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

Tactic:
refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd

Result:
case intro.intro.e_a
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ EqOn (⇑↑starAddEquiv) (⇑(AddMonoidHom.id R)) (range fun s => star s * s)