Theorem: orthoHyperplane_mem (src/Cutspace.lean)

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

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (orthoHyperplane x) ↔ ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [mem_cutSpace]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) ↔ ⟪↑x, y⟫_ℝ = 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) ↔ ⟪↑x, y⟫_ℝ = 0
Tactic:
constructor
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) → ⟪↑x, y⟫_ℝ = 0

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ ⟪↑x, y⟫_ℝ = 0 → ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) → ⟪↑x, y⟫_ℝ = 0
Tactic:
intro h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
have h1 := h (Halfspace.mk (pointDualLin x) 0)
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 :
  { f := pointDualLin x, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin x, α := 0 }.f y ≤ { f := pointDualLin x, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 :
  { f := pointDualLin x, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin x, α := 0 }.f y ≤ { f := pointDualLin x, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
simp only [pointDualLin, ne_eq, map_inv₀, IsROrC.conj_to_real, orthoHyperplane, Set.mem_singleton_iff,
  Halfspace.mk.injEq, and_true, Set.mem_insert_iff, true_or, forall_true_left, InnerProductSpace.toDual_apply,
  inner_smul_left] at h1
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
have h2 := h (Halfspace.mk (pointDualLin ⟨ -x.1, by rw [neg_ne_zero]; exact x.2 ⟩) 0)
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 :
  { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }.f y ≤
      { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 :
  { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }.f y ≤
      { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
simp only [pointDualLin, ne_eq, norm_neg, smul_neg, map_inv₀, IsROrC.conj_to_real, orthoHyperplane,
  Set.mem_singleton_iff, Halfspace.mk.injEq, Subtype.mk.injEq, and_true, Set.mem_insert_iff,
  or_true, forall_true_left, InnerProductSpace.toDual_apply, inner_neg_left, inner_smul_left] at h2
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : -(‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ) ≤ 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : -(‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ) ≤ 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [neg_le, neg_zero] at h2
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
have := le_antisymm h1 h2
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
this : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
this : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [mul_eq_zero] at this
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
this : ‖↑x‖⁻¹ = 0 ∨ ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
this : ‖↑x‖⁻¹ = 0 ∨ ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
cases' this with h3 h4
State after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ‖↑x‖⁻¹ = 0
⊢ ⟪↑x, y⟫_ℝ = 0

case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h4 : ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ -↑x ≠ 0
Tactic:
rw [neg_ne_zero]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ ↑x ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ ↑x ≠ 0
Tactic:
exact x.2
State after:
no goals

State before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ‖↑x‖⁻¹ = 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [inv_eq_zero, norm_eq_zero] at h3
State after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ↑x = 0
⊢ ⟪↑x, y⟫_ℝ = 0

State before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ↑x = 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
exfalso
State after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ↑x = 0
⊢ False

State before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h3 : ↑x = 0
⊢ False
Tactic:
exact x.2 h3
State after:
no goals

State before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
h2 : 0 ≤ ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ
h4 : ⟪↑x, y⟫_ℝ = 0
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
exact h4
State after:
no goals

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ ⟪↑x, y⟫_ℝ = 0 → ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
Tactic:
intro h H hH
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H ∈ orthoHyperplane x
⊢ ↑H.f y ≤ H.α

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H ∈ orthoHyperplane x
⊢ ↑H.f y ≤ H.α
Tactic:
unfold orthoHyperplane at hH
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H ∈ {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}
⊢ ↑H.f y ≤ H.α

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H ∈ {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}
⊢ ↑H.f y ≤ H.α
Tactic:
simp only [ne_eq, Set.mem_singleton_iff, Halfspace.mk.injEq, and_true, Set.mem_insert_iff] at hH
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H = { f := pointDualLin x, α := 0 } ∨ H = { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }
⊢ ↑H.f y ≤ H.α

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ⟪↑x, y⟫_ℝ = 0
H : Halfspace E
hH : H = { f := pointDualLin x, α := 0 } ∨ H = { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }
⊢ ↑H.f y ≤ H.α
Tactic:
cases' hH with H H <;>
simp only [H, pointDualLin, norm_neg, smul_neg, map_inv₀, IsROrC.conj_to_real, InnerProductSpace.toDual_apply,
    inner_neg_left, inner_smul_left, neg_le, neg_zero, h, mul_zero, le_refl]
State after:
no goals