no goals
ι : Type ?u.1132782
ι' : Type ?u.1132785
R : Type ?u.1132788
R₂ : Type ?u.1132791
K : Type u_1
M : Type ?u.1132797
M' : Type ?u.1132800
M'' : Type ?u.1132803
V : Type u
V' : Type ?u.1132808
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndependent K Subtype.val
⊢ range ↑(extend hs) = LinearIndependent.extend hs (_ : s ⊆ univ)
rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]