chore: adaptations for leanprover/lean4#3756

negiizhao · Apr 24, 2024 · 3837547 · 3837547
1 parent 4a54f26
commit 3837547
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 6 deletions.
diff --git a/Std/Logic.lean b/Std/Logic.lean
@@ -94,11 +94,6 @@ theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
 theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
   ⟨heq_of_cast_eq _, fun h => by cases h; rfl⟩
 
-theorem eqRec_eq_cast {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
-    (x : motive a (rfl : a = a)) {a' : α} (e : a = a') :
-    @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by
-  subst e; rfl
-
 --Porting note: new theorem. More general version of `eqRec_heq`
 theorem eqRec_heq_self {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
     (x : motive a (rfl : a = a)) {a' : α} (e : a = a') :

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4-pr-releases:pr-release-3756