From deb7e080f0d5e48de4477e1675fc5b743295ac14 Mon Sep 17 00:00:00 2001 From: FR Date: Sun, 29 Sep 2024 01:45:15 +0800 Subject: [PATCH] chore: use implicit arguments in iff lemmas (#957) Co-authored-by: F. G. Dorais --- Batteries/Logic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean index 03c82eb5ac..9d7d14a70d 100644 --- a/Batteries/Logic.lean +++ b/Batteries/Logic.lean @@ -79,25 +79,25 @@ 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') : + (x : motive a rfl) {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') : + (x : motive a rfl) {a' : α} (e : a = a') : HEq (@Eq.rec α a motive x a' e) x := by subst e; rfl @[simp] theorem eqRec_heq_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') {β : Sort _} (y : β) : + {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} : HEq (@Eq.rec α a motive x a' e) y ↔ HEq x y := by subst e; rfl @[simp] theorem heq_eqRec_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _} - (x : motive a (rfl : a = a)) {a' : α} (e : a = a') {β : Sort _} (y : β) : + {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} : HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x := by subst e; rfl