k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
⊢ vectorSpan k s = ⊤ → affineSpan k s = ⊤
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
refine' ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, _⟩
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
⊢ affineSpan k s = ⊤
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
⊢ vectorSpan k s = ⊤ → affineSpan k s = ⊤
intro h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
⊢ Nonempty { x // x ∈ affineSpan k s }
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
⊢ affineSpan k s = ⊤
suffices Nonempty (affineSpan k s) by
  obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
  rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h : vectorSpan k s = ⊤
x : P
hx : x ∈ s
⊢ Nonempty { x // x ∈ affineSpan k s }
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
⊢ Nonempty { x // x ∈ affineSpan k s }
obtain ⟨x, hx⟩ := hs
no goals
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h : vectorSpan k s = ⊤
x : P
hx : x ∈ s
⊢ Nonempty { x // x ∈ affineSpan k s }
exact ⟨⟨x, mem_affineSpan k hx⟩⟩
case intro.mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
p : P
hp : p ∈ affineSpan k s
⊢ affineSpan k s = ⊤
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
this : Nonempty { x // x ∈ affineSpan k s }
⊢ affineSpan k s = ⊤
obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
no goals
case intro.mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
hs : Set.Nonempty s
h : vectorSpan k s = ⊤
p : P
hp : p ∈ affineSpan k s
⊢ affineSpan k s = ⊤
rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]