Theorem: orthoHyperplane.Finite (src/Cutspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite (orthoHyperplane x)
Tactic:
unfold orthoHyperplane
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, and_true, Set.finite_singleton, Set.Finite.insert]
State after:
no goals