internlm/Lean-Github huggingface dataset:
Theorem: orthoHyperplane_mem
Proof 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)
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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]
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof state after:
no goals
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof 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
Theorem: orthoHyperplane_mem
Proof 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
Proof state after:
no goals
Theorem: orthoHyperplane_mem
Proof 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
Proof state after:
no goals
Theorem: orthoHyperplane_mem
Proof 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
Proof 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.α
Theorem: orthoHyperplane_mem
Proof 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
Proof 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.α
Theorem: orthoHyperplane_mem
Proof 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
Proof 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.α
Theorem: orthoHyperplane_mem
Proof 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]
Proof state after:
no goals
Theorem: cutSpace_sUnion_orthoHyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
⊢ ∀ (y : E), y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
Tactic:
intro y
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
Theorem: cutSpace_sUnion_orthoHyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i
Tactic:
unfold cutSpace
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ ⋂₀ (SetLike.coe '' ⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ ⋂₀ (SetLike.coe '' ↑i)
Theorem: cutSpace_sUnion_orthoHyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set { x // x ≠ 0 }
y : E
⊢ y ∈ ⋂₀ (SetLike.coe '' ⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ ⋂₀ (SetLike.coe '' ↑i)
Tactic:
rw [Set.sUnion_eq_iUnion, Set.image_iUnion, Set.sInter_iUnion, Set.mem_iInter]
Proof state after:
no goals
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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]
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof state after:
no goals
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof 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 })
Theorem: orthoHyperplanes_mem
Proof 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]
Proof 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
Theorem: orthoHyperplanes_mem
Proof 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
Proof state after:
no goals
Theorem: Submodule_cut_finite
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p)
Tactic:
apply Set.Finite.sUnion ?_ (fun t ht => by
  rcases ht with ⟨ x, _, rfl ⟩
  exact orthoHyperplane.Finite _)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))))
Theorem: Submodule_cut_finite
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))))
Tactic:
apply Set.Finite.image
Proof state after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
Theorem: Submodule_cut_finite
Proof state before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
Tactic:
apply Set.Finite.preimage (Set.injOn_of_injective Subtype.val_injective _)
Proof state after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
Theorem: Submodule_cut_finite
Proof state before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
Tactic:
apply Set.finite_range
Proof state after:
no goals
Theorem: Submodule_cut_finite
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
t : Set (Halfspace E)
ht : t ∈ orthoHyperplane '' (Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)))
⊢ Set.Finite t
Tactic:
rcases ht with ⟨ x, _, rfl ⟩
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))
⊢ Set.Finite (orthoHyperplane x)
Theorem: Submodule_cut_finite
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ))
⊢ Set.Finite (orthoHyperplane x)
Tactic:
exact orthoHyperplane.Finite _
Proof state after:
no goals
Theorem: Submodule_cutspace
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ∃ H_, Set.Finite H_ ∧ ↑p = cutSpace H_
Tactic:
use Submodule_cut p
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p) ∧ ↑p = cutSpace (Submodule_cut p)
Theorem: Submodule_cutspace
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ Set.Finite (Submodule_cut p) ∧ ↑p = cutSpace (Submodule_cut p)
Tactic:
use Submodule_cut_finite p
Proof state after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ↑p = cutSpace (Submodule_cut p)
Theorem: Submodule_cutspace
Proof state before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
⊢ ↑p = cutSpace (Submodule_cut p)
Tactic:
ext x
Proof state after:
case right.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p ↔ x ∈ cutSpace (Submodule_cut p)
Theorem: Submodule_cutspace
Proof state before:
case right.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p ↔ x ∈ cutSpace (Submodule_cut p)
Tactic:
constructor
Proof state after:
case right.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p → x ∈ cutSpace (Submodule_cut p)

case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ cutSpace (Submodule_cut p) → x ∈ ↑p