no goals
ι✝ : Type ?u.751654
ι' : Type ?u.751657
R : Type u_2
K : Type ?u.751663
A : Type u_3
A' : Type ?u.751669
A'' : Type ?u.751672
V : Type u
V' : Type ?u.751677
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
ι : Type u_1
s : Set ι
f : ι → A
hs : AlgebraicIndependent R fun x => f ↑x
⊢ AlgebraicIndependent R fun x => ↑x
convert AlgebraicIndependent.image_of_comp s f id hs