[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
s t : ClopenUpperSet α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
t : ClopenUpperSet α
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
upper'✝ : IsUpperSet { carrier := carrier✝, clopen' := clopen'✝ }.carrier
h :
  (fun s => s.carrier) { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ } =
    (fun s => s.carrier) t
⊢ { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LE α
inst✝¹ : TopologicalSpace β
inst✝ : LE β
carrier✝¹ : Set α
clopen'✝¹ : IsClopen carrier✝¹
upper'✝¹ : IsUpperSet { carrier := carrier✝¹, clopen' := clopen'✝¹ }.carrier
carrier✝ : Set α
clopen'✝ : IsClopen carrier✝
upper'✝ : IsUpperSet { carrier := carrier✝, clopen' := clopen'✝ }.carrier
h :
  (fun s => s.carrier) { toClopens := { carrier := carrier✝¹, clopen' := clopen'✝¹ }, upper' := upper'✝¹ } =
    (fun s => s.carrier) { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ }
⊢ { toClopens := { carrier := carrier✝¹, clopen' := clopen'✝¹ }, upper' := upper'✝¹ } =
    { toClopens := { carrier := carrier✝, clopen' := clopen'✝ }, upper' := upper'✝ }
[PROOFSTEP]
congr
