From ecec87460a0ba1a2a29d4e96706704654982750d Mon Sep 17 00:00:00 2001
From: Craig Disselkoen <cdiss@amazon.com>
Date: Tue, 30 Jan 2024 17:50:25 +0000
Subject: [PATCH] new tactic unlocked: exists

---
 cedar-lean/Cedar/Data/List.lean                    |  4 ++--
 cedar-lean/Cedar/Data/Map.lean                     |  9 +++------
 cedar-lean/Cedar/Thm/Authorization/Authorizer.lean | 10 +++++-----
 3 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/cedar-lean/Cedar/Data/List.lean b/cedar-lean/Cedar/Data/List.lean
index 09b1b558e..9fa2cf1de 100644
--- a/cedar-lean/Cedar/Data/List.lean
+++ b/cedar-lean/Cedar/Data/List.lean
@@ -168,7 +168,7 @@ theorem map_equiv (f : α → β) (xs ys : List α) :
   have ⟨a, b⟩ := h
   apply And.intro <;> simp [List.subset_def] <;>
   intro p h <;>
-  apply Exists.intro p <;>
+  exists p <;>
   rw [List.subset_def] at a b <;>
   simp
   exact a h
@@ -181,7 +181,7 @@ theorem filterMap_equiv (f : α → Option β) (xs ys : List α) :
   intros h₁ h₂
   apply And.intro <;>
   intro b a h₃ h₄ <;>
-  apply Exists.intro a <;>
+  exists a <;>
   simp [h₄]
   exact h₁ h₃
   exact h₂ h₃
diff --git a/cedar-lean/Cedar/Data/Map.lean b/cedar-lean/Cedar/Data/Map.lean
index ad7cf37b4..00d8da138 100644
--- a/cedar-lean/Cedar/Data/Map.lean
+++ b/cedar-lean/Cedar/Data/Map.lean
@@ -104,12 +104,9 @@ instance : Membership α (Map α β) where
 theorem in_list_in_map {α : Type u} (k : α) (v : β) (m : Map α β) :
   (k, v) ∈ m.kvs → k ∈ m
 := by
-  intro h0
-  have h1 : k ∈ (List.map Prod.fst m.kvs) := by
-    simp
-    apply Exists.intro (k, v)
-    simp [h0]
-  apply h1
+  intro h₀
+  have h₁ : k ∈ (List.map Prod.fst m.kvs) := by simp ; exists (k, v)
+  apply h₁
 
 theorem contains_iff_some_find? {α β} [BEq α] {m : Map α β} {k : α} :
   m.contains k ↔ ∃ v, m.find? k = .some v
diff --git a/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean b/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean
index 69331d472..68bcf7d17 100644
--- a/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean
+++ b/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean
@@ -53,7 +53,7 @@ theorem if_satisfied_then_satisfiedPolicies_non_empty (effect : Effect) (policie
   rw [←Set.make_non_empty]
   apply @List.ne_nil_of_mem _ policy.id
   rw [List.mem_filterMap]
-  apply Exists.intro policy
+  exists policy
   unfold satisfiedWithEffect
   simp [h₀]
 
@@ -71,7 +71,7 @@ theorem if_satisfiedPolicies_non_empty_then_satisfied (effect : Effect) (policie
   rw [List.mem_filterMap] at h₁
   replace ⟨policy, h₁, h₂⟩ := h₁
   unfold satisfiedWithEffect at h₂
-  apply Exists.intro policy
+  exists policy
   simp [h₁]
   cases h₃ : (policy.effect == effect) <;> simp at h₃
   case false => simp [h₃] at h₂
@@ -111,7 +111,7 @@ theorem sound_policy_slice_is_equisatisfied (effect : Effect) (request : Request
   simp [List.subset_def]
   apply And.intro <;>
   intros pid policy h₃ h₄ <;>
-  apply Exists.intro policy <;>
+  exists policy <;>
   simp [h₄]
   case left =>
     simp [List.subset_def] at h₁
@@ -168,7 +168,7 @@ theorem alternate_errorPolicies_equiv_errorPolicies {policies : Policies} {reque
   apply And.intro
   case left =>
     intro pid p h₁ h₂
-    apply Exists.intro p
+    exists p
     unfold errored hasError at h₂
     split at h₂
     case inl h₃ =>
@@ -179,7 +179,7 @@ theorem alternate_errorPolicies_equiv_errorPolicies {policies : Policies} {reque
     case inr => contradiction
   case right =>
     intro p h₁
-    apply Exists.intro p
+    exists p
     simp [List.mem_filter] at h₁
     apply And.intro
     case left => exact h₁.left