ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
⊢ s = t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
⊢ s = t
let f : t ↪ s :=
  ⟨fun x => ⟨x.1, h x.2⟩, fun a b hab => Subtype.coe_injective (Subtype.mk.inj hab)⟩
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s = t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
⊢ s = t
have h_surj : Surjective f := by
  apply surjective_of_linearIndependent_of_span hs f _
  convert hst <;> simp [comp]
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s = t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s = t
show s = t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
⊢ (range fun x => ↑x) ⊆ ↑(span R (range ((fun x => ↑x) ∘ ↑f)))
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
⊢ Surjective ↑f
apply surjective_of_linearIndependent_of_span hs f _
no goals
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
⊢ (range fun x => ↑x) ⊆ ↑(span R (range ((fun x => ↑x) ∘ ↑f)))
convert hst <;> simp [comp]
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s ⊆ t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s = t
apply Subset.antisymm _ h
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
⊢ x ∈ t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
⊢ s ⊆ t
intro x hx
case intro
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y✝ : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
y : ↑t
hy : ↑f y = { val := x, property := hx }
⊢ x ∈ t
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
⊢ x ∈ t
rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩
case h.e'_4
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y✝ : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
y : ↑t
hy : ↑f y = { val := x, property := hx }
⊢ x = ↑y
case intro
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y✝ : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
y : ↑t
hy : ↑f y = { val := x, property := hx }
⊢ x ∈ t
convert y.mem
no goals
case h.e'_4
ι : Type u'
ι' : Type ?u.605779
R : Type u_1
K : Type ?u.605785
M : Type u_2
M' : Type ?u.605791
M'' : Type ?u.605794
V : Type u
V' : Type ?u.605799
v : ι → M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
a b : R
x✝ y✝ : M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndependent R fun x => ↑x
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s :=
  { toFun := fun x => { val := ↑x, property := (_ : ↑x ∈ s) },
    inj' :=
      (_ :
        ∀ (a b : ↑t),
          (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) a = (fun x => { val := ↑x, property := (_ : ↑x ∈ s) }) b →
            a = b) }
h_surj : Surjective ↑f
x : M
hx : x ∈ s
y : ↑t
hy : ↑f y = { val := x, property := hx }
⊢ x = ↑y
rw [← Subtype.mk.inj hy]