Theorem: orthoHyperplanes_mem (src/Cutspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
⊢ ∀ (y : E), y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
Tactic:
intro y
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [cutSpace_sUnion_orthoHyperplane]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i) ↔ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i) ↔ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
Tactic:
constructor
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i) → ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0) → ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i) → ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
Tactic:
intro h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
⊢ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
⊢ ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
Tactic:
intro x hx
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
x : { x // x ≠ 0 }
hx : x ∈ X
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
x : { x // x ≠ 0 }
hx : x ∈ X
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
simp at h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
x : { x // x ≠ 0 }
hx : x ∈ X
h :
  ∀ (a : Set (Halfspace E)) (x : E) (x_1 : ¬x = 0),
    { val := x, property := x_1 } ∈ X → orthoHyperplane { val := x, property := x_1 } = a → y ∈ cutSpace a
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
x : { x // x ≠ 0 }
hx : x ∈ X
h :
  ∀ (a : Set (Halfspace E)) (x : E) (x_1 : ¬x = 0),
    { val := x, property := x_1 } ∈ X → orthoHyperplane { val := x, property := x_1 } = a → y ∈ cutSpace a
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
specialize h (orthoHyperplane x) x.1 x.2 hx rfl
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
x : { x // x ≠ 0 }
hx : x ∈ X
h : y ∈ cutSpace (orthoHyperplane x)
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
x : { x // x ≠ 0 }
hx : x ∈ X
h : y ∈ cutSpace (orthoHyperplane x)
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
exact (orthoHyperplane_mem x y).mp h
State after:
no goals

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ (∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0) → ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
Tactic:
intro h
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
⊢ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
⊢ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
Tactic:
simp
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
⊢ ∀ (a : Set (Halfspace E)) (x : E) (x_1 : ¬x = 0),
    { val := x, property := x_1 } ∈ X → orthoHyperplane { val := x, property := x_1 } = a → y ∈ cutSpace a

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
⊢ ∀ (a : Set (Halfspace E)) (x : E) (x_1 : ¬x = 0),
    { val := x, property := x_1 } ∈ X → orthoHyperplane { val := x, property := x_1 } = a → y ∈ cutSpace a
Tactic:
rintro a x1 x2 hx rfl
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
x1 : E
x2 : ¬x1 = 0
hx : { val := x1, property := x2 } ∈ X
⊢ y ∈ cutSpace (orthoHyperplane { val := x1, property := x2 })

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
x1 : E
x2 : ¬x1 = 0
hx : { val := x1, property := x2 } ∈ X
⊢ y ∈ cutSpace (orthoHyperplane { val := x1, property := x2 })
Tactic:
rw [orthoHyperplane_mem]
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
x1 : E
x2 : ¬x1 = 0
hx : { val := x1, property := x2 } ∈ X
⊢ ⟪↑{ val := x1, property := x2 }, y⟫_ℝ = 0

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
h : ∀ x ∈ X, ⟪↑x, y⟫_ℝ = 0
x1 : E
x2 : ¬x1 = 0
hx : { val := x1, property := x2 } ∈ X
⊢ ⟪↑{ val := x1, property := x2 }, y⟫_ℝ = 0
Tactic:
exact h _ hx
State after:
no goals