case intro.intro.intro
ι : Type ?u.183706
ι' : Type ?u.183709
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ∃ s x b, ↑b = Subtype.val
ι : Type ?u.183706
ι' : Type ?u.183709
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
⊢ ∃ s x b, ↑b = Subtype.val
obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t
case intro.intro.intro
ι : Type ?u.183706
ι' : Type ?u.183709
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ affineSpan k (range Subtype.val) = ⊤
case intro.intro.intro
ι : Type ?u.183706
ι' : Type ?u.183709
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ∃ s x b, ↑b = Subtype.val
refine' ⟨s, hst, ⟨(↑), h_ind, _⟩, rfl⟩
no goals
case intro.intro.intro
ι : Type ?u.183706
ι' : Type ?u.183709
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ affineSpan k (range Subtype.val) = ⊤
rw [Subtype.range_coe, h_tot, ht]