Theorem: Hpolytope_same (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ Hpolytope hH_1 = Hpolytope hH_2
Tactic:
unfold Hpolytope
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ ⋂₀ (SetLike.coe '' H_) = ⋂₀ (SetLike.coe '' H_)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ ⋂₀ (SetLike.coe '' H_) = ⋂₀ (SetLike.coe '' H_)
Tactic:
rfl
State after:
no goals