case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ Maximal i → ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j

case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → Maximal i
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ Maximal i ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
constructor
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : Maximal i
⊢ Surjective j
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ Maximal i → ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
rintro p κ w i' j rfl
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : Maximal i
⊢ Surjective j
specialize p (range w) i'.coe_range (range_comp_subset_range _ _)
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j
rw [range_comp, ← @image_univ _ _ w] at p
no goals
case mp
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
exact range_iff_surjective.mp (image_injective.mpr i'.injective p)
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
⊢ range v = w
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → Maximal i
intro p w i' h
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
⊢ range v = w
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
⊢ range v = w
specialize
  p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
    (by
      ext
      simp)
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q :
  (fun s => Subtype.val '' s) (range fun i => { val := v i, property := (_ : v i ∈ w) }) =
    (fun s => Subtype.val '' s) univ
⊢ range v = w
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
⊢ range v = w
have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q : (Subtype.val '' range fun i => { val := v i, property := (_ : v i ∈ w) }) = Subtype.val '' univ
⊢ range v = w
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q :
  (fun s => Subtype.val '' s) (range fun i => { val := v i, property := (_ : v i ∈ w) }) =
    (fun s => Subtype.val '' s) univ
⊢ range v = w
dsimp at q
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q : (fun x => ↑{ val := v x, property := (_ : v x ∈ w) }) '' univ = Subtype.val '' univ
⊢ range v = w
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q : (Subtype.val '' range fun i => { val := v i, property := (_ : v i ∈ w) }) = Subtype.val '' univ
⊢ range v = w
rw [← image_univ, image_image] at q
no goals
case mpr
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => { val := v i, property := (_ : v i ∈ w) }
q : (fun x => ↑{ val := v x, property := (_ : v x ∈ w) }) '' univ = Subtype.val '' univ
⊢ range v = w
simpa using q
case h
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
x✝ : ι
⊢ (Subtype.val ∘ fun i => { val := v i, property := (_ : v i ∈ w) }) x✝ = v x✝
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
⊢ (Subtype.val ∘ fun i => { val := v i, property := (_ : v i ∈ w) }) = v
ext
no goals
case h
ι✝ : Type u'
ι' : Type ?u.321729
R✝ : Type ?u.321732
K : Type ?u.321735
M✝ : Type ?u.321738
M' : Type ?u.321741
M'' : Type ?u.321744
V : Type u
V' : Type ?u.321749
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✝
ι : Type w
R : Type u
inst✝³ : Ring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
x✝ : ι
⊢ (Subtype.val ∘ fun i => { val := v i, property := (_ : v i ∈ w) }) x✝ = v x✝
simp