α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
⊢ {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
⊢ IsClosed {x | 0 ≤ x}
suffices { x : E | 0 ≤ x } = NegPart.neg ⁻¹' {(0 : E)} by
  rw [this]
  exact IsClosed.preimage continuous_neg' isClosed_singleton
case h
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
x : E
⊢ x ∈ {x | 0 ≤ x} ↔ x ∈ NegPart.neg ⁻¹' {0}
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
⊢ {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
ext1 x
no goals
case h
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
x : E
⊢ x ∈ {x | 0 ≤ x} ↔ x ∈ NegPart.neg ⁻¹' {0}
simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq,
  @neg_eq_zero_iff E _ _ (OrderedAddCommGroup.to_covariantClass_left_le E)  ]
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed (NegPart.neg ⁻¹' {0})
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed {x | 0 ≤ x}
rw [this]
no goals
α : Type ?u.119963
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_1
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed (NegPart.neg ⁻¹' {0})
exact IsClosed.preimage continuous_neg' isClosed_singleton