[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥
[PROOFSTEP]
rw [vectorSpan_def, vsub_empty, Submodule.span_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ vectorSpan k {p} = ⊥
[PROOFSTEP]
simp [vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Set.Nonempty (spanPoints k s) ↔ Set.Nonempty s
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Set.Nonempty (spanPoints k s) → Set.Nonempty s
[PROOFSTEP]
contrapose
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ¬Set.Nonempty s → ¬Set.Nonempty (spanPoints k s)
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ s = ∅ → spanPoints k s = ∅
[PROOFSTEP]
intro h
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : s = ∅
⊢ spanPoints k s = ∅
[PROOFSTEP]
simp [h, spanPoints]
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Set.Nonempty s → Set.Nonempty (spanPoints k s)
[PROOFSTEP]
exact fun h => h.mono (subset_spanPoints _ _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hp : p ∈ spanPoints k s
hv : v ∈ vectorSpan k s
⊢ v +ᵥ p ∈ spanPoints k s
[PROOFSTEP]
rcases hp with ⟨p2, ⟨hp2, ⟨v2, ⟨hv2, hv2p⟩⟩⟩⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p2 : P
hp2 : p2 ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p = v2 +ᵥ p2
⊢ v +ᵥ p ∈ spanPoints k s
[PROOFSTEP]
rw [hv2p, vadd_vadd]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p2 : P
hp2 : p2 ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p = v2 +ᵥ p2
⊢ v + v2 +ᵥ p2 ∈ spanPoints k s
[PROOFSTEP]
exact ⟨p2, hp2, v + v2, (vectorSpan k s).add_mem hv hv2, rfl⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 : P
hp1 : p1 ∈ spanPoints k s
hp2 : p2 ∈ spanPoints k s
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
[PROOFSTEP]
rcases hp1 with ⟨p1a, ⟨hp1a, ⟨v1, ⟨hv1, hv1p⟩⟩⟩⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 : P
hp2 : p2 ∈ spanPoints k s
p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
[PROOFSTEP]
rcases hp2 with ⟨p2a, ⟨hp2a, ⟨v2, ⟨hv2, hv2p⟩⟩⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
[PROOFSTEP]
rw [hv1p, hv2p, vsub_vadd_eq_vsub_sub (v1 +ᵥ p1a), vadd_vsub_assoc, add_comm, add_sub_assoc]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
[PROOFSTEP]
have hv1v2 : v1 - v2 ∈ vectorSpan k s := by
  rw [sub_eq_add_neg]
  apply (vectorSpan k s).add_mem hv1
  rw [← neg_one_smul k v2]
  exact (vectorSpan k s).smul_mem (-1 : k) hv2
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ v1 - v2 ∈ vectorSpan k s
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ v1 + -v2 ∈ vectorSpan k s
[PROOFSTEP]
apply (vectorSpan k s).add_mem hv1
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -v2 ∈ vectorSpan k s
[PROOFSTEP]
rw [← neg_one_smul k v2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -1 • v2 ∈ vectorSpan k s
[PROOFSTEP]
exact (vectorSpan k s).smul_mem (-1 : k) hv2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
[PROOFSTEP]
refine' (vectorSpan k s).add_mem _ hv1v2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a ∈ vectorSpan k s
[PROOFSTEP]
exact vsub_mem_vectorSpan k hp1a hp2a
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p q : AffineSubspace k P
x✝ : p.carrier = q.carrier
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
q : AffineSubspace k P
carrier✝ : Set P
smul_vsub_vadd_mem✝ :
  ∀ (c : k) {p1 p2 p3 : P}, p1 ∈ carrier✝ → p2 ∈ carrier✝ → p3 ∈ carrier✝ → c • (p1 -ᵥ p2) +ᵥ p3 ∈ carrier✝
x✝ : { carrier := carrier✝, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
carrier✝¹ : Set P
smul_vsub_vadd_mem✝¹ :
  ∀ (c : k) {p1 p2 p3 : P}, p1 ∈ carrier✝¹ → p2 ∈ carrier✝¹ → p3 ∈ carrier✝¹ → c • (p1 -ᵥ p2) +ᵥ p3 ∈ carrier✝¹
carrier✝ : Set P
smul_vsub_vadd_mem✝ :
  ∀ (c : k) {p1 p2 p3 : P}, p1 ∈ carrier✝ → p2 ∈ carrier✝ → p3 ∈ carrier✝ → c • (p1 -ᵥ p2) +ᵥ p3 ∈ carrier✝
x✝ :
  { carrier := carrier✝¹, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝¹ }.carrier =
    { carrier := carrier✝, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝ }.carrier
⊢ { carrier := carrier✝¹, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝¹ } =
    { carrier := carrier✝, smul_vsub_vadd_mem := smul_vsub_vadd_mem✝ }
[PROOFSTEP]
congr
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
intro a b ha hb
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
a b : V
ha : a ∈ ↑s -ᵥ ↑s
hb : b ∈ ↑s -ᵥ ↑s
⊢ a + b ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
rcases ha with ⟨p1, p2, hp1, hp2, rfl⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
b : V
hb : b ∈ ↑s -ᵥ ↑s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 + b ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
rcases hb with ⟨p3, p4, hp3, hp4, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
p3 p4 : P
hp3 : p3 ∈ ↑s
hp4 : p4 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 + (fun x x_1 => x -ᵥ x_1) p3 p4 ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
rw [← vadd_vsub_assoc]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
p3 p4 : P
hp3 : p3 ∈ ↑s
hp4 : p4 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 +ᵥ p3 -ᵥ p4 ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
refine' vsub_mem_vsub _ hp4
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
p3 p4 : P
hp3 : p3 ∈ ↑s
hp4 : p4 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 +ᵥ p3 ∈ ↑s
[PROOFSTEP]
convert s.smul_vsub_vadd_mem 1 hp1 hp2 hp3
[GOAL]
case h.e'_4.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
p3 p4 : P
hp3 : p3 ∈ ↑s
hp4 : p4 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 = 1 • (p1 -ᵥ p2)
[PROOFSTEP]
rw [one_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ 0 ∈ { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier
[PROOFSTEP]
cases' h with p hp
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ ↑s
⊢ 0 ∈ { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier
[PROOFSTEP]
exact vsub_self p ▸ vsub_mem_vsub hp hp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ ∀ (c : k) {x : V},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := ↑s -ᵥ ↑s,
                        add_mem' :=
                          (_ :
                            ∀ {a b : V},
                              a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := ↑s -ᵥ ↑s,
                        add_mem' :=
                          (_ :
                            ∀ {a b : V},
                              a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
intro c v hv
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
c : k
v : V
hv :
  v ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := ↑s -ᵥ ↑s,
                    add_mem' :=
                      (_ :
                        ∀ {a b : V},
                          a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • v ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := ↑s -ᵥ ↑s,
                    add_mem' :=
                      (_ :
                        ∀ {a b : V},
                          a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases hv with ⟨p1, p2, hp1, hp2, rfl⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
c : k
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
⊢ c • (fun x x_1 => x -ᵥ x_1) p1 p2 ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := ↑s -ᵥ ↑s,
                    add_mem' :=
                      (_ :
                        ∀ {a b : V},
                          a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [← vadd_vsub (c • (p1 -ᵥ p2)) p2]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
c : k
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
⊢ c • (p1 -ᵥ p2) +ᵥ p2 -ᵥ p2 ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := ↑s -ᵥ ↑s,
                    add_mem' :=
                      (_ :
                        ∀ {a b : V},
                          a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
refine' vsub_mem_vsub _ hp2
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
c : k
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
⊢ c • (p1 -ᵥ p2) +ᵥ p2 ∈ ↑s
[PROOFSTEP]
exact s.smul_vsub_vadd_mem c hp1 hp2 hp2
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ directionOfNonempty h = direction s
[PROOFSTEP]
refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ directionOfNonempty h ≤ direction s
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk, AddSubmonoid.coe_set_mk]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := (_ : ∀ {a b : V}, a ∈ ↑s -ᵥ ↑s → b ∈ ↑s -ᵥ ↑s → a + b ∈ ↑s -ᵥ ↑s) } ⊆
    ↑(vectorSpan k ↑s)
[PROOFSTEP]
exact (vsub_set_subset_vectorSpan k _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
v : V
⊢ v ∈ direction s ↔ ∃ p1, p1 ∈ s ∧ ∃ p2, p2 ∈ s ∧ v = p1 -ᵥ p2
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
v : V
⊢ v ∈ ↑s -ᵥ ↑s ↔ ∃ p1, p1 ∈ s ∧ ∃ p2, p2 ∈ s ∧ v = p1 -ᵥ p2
[PROOFSTEP]
exact
  ⟨fun ⟨p1, p2, hp1, hp2, hv⟩ => ⟨p1, hp1, p2, hp2, hv.symm⟩, fun ⟨p1, hp1, p2, hp2, hv⟩ => ⟨p1, p2, hp1, hp2, hv.symm⟩⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ direction s
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s
[PROOFSTEP]
rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : ∃ p1, p1 ∈ s ∧ ∃ p2, p2 ∈ s ∧ v = p1 -ᵥ p2
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s
[PROOFSTEP]
rcases hv with ⟨p1, hp1, p2, hp2, hv⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p1 : P
hp1 : p1 ∈ s
p2 : P
hp2 : p2 ∈ s
hv : v = p1 -ᵥ p2
⊢ v +ᵥ p ∈ s
[PROOFSTEP]
rw [hv]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p1 : P
hp1 : p1 ∈ s
p2 : P
hp2 : p2 ∈ s
hv : v = p1 -ᵥ p2
⊢ p1 -ᵥ p2 +ᵥ p ∈ s
[PROOFSTEP]
convert s.smul_vsub_vadd_mem 1 hp1 hp2 hp
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p1 : P
hp1 : p1 ∈ s
p2 : P
hp2 : p2 ∈ s
hv : v = p1 -ᵥ p2
⊢ p1 -ᵥ p2 +ᵥ p ∈ s ↔ 1 • (p1 -ᵥ p2) +ᵥ p ∈ s.carrier
[PROOFSTEP]
rw [one_smul]
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p1 : P
hp1 : p1 ∈ s
p2 : P
hp2 : p2 ∈ s
hv : v = p1 -ᵥ p2
⊢ p1 -ᵥ p2 +ᵥ p ∈ s ↔ p1 -ᵥ p2 +ᵥ p ∈ s.carrier
[PROOFSTEP]
exact s.mem_coe k P _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
h : v +ᵥ p ∈ s
⊢ v ∈ direction s
[PROOFSTEP]
simpa using vsub_mem_direction h hp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ direction s
p : P
⊢ v +ᵥ p ∈ s ↔ p ∈ s
[PROOFSTEP]
refine' ⟨fun h => _, fun h => vadd_mem_of_mem_direction hv h⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ direction s
p : P
h : v +ᵥ p ∈ s
⊢ p ∈ s
[PROOFSTEP]
convert vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h
[GOAL]
case h.e'_4
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ direction s
p : P
h : v +ᵥ p ∈ s
⊢ p = -v +ᵥ (v +ᵥ p)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑(direction s) = (fun x => x -ᵥ p) '' ↑s
[PROOFSTEP]
rw [coe_direction_eq_vsub_set ⟨p, hp⟩]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s = (fun x => x -ᵥ p) '' ↑s
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s ≤ (fun x => x -ᵥ p) '' ↑s
[PROOFSTEP]
rintro v ⟨p1, p2, hp1, hp2, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p1 p2 : P
hp1 : p1 ∈ ↑s
hp2 : p2 ∈ ↑s
⊢ (fun x x_1 => x -ᵥ x_1) p1 p2 ∈ (fun x => x -ᵥ p) '' ↑s
[PROOFSTEP]
exact ⟨p1 -ᵥ p2 +ᵥ p, vadd_mem_of_mem_direction (vsub_mem_direction hp1 hp2) hp, vadd_vsub _ _⟩
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ (fun x => x -ᵥ p) '' ↑s ≤ ↑s -ᵥ ↑s
[PROOFSTEP]
rintro v ⟨p2, hp2, rfl⟩
[GOAL]
case refine'_2.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
hp2 : p2 ∈ ↑s
⊢ (fun x => x -ᵥ p) p2 ∈ ↑s -ᵥ ↑s
[PROOFSTEP]
exact ⟨p2, p, hp2, hp, rfl⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑(direction s) = (fun x x_1 => x -ᵥ x_1) p '' ↑s
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑(direction s) ↔ v ∈ (fun x x_1 => x -ᵥ x_1) p '' ↑s
[PROOFSTEP]
rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp,
  Set.mem_image_iff_bex, Set.mem_image_iff_bex]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ (∃ x x_1, x -ᵥ p = -v) ↔ ∃ x x_1, (fun x x_2 => x -ᵥ x_2) p x = v
[PROOFSTEP]
conv_lhs =>
  congr
  ext
  rw [← neg_vsub_eq_vsub_rev, neg_inj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
| ∃ x x_1, x -ᵥ p = -v
[PROOFSTEP]
  congr
  ext
  rw [← neg_vsub_eq_vsub_rev, neg_inj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
| ∃ x x_1, x -ᵥ p = -v
[PROOFSTEP]
  congr
  ext
  rw [← neg_vsub_eq_vsub_rev, neg_inj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
| ∃ x x_1, x -ᵥ p = -v
[PROOFSTEP]
congr
[GOAL]
case p
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
| fun x => ∃ x_1, x -ᵥ p = -v
[PROOFSTEP]
ext
[GOAL]
case p.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
x✝ : P
| ∃ x, x✝ -ᵥ p = -v
[PROOFSTEP]
rw [← neg_vsub_eq_vsub_rev, neg_inj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ direction s ↔ ∃ p2, p2 ∈ s ∧ v = p2 -ᵥ p
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x => x -ᵥ p) '' ↑s ↔ ∃ p2, p2 ∈ s ∧ v = p2 -ᵥ p
[PROOFSTEP]
exact ⟨fun ⟨p2, hp2, hv⟩ => ⟨p2, hp2, hv.symm⟩, fun ⟨p2, hp2, hv⟩ => ⟨p2, hp2, hv.symm⟩⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ direction s ↔ ∃ p2, p2 ∈ s ∧ v = p -ᵥ p2
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x x_1 => x -ᵥ x_1) p '' ↑s ↔ ∃ p2, p2 ∈ s ∧ v = p -ᵥ p2
[PROOFSTEP]
exact ⟨fun ⟨p2, hp2, hv⟩ => ⟨p2, hp2, hv.symm⟩, fun ⟨p2, hp2, hv⟩ => ⟨p2, hp2, hv.symm⟩⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
⊢ p2 -ᵥ p ∈ direction s ↔ p2 ∈ s
[PROOFSTEP]
rw [mem_direction_iff_eq_vsub_right hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
⊢ (∃ p2_1, p2_1 ∈ s ∧ p2 -ᵥ p = p2_1 -ᵥ p) ↔ p2 ∈ s
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
⊢ p -ᵥ p2 ∈ direction s ↔ p2 ∈ s
[PROOFSTEP]
rw [mem_direction_iff_eq_vsub_left hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
⊢ (∃ p2_1, p2_1 ∈ s ∧ p -ᵥ p2 = p -ᵥ p2_1) ↔ p2 ∈ s
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
⊢ s1 = s2
[PROOFSTEP]
ext p
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
⊢ p ∈ s1 ↔ p ∈ s2
[PROOFSTEP]
have hq1 := Set.mem_of_mem_inter_left hn.some_mem
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
⊢ p ∈ s1 ↔ p ∈ s2
[PROOFSTEP]
have hq2 := Set.mem_of_mem_inter_right hn.some_mem
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 ↔ p ∈ s2
[PROOFSTEP]
constructor
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 → p ∈ s2
[PROOFSTEP]
intro hp
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p ∈ s2
[PROOFSTEP]
rw [← vsub_vadd p hn.some]
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s2
[PROOFSTEP]
refine' vadd_mem_of_mem_direction _ hq2
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
[PROOFSTEP]
rw [← hd]
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
[PROOFSTEP]
exact vsub_mem_direction hp hq1
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s2 → p ∈ s1
[PROOFSTEP]
intro hp
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p ∈ s1
[PROOFSTEP]
rw [← vsub_vadd p hn.some]
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s1
[PROOFSTEP]
refine' vadd_mem_of_mem_direction _ hq1
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
[PROOFSTEP]
rw [hd]
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
[PROOFSTEP]
exact vsub_mem_direction hp hq2
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a : { x // x ∈ s }
⊢ 0 +ᵥ a = a
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a : { x // x ∈ s }
⊢ ↑(0 +ᵥ a) = ↑a
[PROOFSTEP]
exact zero_vadd _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a b : { x // x ∈ direction s }
c : { x // x ∈ s }
⊢ a + b +ᵥ c = a +ᵥ (b +ᵥ c)
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a b : { x // x ∈ direction s }
c : { x // x ∈ s }
⊢ ↑(a + b +ᵥ c) = ↑(a +ᵥ (b +ᵥ c))
[PROOFSTEP]
apply add_vadd
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
⊢ Nonempty { x // x ∈ s }
[PROOFSTEP]
infer_instance
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a b : { x // x ∈ s }
⊢ a -ᵥ b +ᵥ b = a
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a b : { x // x ∈ s }
⊢ ↑(a -ᵥ b +ᵥ b) = ↑a
[PROOFSTEP]
apply AddTorsor.vsub_vadd'
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a : { x // x ∈ direction s }
b : { x // x ∈ s }
⊢ a +ᵥ b -ᵥ b = a
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty { x // x ∈ s }
a : { x // x ∈ direction s }
b : { x // x ∈ s }
⊢ ↑(a +ᵥ b -ᵥ b) = ↑a
[PROOFSTEP]
apply AddTorsor.vadd_vsub'
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
c : k
p1 p2 p3 : P
hp1 : p1 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
hp2 : p2 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
hp3 : p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
[PROOFSTEP]
rcases hp1 with ⟨v1, hv1, hp1⟩
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
c : k
p1 p2 p3 : P
hp2 : p2 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
hp3 : p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
[PROOFSTEP]
rcases hp2 with ⟨v2, hv2, hp2⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
c : k
p1 p2 p3 : P
hp3 : p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
v2 : V
hv2 : v2 ∈ direction
hp2 : p2 = v2 +ᵥ p
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
[PROOFSTEP]
rcases hp3 with ⟨v3, hv3, hp3⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
c : k
p1 p2 p3 : P
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
v2 : V
hv2 : v2 ∈ direction
hp2 : p2 = v2 +ᵥ p
v3 : V
hv3 : v3 ∈ direction
hp3 : p3 = v3 +ᵥ p
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ {q | ∃ v, v ∈ direction ∧ q = v +ᵥ p}
[PROOFSTEP]
use c • (v1 - v2) + v3, direction.add_mem (direction.smul_mem c (direction.sub_mem hv1 hv2)) hv3
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
c : k
p1 p2 p3 : P
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
v2 : V
hv2 : v2 ∈ direction
hp2 : p2 = v2 +ᵥ p
v3 : V
hv3 : v3 ∈ direction
hp3 : p3 = v3 +ᵥ p
⊢ c • (p1 -ᵥ p2) +ᵥ p3 = c • (v1 - v2) + v3 +ᵥ p
[PROOFSTEP]
simp [hp1, hp2, hp3, vadd_vadd]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
⊢ AffineSubspace.direction (mk' p direction) = direction
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
⊢ v ∈ AffineSubspace.direction (mk' p direction) ↔ v ∈ direction
[PROOFSTEP]
rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
⊢ (∃ p1, p1 ∈ mk' p direction ∧ ∃ p2, p2 ∈ mk' p direction ∧ v = p1 -ᵥ p2) ↔ v ∈ direction
[PROOFSTEP]
constructor
[GOAL]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
⊢ (∃ p1, p1 ∈ mk' p direction ∧ ∃ p2, p2 ∈ mk' p direction ∧ v = p1 -ᵥ p2) → v ∈ direction
[PROOFSTEP]
rintro ⟨p1, ⟨v1, hv1, hp1⟩, p2, ⟨v2, hv2, hp2⟩, hv⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
p1 : P
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
p2 : P
hv : v = p1 -ᵥ p2
v2 : V
hv2 : v2 ∈ direction
hp2 : p2 = v2 +ᵥ p
⊢ v ∈ direction
[PROOFSTEP]
rw [hv, hp1, hp2, vadd_vsub_vadd_cancel_right]
[GOAL]
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
p1 : P
v1 : V
hv1 : v1 ∈ direction
hp1 : p1 = v1 +ᵥ p
p2 : P
hv : v = p1 -ᵥ p2
v2 : V
hv2 : v2 ∈ direction
hp2 : p2 = v2 +ᵥ p
⊢ v1 - v2 ∈ direction
[PROOFSTEP]
exact direction.sub_mem hv1 hv2
[GOAL]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
⊢ v ∈ direction → ∃ p1, p1 ∈ mk' p direction ∧ ∃ p2, p2 ∈ mk' p direction ∧ v = p1 -ᵥ p2
[PROOFSTEP]
exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
⊢ p₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ direction
[PROOFSTEP]
rw [← direction_mk' p₁ direction]
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ AffineSubspace.direction (mk' p₁ direction)
[PROOFSTEP]
exact vsub_mem_direction h (self_mem_mk' _ _)
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ ∈ mk' p₁ direction
[PROOFSTEP]
rw [← vsub_vadd p₂ p₁]
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ -ᵥ p₁ +ᵥ p₁ ∈ mk' p₁ direction
[PROOFSTEP]
exact vadd_mem_mk' p₁ h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
⊢ spanPoints k s ⊆ ↑s1
[PROOFSTEP]
rintro p ⟨p1, hp1, v, hv, hp⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
⊢ p ∈ ↑s1
[PROOFSTEP]
rw [hp]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
⊢ v +ᵥ p1 ∈ ↑s1
[PROOFSTEP]
have hp1s1 : p1 ∈ (s1 : Set P) := Set.mem_of_mem_of_subset hp1 h
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
hp1s1 : p1 ∈ ↑s1
⊢ v +ᵥ p1 ∈ ↑s1
[PROOFSTEP]
refine' vadd_mem_of_mem_direction _ hp1s1
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
hp1s1 : p1 ∈ ↑s1
⊢ v ∈ direction s1
[PROOFSTEP]
have hs : vectorSpan k s ≤ s1.direction := vectorSpan_mono k h
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
hp1s1 : p1 ∈ ↑s1
hs : vectorSpan k s ≤ direction s1
⊢ v ∈ direction s1
[PROOFSTEP]
rw [SetLike.le_def] at hs 
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
hp1s1 : p1 ∈ ↑s1
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ direction s1
⊢ v ∈ direction s1
[PROOFSTEP]
rw [← SetLike.mem_coe]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s1 : AffineSubspace k P
h : s ⊆ ↑s1
p p1 : P
hp1 : p1 ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p1
hp1s1 : p1 ∈ ↑s1
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ direction s1
⊢ v ∈ ↑(direction s1)
[PROOFSTEP]
exact Set.mem_of_mem_of_subset hv hs
[GOAL]
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
⊢ AffineSubspace.direction (toAffineSubspace s) = s
[PROOFSTEP]
ext x
[GOAL]
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ AffineSubspace.direction (toAffineSubspace s) ↔ x ∈ s
[PROOFSTEP]
simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ ↑(lineMap p₀ p₁) c ∈ Q
[PROOFSTEP]
rw [AffineMap.lineMap_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
[PROOFSTEP]
exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ AffineSubspace.direction (affineSpan k s) = vectorSpan k s
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ AffineSubspace.direction (affineSpan k s) ≤ vectorSpan k s
[PROOFSTEP]
refine' Submodule.span_le.2 _
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ↑(affineSpan k s) -ᵥ ↑(affineSpan k s) ⊆ ↑(vectorSpan k s)
[PROOFSTEP]
rintro v ⟨p1, p3, ⟨p2, hp2, v1, hv1, hp1⟩, ⟨p4, hp4, v2, hv2, hp3⟩, rfl⟩
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p3 p2 : P
hp2 : p2 ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hp1 : p1 = v1 +ᵥ p2
p4 : P
hp4 : p4 ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hp3 : p3 = v2 +ᵥ p4
⊢ (fun x x_1 => x -ᵥ x_1) p1 p3 ∈ ↑(vectorSpan k s)
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p3 p2 : P
hp2 : p2 ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hp1 : p1 = v1 +ᵥ p2
p4 : P
hp4 : p4 ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hp3 : p3 = v2 +ᵥ p4
⊢ p1 -ᵥ p3 ∈ vectorSpan k s
[PROOFSTEP]
rw [hp1, hp3, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p3 p2 : P
hp2 : p2 ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hp1 : p1 = v1 +ᵥ p2
p4 : P
hp4 : p4 ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hp3 : p3 = v2 +ᵥ p4
⊢ v1 + (p2 -ᵥ p4) - v2 ∈ vectorSpan k s
[PROOFSTEP]
exact (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv1 (vsub_mem_vectorSpan k hp2 hp4)) hv2
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ vectorSpan k s ≤ AffineSubspace.direction (affineSpan k s)
[PROOFSTEP]
exact vectorSpan_mono k (subset_spanPoints k s)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
src✝ : PartialOrder (AffineSubspace k P) := PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)
s : Set (AffineSubspace k P)
c : k
p1 p2 p3 : P
hp1 : p1 ∈ ⋂ (s' : AffineSubspace k P) (_ : s' ∈ s), ↑s'
hp2 : p2 ∈ ⋂ (s' : AffineSubspace k P) (_ : s' ∈ s), ↑s'
hp3 : p3 ∈ ⋂ (s' : AffineSubspace k P) (_ : s' ∈ s), ↑s'
s2 : AffineSubspace k P
hs2 : s2 ∈ s
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ ↑s2
[PROOFSTEP]
rw [Set.mem_iInter₂] at *
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
src✝ : PartialOrder (AffineSubspace k P) := PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)
s : Set (AffineSubspace k P)
c : k
p1 p2 p3 : P
hp1 : ∀ (i : AffineSubspace k P), i ∈ s → p1 ∈ ↑i
hp2 : ∀ (i : AffineSubspace k P), i ∈ s → p2 ∈ ↑i
hp3 : ∀ (i : AffineSubspace k P), i ∈ s → p3 ∈ ↑i
s2 : AffineSubspace k P
hs2 : s2 ∈ s
⊢ c • (p1 -ᵥ p2) +ᵥ p3 ∈ ↑s2
[PROOFSTEP]
exact s2.smul_vsub_vadd_mem c (hp1 s2 hs2) (hp2 s2 hs2) (hp3 s2 hs2)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S✝ : AffineSpace V P
src✝ : PartialOrder (AffineSubspace k P) := PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)
S : Set (AffineSubspace k P)
s1 : AffineSubspace k P
hs1 : ∀ (b : AffineSubspace k P), b ∈ S → s1 ≤ b
⊢ s1 ≤ sInf S
[PROOFSTEP]
refine' Set.subset_sInter (t := (s1 : Set P)) _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S✝ : AffineSpace V P
src✝ : PartialOrder (AffineSubspace k P) := PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)
S : Set (AffineSubspace k P)
s1 : AffineSubspace k P
hs1 : ∀ (b : AffineSubspace k P), b ∈ S → s1 ≤ b
⊢ ∀ (t' : Set P), (t' ∈ range fun s' => ⋂ (_ : s' ∈ S), ↑s') → ↑s1 ⊆ t'
[PROOFSTEP]
rintro t ⟨s, _hs, rfl⟩
[GOAL]
case intro.refl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S✝ : AffineSpace V P
src✝ : PartialOrder (AffineSubspace k P) := PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)
S : Set (AffineSubspace k P)
s1 : AffineSubspace k P
hs1 : ∀ (b : AffineSubspace k P), b ∈ S → s1 ≤ b
s : AffineSubspace k P
⊢ ↑s1 ⊆ (fun s' => ⋂ (_ : s' ∈ S), ↑s') s
[PROOFSTEP]
exact Set.subset_iInter (hs1 s)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s1 s2 : AffineSubspace k P
⊢ s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p, p ∈ s2 ∧ ¬p ∈ s1
[PROOFSTEP]
rw [lt_iff_le_not_le, not_le_iff_exists]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
⊢ ↑(affineSpan k {p}) = {p}
[PROOFSTEP]
ext x
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}
[PROOFSTEP]
rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _, direction_affineSpan]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂
[PROOFSTEP]
simp [← mem_coe]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ direction ⊤ = ⊤
[PROOFSTEP]
cases' S.Nonempty with p
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
⊢ direction ⊤ = ⊤
[PROOFSTEP]
ext v
[GOAL]
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
⊢ v ∈ direction ⊤ ↔ v ∈ ⊤
[PROOFSTEP]
refine' ⟨imp_intro Submodule.mem_top, fun _hv => _⟩
[GOAL]
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ direction ⊤
[PROOFSTEP]
have hpv : (v +ᵥ p -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction := vsub_mem_direction (mem_top k V _) (mem_top k V _)
[GOAL]
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
hpv : v +ᵥ p -ᵥ p ∈ direction ⊤
⊢ v ∈ direction ⊤
[PROOFSTEP]
rwa [vadd_vsub] at hpv 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
intro contra
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
contra : ⊥ = ⊤
⊢ False
[PROOFSTEP]
rw [← ext_iff, bot_coe, top_coe] at contra 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
contra : ∅ = univ
⊢ False
[PROOFSTEP]
exact Set.empty_ne_univ contra
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h : affineSpan k s = ⊤
⊢ Set.Nonempty s
[PROOFSTEP]
rw [Set.nonempty_iff_ne_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅
[PROOFSTEP]
rintro rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
h : affineSpan k ∅ = ⊤
⊢ False
[PROOFSTEP]
rw [AffineSubspace.span_empty] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
h : ⊥ = ⊤
⊢ False
[PROOFSTEP]
exact bot_ne_top k V P h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h : affineSpan k s = ⊤
⊢ vectorSpan k s = ⊤
[PROOFSTEP]
rw [← direction_affineSpan, h, direction_top]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
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 = ⊤
[PROOFSTEP]
refine' ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, _⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
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 = ⊤
[PROOFSTEP]
intro h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
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 = ⊤
[PROOFSTEP]
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]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
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 = ⊤
[PROOFSTEP]
obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
[GOAL]
case intro.mk
k : Type u_1
V : Type u_2
P : Type u_3
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 = ⊤
[PROOFSTEP]
rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
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 }
[PROOFSTEP]
obtain ⟨x, hx⟩ := hs
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
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 }
[PROOFSTEP]
exact ⟨⟨x, mem_affineSpan k hx⟩⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
inst✝ : Nontrivial P
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with hs hs
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
inst✝ : Nontrivial P
hs : s = ∅
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
[PROOFSTEP]
simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]
[GOAL]
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
inst✝ : Nontrivial P
hs : Set.Nonempty s
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
[PROOFSTEP]
rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
p₁ p₂ : P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
⊢ 0 < Fintype.card ι
[PROOFSTEP]
obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
p₁ p₂ : P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
i : ι
⊢ 0 < Fintype.card ι
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr ⟨i⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ direction ⊥ = ⊥
[PROOFSTEP]
rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
Q : AffineSubspace k P
⊢ Set.Nonempty ↑Q ↔ Q ≠ ⊥
[PROOFSTEP]
rw [nonempty_iff_ne_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥
[PROOFSTEP]
exact not_congr Q.coe_eq_bot_iff
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Set.Nonempty ↑Q
[PROOFSTEP]
rw [nonempty_iff_ne_bot]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥
[PROOFSTEP]
apply eq_or_ne
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
⊢ Subsingleton P
[PROOFSTEP]
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P
[PROOFSTEP]
have : s = { p } := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s
[PROOFSTEP]
simp [hp]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
[PROOFSTEP]
rw [this, ← AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton, AffineSubspace.top_coe, eq_comm, ←
  subsingleton_iff_singleton (mem_univ _)] at h₂ 
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
p : P
h₂ : Set.Subsingleton univ
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
[PROOFSTEP]
exact subsingleton_of_univ_subsingleton h₂
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
⊢ s = univ
[PROOFSTEP]
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ
[PROOFSTEP]
have : s = { p } := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s
[PROOFSTEP]
simp [hp]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ
[PROOFSTEP]
rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
[PROOFSTEP]
exact subsingleton_of_subsingleton_span_eq_top h₁ h₂
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ direction s = ⊤ ↔ s = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ direction s = ⊤ → s = ⊤
[PROOFSTEP]
intro hd
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = ⊤
⊢ s = ⊤
[PROOFSTEP]
rw [← direction_top k V P] at hd 
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ s = ⊤
[PROOFSTEP]
refine' ext_of_direction_eq hd _
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ Set.Nonempty (↑s ∩ ↑⊤)
[PROOFSTEP]
simp [h]
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ s = ⊤ → direction s = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
h : Set.Nonempty ↑⊤
⊢ direction ⊤ = ⊤
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
⊢ direction (s1 ⊓ s2) ≤ direction s1 ⊓ direction s2
[PROOFSTEP]
simp only [direction_eq_vectorSpan, vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
⊢ Submodule.span k (↑(s1 ⊓ s2) -ᵥ ↑(s1 ⊓ s2)) ≤ Submodule.span k (↑s1 -ᵥ ↑s1) ⊓ Submodule.span k (↑s2 -ᵥ ↑s2)
[PROOFSTEP]
exact
  le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono (inter_subset_left _ _)) hp)
    (sInf_le_sInf fun p hp => trans (vsub_self_mono (inter_subset_right _ _)) hp)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
⊢ direction (s₁ ⊓ s₂) = direction s₁ ⊓ direction s₂
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ direction (s₁ ⊓ s₂) ↔ v ∈ direction s₁ ⊓ direction s₂
[PROOFSTEP]
rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
  vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h : s1 ≤ s2
⊢ direction s1 ≤ direction s2
[PROOFSTEP]
simp only [direction_eq_vectorSpan, vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h : s1 ≤ s2
⊢ Submodule.span k (↑s1 -ᵥ ↑s1) ≤ Submodule.span k (↑s2 -ᵥ ↑s2)
[PROOFSTEP]
exact vectorSpan_mono k h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h : s1 < s2
hn : Set.Nonempty ↑s1
⊢ direction s1 < direction s2
[PROOFSTEP]
cases' hn with p hp
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h : s1 < s2
p : P
hp : p ∈ ↑s1
⊢ direction s1 < direction s2
[PROOFSTEP]
rw [lt_iff_le_and_exists] at h 
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h : s1 ≤ s2 ∧ ∃ p, p ∈ s2 ∧ ¬p ∈ s1
p : P
hp : p ∈ ↑s1
⊢ direction s1 < direction s2
[PROOFSTEP]
rcases h with ⟨hle, p2, hp2, hp2s1⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
p : P
hp : p ∈ ↑s1
hle : s1 ≤ s2
p2 : P
hp2 : p2 ∈ s2
hp2s1 : ¬p2 ∈ s1
⊢ direction s1 < direction s2
[PROOFSTEP]
rw [SetLike.lt_iff_le_and_exists]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
p : P
hp : p ∈ ↑s1
hle : s1 ≤ s2
p2 : P
hp2 : p2 ∈ s2
hp2s1 : ¬p2 ∈ s1
⊢ direction s1 ≤ direction s2 ∧ ∃ x, x ∈ direction s2 ∧ ¬x ∈ direction s1
[PROOFSTEP]
use direction_le hle, p2 -ᵥ p, vsub_mem_direction hp2 (hle hp)
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
p : P
hp : p ∈ ↑s1
hle : s1 ≤ s2
p2 : P
hp2 : p2 ∈ s2
hp2s1 : ¬p2 ∈ s1
⊢ ¬p2 -ᵥ p ∈ direction s1
[PROOFSTEP]
intro hm
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
p : P
hp : p ∈ ↑s1
hle : s1 ≤ s2
p2 : P
hp2 : p2 ∈ s2
hp2s1 : ¬p2 ∈ s1
hm : p2 -ᵥ p ∈ direction s1
⊢ False
[PROOFSTEP]
rw [vsub_right_mem_direction_iff_mem hp p2] at hm 
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
p : P
hp : p ∈ ↑s1
hle : s1 ≤ s2
p2 : P
hp2 : p2 ∈ s2
hp2s1 : ¬p2 ∈ s1
hm : p2 ∈ s1
⊢ False
[PROOFSTEP]
exact hp2s1 hm
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
⊢ direction s1 ⊔ direction s2 ≤ direction (s1 ⊔ s2)
[PROOFSTEP]
simp only [direction_eq_vectorSpan, vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
⊢ Submodule.span k (↑s1 -ᵥ ↑s1) ⊔ Submodule.span k (↑s2 -ᵥ ↑s2) ≤ Submodule.span k (↑(s1 ⊔ s2) -ᵥ ↑(s1 ⊔ s2))
[PROOFSTEP]
exact
  sup_le (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_left : s1 ≤ s1 ⊔ s2)) hp)
    (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_right : s2 ≤ s1 ⊔ s2)) hp)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
he : ↑s1 ∩ ↑s2 = ∅
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
[PROOFSTEP]
cases' h1 with p1 hp1
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h2 : Set.Nonempty ↑s2
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
[PROOFSTEP]
cases' h2 with p2 hp2
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
[PROOFSTEP]
rw [SetLike.lt_iff_le_and_exists]
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 ≤ direction (s1 ⊔ s2) ∧ ∃ x, x ∈ direction (s1 ⊔ s2) ∧ ¬x ∈ direction s1 ⊔ direction s2
[PROOFSTEP]
use sup_direction_le s1 s2, p2 -ᵥ p1,
  vsub_mem_direction ((le_sup_right : s2 ≤ s1 ⊔ s2) hp2) ((le_sup_left : s1 ≤ s1 ⊔ s2) hp1)
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ ¬p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
[PROOFSTEP]
intro h
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
⊢ False
[PROOFSTEP]
rw [Submodule.mem_sup] at h 
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : ∃ y, y ∈ direction s1 ∧ ∃ z, z ∈ direction s2 ∧ y + z = p2 -ᵥ p1
⊢ False
[PROOFSTEP]
rcases h with ⟨v1, hv1, v2, hv2, hv1v2⟩
[GOAL]
case right.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2 : v1 + v2 = p2 -ᵥ p1
⊢ False
[PROOFSTEP]
rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v1, add_assoc, ← vadd_vsub_assoc, ← neg_neg v2,
  add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hv1v2 
[GOAL]
case right.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ False
[PROOFSTEP]
refine' Set.Nonempty.ne_empty _ he
[GOAL]
case right.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ Set.Nonempty (↑s1 ∩ ↑s2)
[PROOFSTEP]
use v1 +ᵥ p1, vadd_mem_of_mem_direction hv1 hp1
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ v1 +ᵥ p1 ∈ ↑s2
[PROOFSTEP]
rw [hv1v2]
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ -v2 +ᵥ p2 ∈ ↑s2
[PROOFSTEP]
exact vadd_mem_of_mem_direction (Submodule.neg_mem _ hv2) hp2
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : direction s1 ⊔ direction s2 = ⊤
⊢ Set.Nonempty (↑s1 ∩ ↑s2)
[PROOFSTEP]
by_contra h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : direction s1 ⊔ direction s2 = ⊤
h : ¬Set.Nonempty (↑s1 ∩ ↑s2)
⊢ False
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
⊢ False
[PROOFSTEP]
have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
⊢ False
[PROOFSTEP]
rw [hd] at hlt 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : ⊤ < direction (s1 ⊔ s2)
⊢ False
[PROOFSTEP]
exact not_top_lt hlt
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
⊢ ∃ p, ↑s1 ∩ ↑s2 = {p}
[PROOFSTEP]
cases' inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top with p hp
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ∃ p, ↑s1 ∩ ↑s2 = {p}
[PROOFSTEP]
use p
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ↑s1 ∩ ↑s2 = {p}
[PROOFSTEP]
ext q
[GOAL]
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q ∈ {p}
[PROOFSTEP]
rw [Set.mem_singleton_iff]
[GOAL]
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q = p
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 → q = p
[PROOFSTEP]
rintro ⟨hq1, hq2⟩
[GOAL]
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
⊢ q = p
[PROOFSTEP]
have hqp : q -ᵥ p ∈ s1.direction ⊓ s2.direction := ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
[GOAL]
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
hqp : q -ᵥ p ∈ direction s1 ⊓ direction s2
⊢ q = p
[PROOFSTEP]
rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp 
[GOAL]
case h.h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q = p → q ∈ ↑s1 ∩ ↑s2
[PROOFSTEP]
exact fun h => h.symm ▸ hp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
⊢ affineSpan k ↑s = s
[PROOFSTEP]
refine' le_antisymm _ (subset_spanPoints _ _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
⊢ affineSpan k ↑s ≤ s
[PROOFSTEP]
rintro p ⟨p1, hp1, v, hv, rfl⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
v : V
hv : v ∈ vectorSpan k ↑s
⊢ v +ᵥ p1 ∈ ↑s
[PROOFSTEP]
exact vadd_mem_of_mem_direction hv hp1
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
[PROOFSTEP]
rw [vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
[PROOFSTEP]
refine' le_antisymm _ (Submodule.span_mono _)
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
[PROOFSTEP]
rintro v ⟨p1, p2, hp1, hp2, hv⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p1 p2 = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
[PROOFSTEP]
simp_rw [← vsub_sub_vsub_cancel_left p1 p2 p] at hv 
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
[PROOFSTEP]
rw [← hv, SetLike.mem_coe, Submodule.mem_span]
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ ∀ (p_1 : Submodule k V), (fun x x_1 => x -ᵥ x_1) p '' s ⊆ ↑p_1 → p -ᵥ p2 - (p -ᵥ p1) ∈ p_1
[PROOFSTEP]
exact fun m hm => Submodule.sub_mem _ (hm ⟨p2, hp2, rfl⟩) (hm ⟨p1, hp1, rfl⟩)
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ (fun x x_1 => x -ᵥ x_1) p '' s ⊆ s -ᵥ s
[PROOFSTEP]
rintro v ⟨p2, hp2, hv⟩
[GOAL]
case refine'_2.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p2 : P
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p p2 = v
⊢ v ∈ s -ᵥ s
[PROOFSTEP]
exact ⟨p, p2, hp, hp2, hv⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' s)
[PROOFSTEP]
rw [vectorSpan_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x => x -ᵥ p) '' s)
[PROOFSTEP]
refine' le_antisymm _ (Submodule.span_mono _)
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x => x -ᵥ p) '' s)
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x => x -ᵥ p) '' s))
[PROOFSTEP]
rintro v ⟨p1, p2, hp1, hp2, hv⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p1 p2 = v
⊢ v ∈ ↑(Submodule.span k ((fun x => x -ᵥ p) '' s))
[PROOFSTEP]
simp_rw [← vsub_sub_vsub_cancel_right p1 p2 p] at hv 
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p1 -ᵥ p - (p2 -ᵥ p) = v
⊢ v ∈ ↑(Submodule.span k ((fun x => x -ᵥ p) '' s))
[PROOFSTEP]
rw [← hv, SetLike.mem_coe, Submodule.mem_span]
[GOAL]
case refine'_1.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p1 -ᵥ p - (p2 -ᵥ p) = v
⊢ ∀ (p_1 : Submodule k V), (fun x => x -ᵥ p) '' s ⊆ ↑p_1 → p1 -ᵥ p - (p2 -ᵥ p) ∈ p_1
[PROOFSTEP]
exact fun m hm => Submodule.sub_mem _ (hm ⟨p1, hp1, rfl⟩) (hm ⟨p2, hp2, rfl⟩)
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ (fun x => x -ᵥ p) '' s ⊆ s -ᵥ s
[PROOFSTEP]
rintro v ⟨p2, hp2, hv⟩
[GOAL]
case refine'_2.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
v : V
p2 : P
hp2 : p2 ∈ s
hv : (fun x => x -ᵥ p) p2 = v
⊢ v ∈ s -ᵥ s
[PROOFSTEP]
exact ⟨p2, p, hp2, hp, hv⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' (s \ {p}))
[PROOFSTEP]
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton,
    Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert ((fun x x_1 => x -ᵥ x_1) p p) ((fun x x_1 => x -ᵥ x_1) p '' (s \ {p}))) =
    Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' (s \ {p}))
[PROOFSTEP]
simp [Submodule.span_insert_eq_span]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
[PROOFSTEP]
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton,
    Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x => x -ᵥ p) '' (s \ {p}))) =
    Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
[PROOFSTEP]
simp [Submodule.span_insert_eq_span]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
inst✝¹ : DecidableEq P
inst✝ : DecidableEq V
s : Finset P
p : P
hp : p ∈ s
⊢ vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (Finset.erase s p))
[PROOFSTEP]
simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x x_1 => x -ᵥ x_1) (p i) '' (p '' (s \ {i})))
[PROOFSTEP]
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
  Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert ((fun x x_1 => x -ᵥ x_1) (p i) (p i)) ((fun x x_1 => x -ᵥ x_1) (p i) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x x_1 => x -ᵥ x_1) (p i) '' (p '' (s \ {i})))
[PROOFSTEP]
simp [Submodule.span_insert_eq_span]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
[PROOFSTEP]
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
  Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert (p i -ᵥ p i) ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
[PROOFSTEP]
simp [Submodule.span_insert_eq_span]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i0 -ᵥ p i)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x x_1 => x -ᵥ x_1) (p i0) ∘ p)) = Submodule.span k (range fun i => p i0 -ᵥ p i)
[PROOFSTEP]
congr
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i -ᵥ p i0)
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x => x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i => p i -ᵥ p i0)
[PROOFSTEP]
congr
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
[PROOFSTEP]
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ Submodule.span k ((fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀}))) =
    Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
[PROOFSTEP]
congr with v
[GOAL]
case e_s.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ v ∈ (fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p i₀ -ᵥ p ↑i
[PROOFSTEP]
simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists, Subtype.coe_mk]
[GOAL]
case e_s.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔ ∃ a h, p i₀ -ᵥ p a = v
[PROOFSTEP]
constructor
[GOAL]
case e_s.h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) → ∃ a h, p i₀ -ᵥ p a = v
[PROOFSTEP]
rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
[GOAL]
case e_s.h.mp.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
i₁ : ι
left✝ : i₁ ∈ univ
hi₁ : ¬i₁ = i₀
hv : p i₀ -ᵥ p i₁ = v
⊢ ∃ a h, p i₀ -ᵥ p a = v
[PROOFSTEP]
exact ⟨i₁, hi₁, hv⟩
[GOAL]
case e_s.h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a h, p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v
[PROOFSTEP]
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p ↑i -ᵥ p i₀)
[PROOFSTEP]
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_right_ne k _ (Set.mem_univ i₀)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ Submodule.span k ((fun x => x -ᵥ p i₀) '' (p '' (univ \ {i₀}))) = Submodule.span k (range fun i => p ↑i -ᵥ p i₀)
[PROOFSTEP]
congr with v
[GOAL]
case e_s.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ v ∈ (fun x => x -ᵥ p i₀) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p ↑i -ᵥ p i₀
[PROOFSTEP]
simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists, Subtype.coe_mk]
[GOAL]
case e_s.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) ↔ ∃ a h, p a -ᵥ p i₀ = v
[PROOFSTEP]
constructor
[GOAL]
case e_s.h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) → ∃ a h, p a -ᵥ p i₀ = v
[PROOFSTEP]
rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
[GOAL]
case e_s.h.mp.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
i₁ : ι
left✝ : i₁ ∈ univ
hi₁ : ¬i₁ = i₀
hv : p i₁ -ᵥ p i₀ = v
⊢ ∃ a h, p a -ᵥ p i₀ = v
[PROOFSTEP]
exact ⟨i₁, hi₁, hv⟩
[GOAL]
case e_s.h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a h, p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v
[PROOFSTEP]
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
⊢ affineSpan k s = ⊥ ↔ s = ∅
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← Ne.def, ← nonempty_iff_ne_bot, affineSpan_nonempty, nonempty_iff_ne_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
⊢ ⊥ < affineSpan k s ↔ Set.Nonempty s
[PROOFSTEP]
rw [bot_lt_iff_ne_bot, nonempty_iff_ne_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅
[PROOFSTEP]
exact (affineSpan_eq_bot _).not
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ p x h
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ affineSpan k s) (hc : p x hx) => hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
refine' @affineSpan_induction k V P _ _ _ _ _ _ (fun y => ∃ z, p y z) h _ _
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (x : P), x ∈ s → (fun y => ∃ z, p y z) x
[PROOFSTEP]
exact fun y hy => ⟨subset_affineSpan _ _ hy, Hs y hy⟩
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
Hs : ∀ (y : P) (hys : y ∈ s), p y (_ : y ∈ ↑(affineSpan k s))
Hc :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k s).carrier)
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (fun y => ∃ z, p y z) u →
      (fun y => ∃ z, p y z) v → (fun y => ∃ z, p y z) w → (fun y => ∃ z, p y z) (c • (u -ᵥ v) +ᵥ w)
