From e4d4db45e9516e7a0fbb7068cd07198cdcaad2be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Mar 2021 14:51:18 -0700 Subject: [PATCH] feat: add missing `simp` lemmas for `->` --- src/Init/SimpLemmas.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 57651d34c9..9a239a0ed4 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -86,5 +86,8 @@ namespace Lean.Simp @[simp] theorem Or_False (p : Prop) : (p ∨ False) = p := propext <| Iff.intro (fun | Or.inl h => h | Or.inr h => False.elim h) (fun h => Or.inl h) @[simp] theorem False_Or (p : Prop) : (False ∨ p) = p := propext <| Iff.intro (fun | Or.inr h => h | Or.inl h => False.elim h) (fun h => Or.inr h) @[simp] theorem Iff_self (p : Prop) : (p ↔ p) = True := propext <| Iff.intro (fun h => trivial) (fun _ => Iff.intro id id) +@[simp] theorem False_arrow (p : Prop) : (False → p) = True := propext <| Iff.intro (fun _ => trivial) (by intros; trivial) +@[simp] theorem arrow_True (p : Prop) : (p → True) = True := propext <| Iff.intro (fun _ => trivial) (by intros; trivial) +@[simp] theorem True_arrow (p : Prop) : (True → p) = p := propext <| Iff.intro (fun h => h trivial) (by intros; trivial) end Lean.Simp