feat: AList.keys_subset_keys_of_entries_subset_entries (#6150)

leanprover-community · Aug 1, 2023 · fa24f8f · fa24f8f
1 parent 4d41532
commit fa24f8f
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Mathlib/Data/List/AList.lean b/Mathlib/Data/List/AList.lean
@@ -180,6 +180,15 @@ theorem perm_lookup {a : α} {s₁ s₂ : AList β} (p : s₁.entries ~ s₂.ent
 instance (a : α) (s : AList β) : Decidable (a ∈ s) :=
   decidable_of_iff _ lookup_isSome
 
+theorem keys_subset_keys_of_entries_subset_entries
+    {s₁ s₂ : AList β} (h : s₁.entries ⊆ s₂.entries) : s₁.keys ⊆ s₂.keys := by
+  intro k hk
+  letI : DecidableEq α := Classical.decEq α
+  have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
+  rw [← mem_lookup_iff, Option.mem_def] at this
+  rw [← mem_keys, ← lookup_isSome, this]
+  exact Option.isSome_some
+
 /-! ### replace -/