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
k : Type 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
ext v
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
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
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]
no goals
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
conv_lhs =>
  congr
  ext
  rw [← neg_vsub_eq_vsub_rev, neg_inj]