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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n ↔ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]
case mp
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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n → n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }

case mpr
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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) } → finrank k { x // x ∈ vectorSpan k (Set.range p) } = 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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n ↔ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
constructor
case mp
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
inst✝ : Fintype ι
p : ι → P
hc : Fintype.card ι = finrank k { x // x ∈ vectorSpan k (Set.range p) } + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
case mp
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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n → n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
rintro rfl
no goals
case mp
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
inst✝ : Fintype ι
p : ι → P
hc : Fintype.card ι = finrank k { x // x ∈ vectorSpan k (Set.range p) } + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
rfl
no goals
case mpr
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
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) } → finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
exact fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle