congr
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
univ_mem_sets✝¹ : Set.univ ∈ sets✝¹
superset_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }
no goals