case intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Set P
b : AffineBasis (↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
⊢ Nonempty (AffineBasis ι k P)
obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
case intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Set P
b : AffineBasis (↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
lift s to Finset P using b.finite_set
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Fintype.card ↑↑s = Fintype.card ι
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
refine' ⟨b.reindex <| Fintype.equivOfCardEq _⟩
no goals
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Fintype.card ↑↑s = Fintype.card ι
rw [h, ← b.card_eq_finrank_add_one]