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}

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)
k : Type 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}
refine' le_antisymm _ _
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}
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}
change (affineSpan k ((s1 : Set P) ∪ s2)).direction ≤ _
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}
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}
rw [← mem_coe] at hp1
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})
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}
rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp1),
  Submodule.span_le]
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})
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})
rintro v ⟨p3, hp3, rfl⟩
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})

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})
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})
cases' hp3 with hp3 hp3
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
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})
rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]
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
⊢ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
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
use 0, Submodule.zero_mem _, p3 -ᵥ p1, vsub_mem_direction hp3 hp1
no goals
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
⊢ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
rw [zero_add]
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
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})
rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]
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
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ∧ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
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
use 0, Submodule.zero_mem _, p3 -ᵥ p1
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
⊢ p3 -ᵥ p1 = (fun x => x -ᵥ p1) p3 ∧ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
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
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1} ∧ 0 + (p3 -ᵥ p1) = (fun x => x -ᵥ p1) p3
rw [and_comm, zero_add]
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
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
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
⊢ p3 -ᵥ p1 = (fun x => x -ᵥ p1) p3 ∧ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
use rfl
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 s2 ∧ ∃ z, z ∈ Submodule.span k {p2 -ᵥ p1} ∧ y + z = p3 -ᵥ p2 + (p2 -ᵥ p1)
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
⊢ p3 -ᵥ p1 ∈ direction s2 ⊔ Submodule.span k {p2 -ᵥ p1}
rw [← vsub_add_vsub_cancel p3 p2 p1, Submodule.mem_sup]
no goals
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 s2 ∧ ∃ z, z ∈ Submodule.span k {p2 -ᵥ p1} ∧ y + z = p3 -ᵥ p2 + (p2 -ᵥ p1)
use p3 -ᵥ p2, vsub_mem_direction hp3 hp2, p2 -ᵥ p1, Submodule.mem_span_singleton_self _
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)
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)
refine' sup_le (sup_direction_le _ _) _
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))
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)
rw [direction_eq_vectorSpan, vectorSpan_def]
no goals
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))
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