[PROOFSTEP]
exact fun c u v w hu hv hw =>
  Exists.elim hu fun hu' hu =>
    Exists.elim hv fun hv' hv =>
      Exists.elim hw fun hw' hw => ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw', Hc _ _ _ _ _ _ _ hu hv hw⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
[PROOFSTEP]
rintro ⟨x, hx⟩ -
[GOAL]
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
⊢ { val := x, property := hx } ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
[PROOFSTEP]
refine'
  affineSpan_induction' (fun y hy => _) (fun c u hu v hv w hw => _) hx (p := fun y hy =>
    ⟨y, hy⟩ ∈ (affineSpan k (((↑) : { z // z ∈ affineSpan k A } → P) ⁻¹' A)))
    -- porting note: Lean couldn't infer the motive
[GOAL]
case mk.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
y : P
hy : y ∈ A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) y (_ : y ∈ ↑(affineSpan k A))
[PROOFSTEP]
exact subset_affineSpan _ _ hy
[GOAL]
case mk.refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ ↑(affineSpan k A)
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) u hu →
    (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) v hv →
      (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) w hw →
        (fun y hy => { val := y, property := hy } ∈ affineSpan k (Subtype.val ⁻¹' A)) (c • (u -ᵥ v) +ᵥ w)
          (_ : c • (u -ᵥ v) +ᵥ w ∈ (affineSpan k A).carrier)
[PROOFSTEP]
exact AffineSubspace.smul_vsub_vadd_mem _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤
[PROOFSTEP]
convert ext_of_direction_eq _ ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩
[GOAL]
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ direction (affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s)) = direction ⊤
[PROOFSTEP]
rw [direction_affineSpan, direction_top,
  vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _), eq_top_iff, ← h]
[GOAL]
case convert_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ Submodule.span k (range Subtype.val) ≤ Submodule.span k ((fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s))
[PROOFSTEP]
apply Submodule.span_mono
[GOAL]
case convert_1.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ range Subtype.val ⊆ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)
[PROOFSTEP]
rintro v ⟨v', rfl⟩
[GOAL]
case convert_1.h.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' ∈ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)
[PROOFSTEP]
use(v' : V) +ᵥ p
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' +ᵥ p ∈ {p} ∪ (fun v => v +ᵥ p) '' s ∧ (fun x => x -ᵥ p) (↑v' +ᵥ p) = ↑v'
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}
[PROOFSTEP]
simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self, Submodule.span_insert_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}
[PROOFSTEP]
rw [pair_comm, vectorSpan_pair]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
[PROOFSTEP]
rw [vectorSpan_pair, Submodule.mem_span_singleton]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
[PROOFSTEP]
rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
v : V
⊢ v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
[PROOFSTEP]
rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan, mem_vectorSpan_pair_rev]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
v : V
⊢ v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
[PROOFSTEP]
rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan, mem_vectorSpan_pair]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ affineSpan k {p₁, p₂} ≤ s
[PROOFSTEP]
rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ p₂ ∈ ↑s
[PROOFSTEP]
exact ⟨hp₁, hp₂⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : P
ps : Set P
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
[PROOFSTEP]
rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ affineSpan k (insert p ps) = affineSpan k ps
[PROOFSTEP]
rw [← mem_coe] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ps) = affineSpan k ps
[PROOFSTEP]
rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ vectorSpan k (insert p ps) = vectorSpan k ps
[PROOFSTEP]
simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ direction (s1 ⊔ s2) = direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ direction (s1 ⊔ s2) ≤ direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
change (affineSpan k ((s1 : Set P) ∪ s2)).direction ≤ _
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ direction (affineSpan k (↑s1 ∪ ↑s2)) ≤ direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
rw [← mem_coe] at hp1 
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
⊢ direction (affineSpan k (↑s1 ∪ ↑s2)) ≤ direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp1), Submodule.span_le]
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
⊢ (fun x => x -ᵥ p1) '' (↑s1 ∪ ↑s2) ⊆ ↑(direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1})
[PROOFSTEP]
rintro v ⟨p3, hp3, rfl⟩
[GOAL]
case refine'_1.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s1 ∪ ↑s2
⊢ (fun x => x -ᵥ p1) p3 ∈ ↑(direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1})
[PROOFSTEP]
cases' hp3 with hp3 hp3
[GOAL]
case refine'_1.intro.intro.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s1
⊢ (fun x => x -ᵥ p1) p3 ∈ ↑(direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1})
[PROOFSTEP]
rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]
[GOAL]
case refine'_1.intro.intro.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s1
⊢ ∃ y, y ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s1 ∧ y + z = (fun x => x -ᵥ p1) p3
[PROOFSTEP]
use 0, Submodule.zero_mem _, p3 -ᵥ p1, vsub_mem_direction hp3 hp1
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s1
⊢ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
[PROOFSTEP]
rw [zero_add]
[GOAL]
case refine'_1.intro.intro.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ (fun x => x -ᵥ p1) p3 ∈ ↑(direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1})
[PROOFSTEP]
rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]
[GOAL]
case refine'_1.intro.intro.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ ∃ y, y ∈ direction s1 ∧ ∃ z, z ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ∧ y + z = (fun x => x -ᵥ p1) p3
[PROOFSTEP]
use 0, Submodule.zero_mem _, p3 -ᵥ p1
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ∧ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
[PROOFSTEP]
rw [and_comm, zero_add]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ p3 -ᵥ p1 = (fun x => x -ᵥ p1) p3 ∧ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
use rfl
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
rw [← vsub_add_vsub_cancel p3 p2 p1, Submodule.mem_sup]
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ ↑s1
hp2 : p2 ∈ s2
p3 : P
hp3 : p3 ∈ ↑s2
⊢ ∃ y, y ∈ direction s2 ∧ ∃ z, z ∈ Submodule.span k {p2 -ᵥ p1} ∧ y + z = p3 -ᵥ p2 + (p2 -ᵥ p1)
[PROOFSTEP]
use p3 -ᵥ p2, vsub_mem_direction hp3 hp2, p2 -ᵥ p1, Submodule.mem_span_singleton_self _
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ direction s1 ⊔ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ≤ direction (s1 ⊔ s2)
[PROOFSTEP]
refine' sup_le (sup_direction_le _ _) _
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ Submodule.span k {p2 -ᵥ p1} ≤ direction (s1 ⊔ s2)
[PROOFSTEP]
rw [direction_eq_vectorSpan, vectorSpan_def]
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s1
hp2 : p2 ∈ s2
⊢ Submodule.span k {p2 -ᵥ p1} ≤ Submodule.span k (↑(s1 ⊔ s2) -ᵥ ↑(s1 ⊔ s2))
[PROOFSTEP]
exact
  sInf_le_sInf fun p hp =>
    Set.Subset.trans
      (Set.singleton_subset_iff.2
        (vsub_mem_vsub (mem_spanPoints k p2 _ (Set.mem_union_right _ hp2))
          (mem_spanPoints k p1 _ (Set.mem_union_left _ hp1))))
      hp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (affineSpan k (insert p2 ↑s)) = Submodule.span k {p2 -ᵥ p1} ⊔ direction s
