Theorem: Hpolytope.I_mem (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ ∀ (Hi_ : Halfspace E), Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
rintro Hi_
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
unfold I
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
rw [Set.mem_setOf]
State after:
no goals