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