[PROOFSTEP]
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (affineSpan k (↑s ∪ ↑(affineSpan k {p2}))) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
change (s ⊔ affineSpan k { p2 }).direction = _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (s ⊔ affineSpan k {p2}) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
rw [direction_sup hp1 (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction s ⊔ vectorSpan k {p2} ⊔ Submodule.span k {p2 -ᵥ p1} = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ s
p2 p : P
⊢ p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
rw [← mem_coe] at hp1 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp1)),
  direction_affineSpan_insert hp1, Submodule.mem_sup]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) ↔
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) →
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
rintro ⟨v1, hv1, v2, hv2, hp⟩
[GOAL]
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : v1 ∈ Submodule.span k {p2 -ᵥ p1}
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
rw [Submodule.mem_span_singleton] at hv1 
[GOAL]
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : ∃ a, a • (p2 -ᵥ p1) = v1
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
rcases hv1 with ⟨r, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
[PROOFSTEP]
use r, v2 +ᵥ p1, vadd_mem_of_mem_direction hv2 hp1
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
[PROOFSTEP]
symm at hp 
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
[PROOFSTEP]
rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp 
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp✝ : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
hp : p = r • (p2 -ᵥ p1) + v2 +ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
[PROOFSTEP]
rw [hp, vadd_vadd]
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0) →
    ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1
[PROOFSTEP]
rintro ⟨r, p3, hp3, rfl⟩
[GOAL]
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
[PROOFSTEP]
use r • (p2 -ᵥ p1), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p3 -ᵥ p1, vsub_mem_direction hp3 hp1
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ r • (p2 -ᵥ p1) + (p3 -ᵥ p1) = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
[PROOFSTEP]
rw [vadd_vsub_assoc, add_comm]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ Submodule.map f.linear (vectorSpan k s) = vectorSpan k (↑f '' s)
[PROOFSTEP]
rw [vectorSpan_def, vectorSpan_def, f.image_vsub_image, Submodule.span_image]
  -- porting note: Lean unfolds things too far with `simp` here.
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ ∀ (c : k) {p1 p2 p3 : P₂}, p1 ∈ ↑f '' ↑s → p2 ∈ ↑f '' ↑s → p3 ∈ ↑f '' ↑s → c • (p1 -ᵥ p2) +ᵥ p3 ∈ ↑f '' ↑s
[PROOFSTEP]
rintro t - - - ⟨p₁, h₁, rfl⟩ ⟨p₂, h₂, rfl⟩ ⟨p₃, h₃, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
⊢ t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃ ∈ ↑f '' ↑s
[PROOFSTEP]
use t • (p₁ -ᵥ p₂) +ᵥ p₃
[GOAL]
case h
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s ∧ ↑f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃
[PROOFSTEP]
suffices t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s by {
  simp only [SetLike.mem_coe, true_and, this]
  rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
}
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s ∧ ↑f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃
[PROOFSTEP]
{ simp only [SetLike.mem_coe, true_and, this]
  rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
}
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s ∧ ↑f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃
[PROOFSTEP]
simp only [SetLike.mem_coe, true_and, this]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ ↑f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃
[PROOFSTEP]
rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
[GOAL]
case h
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
[PROOFSTEP]
exact s.smul_vsub_vadd_mem t h₁ h₂ h₃
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f✝ f : P₁ →ᵃ[k] P₂
x : P₂
s : AffineSubspace k P₁
⊢ x ∈ map f s ↔ ∃ y, y ∈ s ∧ ↑f y = x
[PROOFSTEP]
simpa only [bex_def] using mem_image_iff_bex
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥
[PROOFSTEP]
rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h 
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥
[PROOFSTEP]
rw [h, map_bot]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ direction (map f s) = Submodule.map f.linear (direction s)
[PROOFSTEP]
rw [direction_eq_vectorSpan, direction_eq_vectorSpan, coe_map, AffineMap.vectorSpan_image_eq_submodule_map]
  -- porting note: again, Lean unfolds too aggressively with `simp`
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k (↑f '' s)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
[GOAL]
case inl
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
⊢ map f (affineSpan k ∅) = affineSpan k (↑f '' ∅)
[PROOFSTEP]
rw [image_empty, span_empty, span_empty, map_bot]
  -- porting note: I don't know exactly why this `simp` was broken.
