Theorem: frontierHalfspace_Hyperplane (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
have := ContinuousLinearMap.frontier_preimage Hi_.f.1 (unitSphereDual_surj Hi_.f) (Set.Iic Hi_.α)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' frontier (Set.Iic Hi_.α)
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' frontier (Set.Iic Hi_.α)
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
simp only [ne_eq, LinearMap.coe_toContinuousLinearMap', Set.nonempty_Ioi, frontier_Iic'] at this
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
change frontier ( Hi_.f.1 ⁻¹' {x | x ≤ Hi_.α}) = Hi_.f.1 ⁻¹' {Hi_.α} at this
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Hi_.h, this]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
clear this
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
unfold Set.preimage
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ {x | ↑Hi_.f x ∈ {Hi_.α}} = {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ {x | ↑Hi_.f x ∈ {Hi_.α}} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
simp only [ne_eq, Set.mem_singleton_iff]
State after:
no goals