-- 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:
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₁})

Tactic:
rcases hp₃ with hp₃ | hp₃

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

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
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₁})

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

Tactic:
use 0, Submodule.zero_mem _, p₃ -ᵥ p₁, vsub_mem_direction hp₃ hp₁

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₁
⊢ 0 + (p₃ -ᵥ p₁) = (fun x => x -ᵥ p₁) p₃

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₁ ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁} ∧ 0 + (p₃ -ᵥ p₁) = (fun x => x -ᵥ p₁) p₃

Tactic:
rw [and_comm, zero_add]

Result:
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₁}

Proof state:
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
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, SetLike.mem_coe, Submodule.mem_sup]

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

Tactic:
rw [← mem_coe] at hp₁

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

Tactic:
use 0, Submodule.zero_mem _, p₃ -ᵥ p₁

Result:
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₁ ∈ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁} ∧ 0 + (p₃ -ᵥ p₁) = (fun x => x -ᵥ p₁) p₃