refactor(library/data/list): reduce reliance on definitional equality

library/data/list/comb.lean

@@ -332,10 +332,10 @@ theorem mem_product {a : A} {b : B} : ∀ {l₁ l₂}, a ∈ l₁ → b ∈ l₂
   or.elim (eq_or_mem_of_mem_cons h₁)
     (λ aeqx  : a = x,
       assert aux : (a, b) ∈ map (λ b, (a, b)) l₂, from mem_map _ h₂,
-      by rewrite [-aeqx]; exact (mem_append_left _ aux))
+      begin rewrite [-aeqx, product_cons], exact mem_append_left _ aux end)
     (λ ainl₁ : a ∈ l₁,
-      have inl₁l₂ : (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂,
-      mem_append_right _ inl₁l₂)
+      assert inl₁l₂ : (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂,
+      begin rewrite [product_cons], exact mem_append_right _ inl₁l₂ end)
 
 theorem mem_of_mem_product_left {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → a ∈ l₁
 | []      l₂ h := absurd h !not_mem_nil

library/data/list/perm.lean

@@ -731,7 +731,7 @@ section product
 theorem perm_product_left {l₁ l₂ : list A} (t₁ : list B) : l₁ ~ l₂ → (product l₁ t₁) ~ (product l₂ t₁) :=
 assume p : l₁ ~ l₂, perm.induction_on p
   !perm.refl
-  (λ x l₁ l₂ p r, perm_app !perm.refl r)
+  (λ x l₁ l₂ p r, perm_app (perm.refl (map _ t₁)) r)
   (λ x y l,
     let m₁ := map (λ b, (x, b)) t₁ in
     let m₂ := map (λ b, (y, b)) t₁ in