[GOAL]
case inr.intro
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k (↑f '' s)
[PROOFSTEP]
apply ext_of_direction_eq
[GOAL]
case inr.intro.hd
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ direction (map f (affineSpan k s)) = direction (affineSpan k (↑f '' s))
[PROOFSTEP]
simp [direction_affineSpan]
[GOAL]
case inr.intro.hn
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ Set.Nonempty (↑(map f (affineSpan k s)) ∩ ↑(affineSpan k (↑f '' s)))
[PROOFSTEP]
exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp), subset_affineSpan k _ (mem_image_of_mem f hp)⟩
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ↑f
⊢ AffineSubspace.map f ⊤ = ⊤
[PROOFSTEP]
rw [← AffineSubspace.ext_iff]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ↑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤
[PROOFSTEP]
exact image_univ_of_surjective hf
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
hf : Function.Surjective ↑f
h : affineSpan k s = ⊤
⊢ affineSpan k (↑f '' s) = ⊤
[PROOFSTEP]
rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k s = ⊤ ↔ affineSpan k (↑e '' s) = ⊤
[PROOFSTEP]
refine' ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, _⟩
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k (↑e '' s) = ⊤ → affineSpan k s = ⊤
[PROOFSTEP]
intro h
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ affineSpan k s = ⊤
[PROOFSTEP]
have : s = e.symm '' (e '' s) := by rw [← image_comp]; simp
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ s = ↑(symm e) '' (↑e '' s)
[PROOFSTEP]
rw [← image_comp]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ s = ↑(symm e) ∘ ↑e '' s
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k s = ⊤
[PROOFSTEP]
rw [this]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k (↑(symm e) '' (↑e '' s)) = ⊤
[PROOFSTEP]
exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₂
t : k
p₁ p₂ p₃ : P₁
hp₁ : ↑f p₁ ∈ s
hp₂ : ↑f p₂ ∈ s
hp₃ : ↑f p₃ ∈ s
⊢ ↑f (t • (p₁ -ᵥ p₂) +ᵥ p₃) ∈ s
[PROOFSTEP]
rw [AffineMap.map_vadd, LinearMap.map_smul, AffineMap.linearMap_vsub]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₂
t : k
p₁ p₂ p₃ : P₁
hp₁ : ↑f p₁ ∈ s
hp₂ : ↑f p₂ ∈ s
hp₃ : ↑f p₃ ∈ s
⊢ t • (↑f p₁ -ᵥ ↑f p₂) +ᵥ ↑f p₃ ∈ s
[PROOFSTEP]
apply s.smul_vsub_vadd_mem _ hp₁ hp₂ hp₃
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
⊢ comap f ⊤ = ⊤
[PROOFSTEP]
rw [← ext_iff]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
⊢ ↑(comap f ⊤) = ↑⊤
[PROOFSTEP]
exact preimage_univ (f := f)
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ ≃ᵃ[k] P₂
s : Set P₂
⊢ comap (↑f) (affineSpan k s) = affineSpan k (↑f ⁻¹' s)
[PROOFSTEP]
rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ ∥ s₁
[PROOFSTEP]
rcases h with ⟨v, rfl⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ map (↑(constVAdd k P v)) s₁ ∥ s₁
[PROOFSTEP]
refine' ⟨-v, _⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)
[PROOFSTEP]
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_self, constVAdd_zero, coe_refl_to_affineMap, map_id]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ s = map (↑(constVAdd k P 0)) s
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ s₃ : AffineSubspace k P
h₁₂ : s₁ ∥ s₂
h₂₃ : s₂ ∥ s₃
⊢ s₁ ∥ s₃
[PROOFSTEP]
rcases h₁₂ with ⟨v₁₂, rfl⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂)) s₁ ∥ s₃
⊢ s₁ ∥ s₃
[PROOFSTEP]
rcases h₂₃ with ⟨v₂₃, rfl⟩
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁)
[PROOFSTEP]
refine' ⟨v₂₃ + v₁₂, _⟩
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁) = map (↑(constVAdd k P (v₂₃ + v₁₂))) s₁
[PROOFSTEP]
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ direction s₁ = direction s₂
[PROOFSTEP]
rcases h with ⟨v, rfl⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ direction s₁ = direction (map (↑(constVAdd k P v)) s₁)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ s ∥ ⊥ ↔ s = ⊥
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h ▸ Parallel.refl _⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : s ∥ ⊥
⊢ s = ⊥
[PROOFSTEP]
rcases h with ⟨v, h⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v)) s
⊢ s = ⊥
[PROOFSTEP]
rwa [eq_comm, map_eq_bot_iff] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ ⊥ ∥ s ↔ s = ⊥
[PROOFSTEP]
rw [parallel_comm, parallel_bot_iff_eq_bot]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ∥ s₂ ↔ direction s₁ = direction s₂ ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
[PROOFSTEP]
refine' ⟨fun h => ⟨h.direction_eq, _, _⟩, fun h => _⟩
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁ = ⊥ → s₂ = ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₂ : AffineSubspace k P
h : ⊥ ∥ s₂
⊢ s₂ = ⊥
[PROOFSTEP]
exact bot_parallel_iff_eq_bot.1 h
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ = ⊥ → s₁ = ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
h : s₁ ∥ ⊥
⊢ s₁ = ⊥
[PROOFSTEP]
exact parallel_bot_iff_eq_bot.1 h
[GOAL]
case refine'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : direction s₁ = direction s₂ ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂
[PROOFSTEP]
rcases h with ⟨hd, hb⟩
[GOAL]
case refine'_3.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
⊢ s₁ ∥ s₂
[PROOFSTEP]
by_cases hs₁ : s₁ = ⊥
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₁ ∥ s₂
[PROOFSTEP]
rw [hs₁, bot_parallel_iff_eq_bot]
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₂ = ⊥
[PROOFSTEP]
exact hb.1 hs₁
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
⊢ s₁ ∥ s₂
[PROOFSTEP]
have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
⊢ s₁ ∥ s₂
[PROOFSTEP]
rcases(nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
[GOAL]
case neg.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
⊢ s₁ ∥ s₂
[PROOFSTEP]
rcases(nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
[GOAL]
case neg.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₁ ∥ s₂
[PROOFSTEP]
refine' ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ _).2 _⟩
[GOAL]
case neg.intro.intro.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁
[PROOFSTEP]
rw [mem_map]
[GOAL]
case neg.intro.intro.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ ∃ y, y ∈ s₁ ∧ ↑↑(constVAdd k P (p₂ -ᵥ p₁)) y = p₂
[PROOFSTEP]
refine' ⟨p₁, hp₁, _⟩
[GOAL]
case neg.intro.intro.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ ↑↑(constVAdd k P (p₂ -ᵥ p₁)) p₁ = p₂
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : direction s₁ = direction s₂
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ direction s₂ = direction (map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁)
[PROOFSTEP]
simpa using hd.symm
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ vectorSpan k s₁ = vectorSpan k s₂
[PROOFSTEP]
simp_rw [← direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ direction (affineSpan k s₁) = direction (affineSpan k s₂)
[PROOFSTEP]
exact h.direction_eq
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
[PROOFSTEP]
repeat
  rw [← direction_affineSpan, ← affineSpan_eq_bot k]
    -- porting note: more issues with `simp`
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_eq_bot k]
  -- porting note: more issues with `simp`
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ direction (affineSpan k s₁) = vectorSpan k s₂ ∧ (affineSpan k s₁ = ⊥ ↔ s₂ = ∅)
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_eq_bot k]
  -- porting note: more issues with `simp`
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_eq_bot k]
  -- porting note: more issues with `simp`
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
[PROOFSTEP]
exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
⊢ affineSpan k {p₁, p₂} ∥ affineSpan k {p₃, p₄} ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}
[PROOFSTEP]
simp [affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, ← not_nonempty_iff_eq_empty]
