-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem direction_sup {s₁ s₂ : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s₁) (hp₂ : p₂ ∈ s₂) :
    (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ p₂ -ᵥ p₁

Proof state:
k : Type 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
refine le_antisymm ?_ ?_

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁} ≤ (s₁ ⊔ s₂).direction

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁} ≤ (s₁ ⊔ s₂).direction

Tactic:
refine sup_le (sup_direction_le _ _) ?_

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ Submodule.span k {p₂ -ᵥ p₁} ≤ (s₁ ⊔ s₂).direction

Proof state:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ ∃ y ∈ s₂.direction, ∃ z ∈ Submodule.span k {p₂ -ᵥ p₁}, y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)

Tactic:
use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _

Result:
no goals

Proof state:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ 0 + (p₃ -ᵥ p₁) = (fun x => x -ᵥ p₁) p₃

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
⊢ (fun x => x -ᵥ p₁) '' (↑s₁ ∪ ↑s₂) ⊆ ↑(s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁})

Tactic:
rintro v ⟨p₃, hp₃, rfl⟩

Result:
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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁ ∪ ↑s₂
⊢ (fun x => x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁})

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
⊢ (affineSpan k (↑s₁ ∪ ↑s₂)).direction ≤ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp₁),
  Submodule.span_le]

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
⊢ (fun x => x -ᵥ p₁) '' (↑s₁ ∪ ↑s₂) ⊆ ↑(s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁})

Proof state:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
rw [← vsub_add_vsub_cancel p₃ p₂ p₁, Submodule.mem_sup]

Result:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ ∃ y ∈ s₂.direction, ∃ z ∈ Submodule.span k {p₂ -ᵥ p₁}, y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ Submodule.span k {p₂ -ᵥ p₁} ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ s₂))

Tactic:
exact
  sInf_le_sInf fun p hp =>
    Set.Subset.trans
      (Set.singleton_subset_iff.2
        (vsub_mem_vsub (mem_spanPoints k p₂ _ (Set.mem_union_right _ hp₂))
          (mem_spanPoints k p₁ _ (Set.mem_union_left _ hp₁))))
      hp

Result:
no goals

Proof state:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ = (fun x => x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
use rfl

Result:
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Proof state:
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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ (fun x => x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁})

Tactic:
rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]

Result:
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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ ∃ y ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s₁.direction, y + z = (fun x => x -ᵥ p₁) p₃

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
change (affineSpan k ((s₁ : Set P) ∪ s₂)).direction ≤ _

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (affineSpan k (↑s₁ ∪ ↑s₂)).direction ≤ s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Proof state:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ Submodule.span k {p₂ -ᵥ p₁} ≤ (s₁ ⊔ s₂).direction

Tactic:
rw [direction_eq_vectorSpan, vectorSpan_def]

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ Submodule.span k {p₂ -ᵥ p₁} ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ s₂))