[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A B : Subspace K V
⊢ A.carrier = B.carrier → A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : Subspace K V
carrier✝ : Set (ℙ K V)
mem_add'✝ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝ →
      Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝
⊢ { carrier := carrier✝, mem_add' := mem_add'✝ }.carrier = B.carrier →
    { carrier := carrier✝, mem_add' := mem_add'✝ } = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
carrier✝¹ : Set (ℙ K V)
mem_add'✝¹ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝¹ →
      Projectivization.mk K w hw ∈ carrier✝¹ → Projectivization.mk K (v + w) hvw ∈ carrier✝¹
carrier✝ : Set (ℙ K V)
mem_add'✝ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝ →
      Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝
⊢ { carrier := carrier✝¹, mem_add' := mem_add'✝¹ }.carrier = { carrier := carrier✝, mem_add' := mem_add'✝ }.carrier →
    { carrier := carrier✝¹, mem_add' := mem_add'✝¹ } = { carrier := carrier✝, mem_add' := mem_add'✝ }
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
⊢ A ≤ ↑B → span A ≤ B
[PROOFSTEP]
intro h x hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
hx : x ∈ span A
⊢ x ∈ B
[PROOFSTEP]
induction' hx with y hy
[GOAL]
case of
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x y : ℙ K V
hy : y ∈ A
⊢ y ∈ B
[PROOFSTEP]
apply h
[GOAL]
case of.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x y : ℙ K V
hy : y ∈ A
⊢ y ∈ A
[PROOFSTEP]
assumption
[GOAL]
case mem_add
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K (v✝ + w✝) hvw✝ ∈ B
[PROOFSTEP]
apply B.mem_add
[GOAL]
case mem_add.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K v✝ ?mem_add.hv ∈ B
case mem_add.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K w✝ ?mem_add.hw ∈ B
case mem_add.hv
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ v✝ ≠ 0
case mem_add.hw
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ w✝ ≠ 0
[PROOFSTEP]
assumption'
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
t : Set (ℙ K V)
⊢ t ∈ SetLike.coe '' A → Projectivization.mk K (v + w) hvw ∈ t
[PROOFSTEP]
rintro ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
s : Subspace K V
hs : s ∈ A
⊢ Projectivization.mk K (v + w) hvw ∈ ↑s
[PROOFSTEP]
exact s.mem_add v w hv hw _ (h1 s ⟨s, hs, rfl⟩) (h2 s ⟨s, hs, rfl⟩)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
⊢ ∀ (s : Set (Subspace K V)), IsGLB s (sInf s)
[PROOFSTEP]
refine fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Set (ℙ K V)
⊢ E ∈ SetLike.coe '' s → x ∈ E
[PROOFSTEP]
rintro ⟨E, hE, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ ↑E
[PROOFSTEP]
exact ha hE hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ span Set.univ = ⊤
[PROOFSTEP]
rw [eq_top_iff, SetLike.le_def]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
[PROOFSTEP]
intro x _hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ℙ K V
_hx : x ∈ ⊤
⊢ x ∈ span Set.univ
[PROOFSTEP]
exact subset_span _ (Set.mem_univ x)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span (↑W ∪ S)
[PROOFSTEP]
rw [span_union, span_coe]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span (S ∪ ↑W)
[PROOFSTEP]
rw [span_union, span_coe]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W
[PROOFSTEP]
simp_rw [← span_le_subspace_iff]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
[PROOFSTEP]
exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
⊢ span S = sInf {W | S ⊆ ↑W}
[PROOFSTEP]
ext x
[GOAL]
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier
[PROOFSTEP]
simp_rw [mem_carrier_iff, mem_span x]
[GOAL]
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}
[PROOFSTEP]
refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
[GOAL]
case carrier.h.refine_1
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}
[PROOFSTEP]
rintro W ⟨T, hT, rfl⟩
[GOAL]
case carrier.h.refine_1.intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
T : Subspace K V
hT : T ∈ {W | S ⊆ ↑W}
⊢ x ∈ ↑T
[PROOFSTEP]
exact hx T hT
[GOAL]
case carrier.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W
[PROOFSTEP]
exact (@sInf_le _ _ {W : Subspace K V | S ⊆ ↑W} W hW) hx
