R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s✝ t : Set A
f : A →ₐ[R] B
s : Set A
⊢ s ⊆ ↑f ⁻¹' ↑(adjoin R ((fun a => ↑f a) '' s))
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s✝ t : Set A
f : A →ₐ[R] B
s : Set A
⊢ (fun x => x) '' s ⊆ (Subalgebra.comap f (adjoin R (↑f '' s))).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
simp only [Set.image_id', coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring,
  Subalgebra.coe_comap]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s✝ t : Set A
f : A →ₐ[R] B
s : Set A
⊢ s ⊆ ↑f ⁻¹' ↑(adjoin R ((fun a => ↑f a) '' s))
exact fun x hx => subset_adjoin ⟨x, hx, rfl⟩