case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ → Fintype.card ι = finrank k V + 1

case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι = finrank k V + 1 → affineSpan k (Set.range p) = ⊤
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = finrank k V + 1
constructor
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
⊢ Fintype.card ι = finrank k V + 1
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ → Fintype.card ι = finrank k V + 1
intro h_tot
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
⊢ Fintype.card ι = finrank k V + 1
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
⊢ Fintype.card ι = finrank k V + 1
let n := Fintype.card ι - 1
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ Fintype.card ι = finrank k V + 1
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
⊢ Fintype.card ι = finrank k V + 1
have hn : Fintype.card ι = n + 1 :=
  (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
no goals
case mp
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ Fintype.card ι = finrank k V + 1
rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
  ← hi.finrank_vectorSpan hn]
case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k V + 1
⊢ affineSpan k (Set.range p) = ⊤
case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι = finrank k V + 1 → affineSpan k (Set.range p) = ⊤
intro hc
case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k { x // x ∈ direction ⊤ } + 1
⊢ affineSpan k (Set.range p) = ⊤
case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k V + 1
⊢ affineSpan k (Set.range p) = ⊤
rw [← finrank_top, ← direction_top k V P] at hc
no goals
case mpr
k : Type u_1
V : Type u_2
P : Type u_4
ι : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k { x // x ∈ direction ⊤ } + 1
⊢ affineSpan k (Set.range p) = ⊤
exact hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc