refactor(data/pequiv): simpler proof of pequiv.of_set_univ (#5907)

17X smaller proof co-authors: `lean-gptf`, Stanislas Polu
leanprover-community · Jan 27, 2021 · e9a1e2b · e9a1e2b
1 parent fd55e57
commit e9a1e2b
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/data/pequiv.lean b/src/data/pequiv.lean
@@ -139,8 +139,7 @@ by dsimp [of_set]; split_ifs; split; finish
 
 @[simp] lemma of_set_symm : (of_set s).symm = of_set s := rfl
 
-@[simp] lemma of_set_univ : of_set set.univ = pequiv.refl α :=
-by ext; dsimp [of_set]; simp [eq_comm]
+@[simp] lemma of_set_univ : of_set set.univ = pequiv.refl α := rfl
 
 @[simp] lemma of_set_eq_refl {s : set α} [decidable_pred s] :
   of_set s = pequiv.refl α ↔ s = set.univ :=