Theorem: mem_Halfspace_translation (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
⊢ ∀ (y : E), y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_
Tactic:
intro y
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_
Tactic:
rw [Halfspace_translation.S, Set.image_add_right, Set.mem_preimage, sub_eq_add_neg]
State after:
no goals