Theorem: Halfspace_translation.injective (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Function.Injective fun x_1 => Halfspace_translation x x_1
Tactic:
intro H1 H2 h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ H1 = H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ H1 = H2
Tactic:
rw [SetLike.ext_iff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ ∀ (x : E), x ∈ H1 ↔ x ∈ H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ ∀ (x : E), x ∈ H1 ↔ x ∈ H2
Tactic:
intro y
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
rw [SetLike.ext_iff] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : ∀ (x_1 : E), x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H1 ↔ x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : ∀ (x_1 : E), x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H1 ↔ x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
specialize h (y + x)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y + x ∈ (fun x_1 => Halfspace_translation x x_1) H1 ↔ y + x ∈ (fun x_1 => Halfspace_translation x x_1) H2
⊢ y ∈ H1 ↔ y ∈ H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y + x ∈ (fun x_1 => Halfspace_translation x x_1) H1 ↔ y + x ∈ (fun x_1 => Halfspace_translation x x_1) H2
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
rw [← SetLike.mem_coe, ← SetLike.mem_coe, mem_Halfspace_translation, mem_Halfspace_translation, add_sub_cancel] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y ∈ ↑H1 ↔ y ∈ ↑H2
⊢ y ∈ H1 ↔ y ∈ H2

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y ∈ ↑H1 ↔ y ∈ ↑H2
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
exact h
State after:
no goals