k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hn : Finset.Nonempty (Finset.image p s)
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
have hn : (s.image p).Nonempty := by
  rw [Finset.Nonempty.image_iff, ← Finset.card_pos, hc]
  apply Nat.succ_pos
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hn : Finset.Nonempty (Finset.image p s)
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
rcases hn with ⟨p₁, hp₁⟩
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ Submodule.span k ↑(Finset.image (fun x => x -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) } ≤ n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image (fun p => p -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) ≤ n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ Submodule.span k ↑(Finset.image (fun x => x -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) } ≤ n
refine' le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) _
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image p s) ≤ Finset.card s
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image (fun p => p -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) ≤ n
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁,
  tsub_le_iff_right, ← hc]
no goals
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image p s) ≤ Finset.card s
apply Finset.card_image_le
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ 0 < n + 1
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ Finset.Nonempty (Finset.image p s)
rw [Finset.Nonempty.image_iff, ← Finset.card_pos, hc]
no goals
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ 0 < n + 1
apply Nat.succ_pos