-- Mathlib/Algebra/Order/Star/Basic.lean
lemma NonUnitalStarRingHom.map_le_map_of_map_star (f : R →⋆ₙ+* S) {x y : R} (hxy : x ≤ y) :
    f x ≤ f y

Proof state:
case intro.intro.mul
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
aesop

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ f p ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
have hf : ∀ r, f (star r) = star (f r) := map_star _

Result:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f p ∈ AddSubmonoid.closure (range fun s => star s * s)

Proof state:
case intro.intro.mem
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ : R
h✝ : x✝ ∈ range fun s => star s * s
⊢ f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)

case intro.intro.one
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f 0 ∈ AddSubmonoid.closure (range fun s => star s * s)

case intro.intro.mul
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
all_goals aesop

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), f y = f x + p

Tactic:
obtain ⟨p, hp, rfl⟩ := hxy

Result:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), f (x + p) = f x + p_1

Proof state:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f p ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
induction hp using AddSubmonoid.closure_induction

Result:
case intro.intro.mem
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ : R
h✝ : x✝ ∈ range fun s => star s * s
⊢ f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)

case intro.intro.one
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f 0 ∈ AddSubmonoid.closure (range fun s => star s * s)

case intro.intro.mul
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s => star s * s)

Proof state:
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
rw [StarOrderedRing.le_iff] at hxy ⊢

Result:
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), f y = f x + p

Proof state:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), f (x + p) = f x + p_1

Tactic:
refine ⟨f p, ?_, map_add f _ _⟩

Result:
case intro.intro
R : Type u_2
S : Type u_3
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ f p ∈ AddSubmonoid.closure (range fun s => star s * s)