no goals
ι : Type ?u.534033
ι' : Type ?u.534036
R : Type u_2
K : Type ?u.534042
A : Type u_1
A' : Type ?u.534048
A'' : Type ?u.534051
V : Type u
V' : Type ?u.534056
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
t s : Set A
h : t ⊆ s
hx : AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
simpa [Function.comp] using hx.comp (inclusion h) (inclusion_injective h)