k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ affineSpan k ↑(Finset.image p s) = sp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k ↑(Finset.image p s) = sp
have hn : s.Nonempty := by
  rw [← Finset.card_pos, hc]
  apply Nat.succ_pos
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ affineSpan k ↑(Finset.image p s) = sp
refine' eq_of_direction_eq_of_nonempty_of_le _ ((hn.image p).to_set.affineSpan k) hle
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : direction (affineSpan k ↑(Finset.image p s)) ≤ direction sp
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
have hd := direction_le hle
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : vectorSpan k ↑(Finset.image p s) ≤ direction sp
⊢ vectorSpan k ↑(Finset.image p s) = direction sp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : direction (affineSpan k ↑(Finset.image p s)) ≤ direction sp
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
rw [direction_affineSpan] at hd⊢
no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : vectorSpan k ↑(Finset.image p s) ≤ direction sp
⊢ vectorSpan k ↑(Finset.image p s) = direction sp
exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ 0 < finrank k { x // x ∈ direction sp } + 1
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ Finset.Nonempty s
rw [← Finset.card_pos, hc]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ 0 < finrank k { x // x ∈ direction sp } + 1
apply Nat.succ_pos