From 564e8f947dd99a1155cf9b47f4c7fe1b3b337f10 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Nov 2015 14:10:02 -0800 Subject: [PATCH] refactor(library): cleanup --- library/algebra/group.lean | 2 +- library/init/logic.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 4beec3903..7369f4cb6 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -297,7 +297,7 @@ section group lemma is_conj.symm (a b : A) : a ~ b → b ~ a := assume Pab, obtain x (Pconj : x ∘c b = a), from Pab, - assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, from (congr_arg2 conj_by (eq.refl x⁻¹) Pconj), + assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, begin congruence, assumption end, exists.intro x⁻¹ (eq.symm (conj_inv_cancel x b ▸ Pxinv)) lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c := diff --git a/library/init/logic.lean b/library/init/logic.lean index 62db17ed2..ff2a93fae 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -347,7 +347,7 @@ iff_true_intro not_false theorem not_congr [congr] (H : a ↔ b) : ¬a ↔ ¬b := iff.intro (λ H₁ H₂, H₁ (iff.mpr H H₂)) (λ H₁ H₂, H₁ (iff.mp H H₂)) -theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false := +theorem ne_self_iff_false [simp] {A : Type} (a : A) : (not (a = a)) ↔ false := iff.intro false_of_ne false.elim theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true :=