-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem coe_direction_eq_vsub_set_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (· -ᵥ p) '' s

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s ≤ (fun x => x -ᵥ p) '' ↑s

Tactic:
rintro v ⟨p₁, hp₁, p₂, hp₂, rfl⟩

Result:
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
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
⊢ (fun x1 x2 => x1 -ᵥ x2) p₁ p₂ ∈ (fun x => x -ᵥ p) '' ↑s

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s.direction = (fun x => x -ᵥ p) '' ↑s

Tactic:
rw [coe_direction_eq_vsub_set ⟨p, hp⟩]

Result:
k : Type 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

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ (fun x => x -ᵥ p) '' ↑s ≤ ↑s -ᵥ ↑s

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

Result:
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
p₂ : P
hp₂ : p₂ ∈ ↑s
⊢ (fun x => x -ᵥ p) p₂ ∈ ↑s -ᵥ ↑s

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

Tactic:
exact ⟨p₂, hp₂, p, hp, rfl⟩

Result:
no goals

Proof state:
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
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
⊢ (fun x1 x2 => x1 -ᵥ x2) p₁ p₂ ∈ (fun x => x -ᵥ p) '' ↑s

Tactic:
exact ⟨(p₁ -ᵥ p₂) +ᵥ p,
  vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩

Result:
no goals

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s = (fun x => x -ᵥ p) '' ↑s

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s ≤ (fun x => x -ᵥ p) '' ↑s

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