From fefddcd0f93263a42bfcdae9a5292a9a1986222c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Apr 2015 09:42:24 -0700 Subject: [PATCH] fix(library/data/list/perm): broken theorem --- library/data/list/perm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 62cde2b8d..e5a5e9ca7 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -591,7 +591,7 @@ include H theorem perm_union_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (union l₁ t₁) ~ (union l₂ t₁) := assume p, perm.induction_on p - (by rewrite [union_nil]; exact !refl) + (by rewrite [nil_union]; exact !refl) (λ x l₁ l₂ p₁ r₁, by_cases (λ xint₁ : x ∈ t₁, by rewrite [*union_cons_of_mem _ xint₁]; exact r₁) (λ nxint₁ : x ∉ t₁, by rewrite [*union_cons_of_not_mem _ nxint₁]; exact (skip _ r₁)))