[Merged by Bors] - chore(*): remove after the fact attribute [irreducible] at several places

src/algebra/free_algebra.lean

@@ -179,9 +179,10 @@ variables {X}
 /--
 The canonical function `X → free_algebra R X`.
 -/
-def ι : X → free_algebra R X := λ m, quot.mk _ m
+@[irreducible] def ι : X → free_algebra R X := λ m, quot.mk _ m
 
-@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R m := rfl
+@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R m :=
+by rw [ι]
 
 variables {A : Type*} [semiring A] [algebra R A]
 
@@ -230,16 +231,17 @@ private def lift_aux (f : X → A) : (free_algebra R X →ₐ[R] A) :=
 Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
 of `f` to a morphism of `R`-algebras `free_algebra R X → A`.
 -/
-def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
+@[irreducible] def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
 { to_fun := lift_aux R,
   inv_fun := λ F, F ∘ (ι R),
-  left_inv := λ f, by {ext, refl},
+  left_inv := λ f, by {ext, rw [ι], refl},
   right_inv := λ F, by
   { ext x,
     rcases x,
     induction x,
     case pre.of :
     { change ((F : free_algebra R X → A) ∘ (ι R)) _ = _,
+      rw [ι],
       refl },
     case pre.of_scalar :
     { change algebra_map _ _ x = F (algebra_map _ _ x),
@@ -251,36 +253,35 @@ def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
     { change lift_aux R (F ∘ ι R) (quot.mk _ _ * quot.mk _ _) = F (quot.mk _ _ * quot.mk _ _),
       rw [alg_hom.map_mul, alg_hom.map_mul, ha, hb], }, }, }
 
-@[simp] lemma lift_aux_eq (f : X → A) : lift_aux R f = lift R f := rfl
+@[simp] lemma lift_aux_eq (f : X → A) : lift_aux R f = lift R f :=
+by { rw [lift], refl }
 
 @[simp]
-lemma lift_symm_apply (F : free_algebra R X →ₐ[R] A) : (lift R).symm F = F ∘ (ι R) := rfl
+lemma lift_symm_apply (F : free_algebra R X →ₐ[R] A) : (lift R).symm F = F ∘ (ι R) :=
+by { rw [lift], refl }
 
 variables {R X}
 
 @[simp]
 theorem ι_comp_lift (f : X → A) :
-  (lift R f : free_algebra R X → A) ∘ (ι R) = f := by {ext, refl}
+  (lift R f : free_algebra R X → A) ∘ (ι R) = f :=
+by { ext, rw [ι, lift], refl }
 
 @[simp]
 theorem lift_ι_apply (f : X → A) (x) :
-  lift R f (ι R x) = f x := rfl
+  lift R f (ι R x) = f x :=
+by { rw [ι, lift], refl }
 
 @[simp]
 theorem lift_unique (f : X → A) (g : free_algebra R X →ₐ[R] A) :
   (g : free_algebra R X → A) ∘ (ι R) = f ↔ g = lift R f :=
-(lift R).symm_apply_eq
+by { rw [← (lift R).symm_apply_eq, lift], refl }
 
 /-!
-At this stage we set the basic definitions as `@[irreducible]`, so from this point onwards one
+Since we have set the basic definitions as `@[irreducible]`, from this point onwards one
 should only use the universal properties of the free algebra, and consider the actual implementation
-as a quotient of an inductive type as completely hidden.
+as a quotient of an inductive type as completely hidden. -/
 
-Of course, one still has the option to locally make these definitions `semireducible` if so desired,
-and Lean is still willing in some circumstances to do unification based on the underlying
-definition.
--/
-attribute [irreducible] ι lift
 -- Marking `free_algebra` irreducible makes `ring` instances inaccessible on quotients.
 -- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212580241
 -- For now, we avoid this by not marking it irreducible.

src/algebra/ring_quot.lean

@@ -182,7 +182,7 @@ instance [algebra S R] (r : R → R → Prop) : algebra S (ring_quot r) :=
 /--
 The quotient map from a ring to its quotient, as a homomorphism of rings.
 -/
-def mk_ring_hom (r : R → R → Prop) : R →+* ring_quot r :=
+@[irreducible] def mk_ring_hom (r : R → R → Prop) : R →+* ring_quot r :=
 { to_fun := λ x, ⟨quot.mk _ x⟩,
   map_one'  := by simp [← one_quot],
   map_mul'  := by simp [mul_quot],
@@ -211,7 +211,7 @@ variables  {T : Type u₄} [semiring T]
 Any ring homomorphism `f : R →+* T` which respects a relation `r : R → R → Prop`
 factors uniquely through a morphism `ring_quot r →+* T`.
 -/
-def lift {r : R → R → Prop} :
+@[irreducible] def lift {r : R → R → Prop} :
   {f : R →+* T // ∀ ⦃x y⦄, r x y → f x = f y} ≃ (ring_quot r →+* T) :=
 { to_fun := λ f', let f := (f' : R →+* T) in
   { to_fun := λ x, quot.lift f
@@ -228,13 +228,13 @@ def lift {r : R → R → Prop} :
     map_one' := by simp [← one_quot, f.map_one],
     map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y] }, },
   inv_fun := λ F, ⟨F.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩,
-  left_inv := λ f, by { ext, simp, refl },
-  right_inv := λ F, by { ext, simp, refl } }
+  left_inv := λ f, by { ext, simp [mk_ring_hom] },
+  right_inv := λ F, by { ext, simp [mk_ring_hom] } }
 
 @[simp]
 lemma lift_mk_ring_hom_apply (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (x) :
   lift ⟨f, w⟩ (mk_ring_hom r x) = f x :=
-rfl
+by { simp_rw [lift, mk_ring_hom], refl }
 
 -- note this is essentially `lift.symm_apply_eq.mp h`
 lemma lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y)
@@ -243,7 +243,12 @@ by { ext, simp [h], }
 
 lemma eq_lift_comp_mk_ring_hom {r : R → R → Prop} (f : ring_quot r →+* T) :
   f = lift ⟨f.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩ :=
-(lift.apply_symm_apply f).symm
+begin
+  conv_lhs { rw ← lift.apply_symm_apply f },
+  rw lift,
+  refl,
+end
+
 
 section comm_ring
 /-!
@@ -261,7 +266,11 @@ lift
     λ x y h, ideal.quotient.eq.2 $ submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, sub_add_cancel x y⟩)⟩
 
 @[simp] lemma ring_quot_to_ideal_quotient_apply (r : B → B → Prop) (x : B) :
-  ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x := rfl
+  ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x :=
+begin
+  simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
+  refl
+end
 
 /-- The universal ring homomorphism from `B ⧸ ideal.of_rel r` to `ring_quot r`. -/
 def ideal_quotient_to_ring_quot (r : B → B → Prop) :
@@ -287,7 +296,20 @@ The ring equivalence between `ring_quot r` and `(ideal.of_rel r).quotient`
 def ring_quot_equiv_ideal_quotient (r : B → B → Prop) :
   ring_quot r ≃+* B ⧸ ideal.of_rel r :=
 ring_equiv.of_hom_inv (ring_quot_to_ideal_quotient r) (ideal_quotient_to_ring_quot r)
-  (by { ext, refl, }) (by { ext, refl, })
+  (begin
+    ext,
+    simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
+    dsimp,
+    rw [mk_ring_hom],
+    refl
+  end)
+  (begin
+    ext,
+    simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
+    dsimp,
+    rw [mk_ring_hom],
+    refl
+  end)
 
 end comm_ring
 
@@ -331,20 +353,20 @@ variables (S)
 /--
 The quotient map from an `S`-algebra to its quotient, as a homomorphism of `S`-algebras.
 -/
-def mk_alg_hom (s : A → A → Prop) : A →ₐ[S] ring_quot s :=
-{ commutes' := λ r, rfl,
+@[irreducible] def mk_alg_hom (s : A → A → Prop) : A →ₐ[S] ring_quot s :=
+{ commutes' := λ r, by { simp [mk_ring_hom], refl },
   ..mk_ring_hom s }
 
 @[simp]
 lemma mk_alg_hom_coe (s : A → A → Prop) : (mk_alg_hom S s : A →+* ring_quot s) = mk_ring_hom s :=
-rfl
+by { simp_rw [mk_alg_hom, mk_ring_hom], refl }
 
 lemma mk_alg_hom_rel {s : A → A → Prop} {x y : A} (w : s x y) :
   mk_alg_hom S s x = mk_alg_hom S s y :=
 by simp [mk_alg_hom, mk_ring_hom, quot.sound (rel.of w)]
 
 lemma mk_alg_hom_surjective (s : A → A → Prop) : function.surjective (mk_alg_hom S s) :=
-by { dsimp [mk_alg_hom], rintro ⟨⟨a⟩⟩, use a, refl, }
+by { dsimp [mk_alg_hom, mk_ring_hom], rintro ⟨⟨a⟩⟩, use a, refl, }
 
 variables {B : Type u₄} [semiring B] [algebra S B]
 
@@ -361,8 +383,8 @@ end
 Any `S`-algebra homomorphism `f : A →ₐ[S] B` which respects a relation `s : A → A → Prop`
 factors uniquely through a morphism `ring_quot s →ₐ[S]  B`.
 -/
-def lift_alg_hom {s : A → A → Prop} :
-  { f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
+@[irreducible] def lift_alg_hom {s : A → A → Prop} :
+  {f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
 { to_fun := λ f', let f := (f' : A →ₐ[S] B) in
   { to_fun := λ x, quot.lift f
     begin
@@ -379,14 +401,14 @@ def lift_alg_hom {s : A → A → Prop} :
     map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y], },
     commutes' := by { rintros x, simp [← one_quot, smul_quot, algebra.algebra_map_eq_smul_one] } },
   inv_fun := λ F, ⟨F.comp (mk_alg_hom S s), λ _ _ h, by { dsimp, erw mk_alg_hom_rel S h }⟩,
-  left_inv := λ f, by { ext, simp, refl },
-  right_inv := λ F, by { ext, simp, refl } }
+  left_inv := λ f, by { ext, simp [mk_alg_hom, mk_ring_hom] },
+  right_inv := λ F, by { ext, simp [mk_alg_hom, mk_ring_hom] } }
 
 @[simp]
 lemma lift_alg_hom_mk_alg_hom_apply (f : A →ₐ[S] B) {s : A → A → Prop}
   (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
   (lift_alg_hom S ⟨f, w⟩) ((mk_alg_hom S s) x) = f x :=
-rfl
+by { simp_rw [lift_alg_hom, mk_alg_hom, mk_ring_hom], refl, }
 
 -- note this is essentially `(lift_alg_hom S).symm_apply_eq.mp h`
 lemma lift_alg_hom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y)
@@ -395,10 +417,12 @@ by { ext, simp [h], }
 
 lemma eq_lift_alg_hom_comp_mk_alg_hom {s : A → A → Prop} (f : ring_quot s →ₐ[S] B) :
   f = lift_alg_hom S ⟨f.comp (mk_alg_hom S s), λ x y h, by { dsimp, erw mk_alg_hom_rel S h, }⟩ :=
-((lift_alg_hom S).apply_symm_apply f).symm
+begin
+  conv_lhs { rw ← ((lift_alg_hom S).apply_symm_apply f) },
+  rw lift_alg_hom,
+  refl,
+end
 
 end algebra
 
-attribute [irreducible] mk_ring_hom mk_alg_hom lift lift_alg_hom
-
 end ring_quot

src/data/polynomial/eval.lean

@@ -31,10 +31,11 @@ variables (f : R →+* S) (x : S)
 
 /-- Evaluate a polynomial `p` given a ring hom `f` from the scalar ring
   to the target and a value `x` for the variable in the target -/
-def eval₂ (p : R[X]) : S :=
+@[irreducible] def eval₂ (p : R[X]) : S :=
 p.sum (λ e a, f a * x ^ e)
 
-lemma eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum (λ e a, f a * x ^ e) := rfl
+lemma eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum (λ e a, f a * x ^ e) :=
+by rw eval₂
 
 lemma eval₂_congr {R S : Type*} [semiring R] [semiring S]
   {f g : R →+* S} {s t : S} {φ ψ : R[X]} :
@@ -66,7 +67,7 @@ begin
 end
 
 @[simp] lemma eval₂_add : (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x :=
-by { apply sum_add_index; simp [add_mul] }
+by { simp only [eval₂_eq_sum], apply sum_add_index; simp [add_mul] }
 
 @[simp] lemma eval₂_one : (1 : R[X]).eval₂ f x = 1 :=
 by rw [← C_1, eval₂_C, f.map_one]
@@ -256,7 +257,7 @@ variables {x : R}
 def eval : R → R[X] → R := eval₂ (ring_hom.id _)
 
 lemma eval_eq_sum : p.eval x = p.sum (λ e a, a * x ^ e) :=
-rfl
+by { rw [eval, eval₂_eq_sum], refl }
 
 lemma eval_eq_sum_range {p : R[X]} (x : R) :
   p.eval x = ∑ i in finset.range (p.nat_degree + 1), p.coeff i * x ^ i :=
@@ -382,8 +383,12 @@ lemma is_root.eq_zero (h : is_root p x) : eval x p = 0 := h
 
 lemma coeff_zero_eq_eval_zero (p : R[X]) : coeff p 0 = p.eval 0 :=
 calc coeff p 0 = coeff p 0 * 0 ^ 0 : by simp
-... = p.eval 0 : eq.symm $
-  finset.sum_eq_single _ (λ b _ hb, by simp [zero_pow (nat.pos_of_ne_zero hb)]) (by simp)
+... = p.eval 0 :
+  begin
+    symmetry,
+    rw [eval_eq_sum],
+    exact finset.sum_eq_single _ (λ b _ hb, by simp [zero_pow (nat.pos_of_ne_zero hb)]) (by simp)
+  end
 
 lemma zero_is_root_of_coeff_zero_eq_zero {p : R[X]} (hp : p.coeff 0 = 0) : is_root p 0 :=
 by rwa coeff_zero_eq_eval_zero at hp
@@ -401,7 +406,8 @@ section comp
 /-- The composition of polynomials as a polynomial. -/
 def comp (p q : R[X]) : R[X] := p.eval₂ C q
 
-lemma comp_eq_sum_left : p.comp q = p.sum (λ e a, C a * q ^ e) := rfl
+lemma comp_eq_sum_left : p.comp q = p.sum (λ e a, C a * q ^ e) :=
+by rw [comp, eval₂_eq_sum]
 
 @[simp] lemma comp_X : p.comp X = p :=
 begin
@@ -735,12 +741,10 @@ end
 end map
 
 /-!
-After having set up the basic theory of `eval₂`, `eval`, `comp`, and `map`,
-we make `eval₂` irreducible.
+we have made `eval₂` irreducible from the start.
 
-Perhaps we can make the others irreducible too?
+Perhaps we can make also `eval`, `comp`, and `map` irreducible too?
 -/
-attribute [irreducible] polynomial.eval₂
 
 section hom_eval₂
 

src/linear_algebra/clifford_algebra/basic.lean

@@ -73,14 +73,14 @@ namespace clifford_algebra
 /--
 The canonical linear map `M →ₗ[R] clifford_algebra Q`.
 -/
-def ι : M →ₗ[R] clifford_algebra Q :=
+@[irreducible] def ι : M →ₗ[R] clifford_algebra Q :=
 (ring_quot.mk_alg_hom R _).to_linear_map.comp (tensor_algebra.ι R)
 
 /-- As well as being linear, `ι Q` squares to the quadratic form -/
 @[simp]
 theorem ι_sq_scalar (m : M) : ι Q m * ι Q m = algebra_map R _ (Q m) :=
 begin
-  erw [←alg_hom.map_mul, ring_quot.mk_alg_hom_rel R (rel.of m), alg_hom.commutes],
+  erw [ι, ←alg_hom.map_mul, ring_quot.mk_alg_hom_rel R (rel.of m), alg_hom.commutes],
   refl,
 end
 
@@ -98,7 +98,7 @@ Given a linear map `f : M →ₗ[R] A` into an `R`-algebra `A`, which satisfies
 `cond : ∀ m : M, f m * f m = Q(m)`, this is the canonical lift of `f` to a morphism of `R`-algebras
 from `clifford_algebra Q` to `A`.
 -/
-@[simps symm_apply]
+@[irreducible, simps symm_apply]
 def lift :
   {f : M →ₗ[R] A // ∀ m, f m * f m = algebra_map _ _ (Q m)} ≃ (clifford_algebra Q →ₐ[R] A) :=
 { to_fun := λ f,
@@ -122,7 +122,8 @@ variables {Q}
 @[simp]
 theorem ι_comp_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebra_map _ _ (Q m)) :
   (lift Q ⟨f, cond⟩).to_linear_map.comp (ι Q) = f :=
-(subtype.mk_eq_mk.mp $ (lift Q).symm_apply_apply ⟨f, cond⟩)
+by simpa only [lift, equiv.coe_fn_mk, equiv.coe_fn_symm_mk]
+  using (lift Q).symm_apply_apply ⟨f, cond⟩
 
 @[simp]
 theorem lift_ι_apply (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebra_map _ _ (Q m)) (x) :
@@ -139,7 +140,9 @@ begin
   simp only,
 end
 
-attribute [irreducible] clifford_algebra ι lift
+-- Marking `clifford_algebra` irreducible makes `ring` instances inaccessible on quotients.
+-- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212580241
+-- For now, we avoid this by not marking it irreducible.
 
 @[simp]
 theorem lift_comp_ι (g : clifford_algebra Q →ₐ[R] A) :
@@ -348,7 +351,7 @@ variables {Q}
 /-- The canonical image of the `tensor_algebra` in the `clifford_algebra`, which maps
 `tensor_algebra.ι R x` to `clifford_algebra.ι Q x`. -/
 def to_clifford : tensor_algebra R M →ₐ[R] clifford_algebra Q :=
-tensor_algebra.lift R (clifford_algebra.ι Q)
+tensor_algebra.lift R (clifford_algebra.ι Q : _)
 
 @[simp] lemma to_clifford_ι (m : M) : (tensor_algebra.ι R m).to_clifford = clifford_algebra.ι Q m :=
 by simp [to_clifford]

src/linear_algebra/clifford_algebra/conjugation.lean

@@ -40,7 +40,10 @@ section involute
 
 /-- Grade involution, inverting the sign of each basis vector. -/
 def involute : clifford_algebra Q →ₐ[R] clifford_algebra Q :=
-clifford_algebra.lift Q ⟨-(ι Q), λ m, by simp⟩
+begin
+  refine clifford_algebra.lift Q _,
+  exact ⟨-(ι Q), λ m, by simp only [linear_map.neg_apply, mul_neg, neg_mul, ι_sq_scalar, neg_neg]⟩
+end
 
 @[simp] lemma involute_ι (m : M) : involute (ι Q m) = -ι Q m :=
 lift_ι_apply _ _ m

src/linear_algebra/clifford_algebra/equivs.lean

@@ -95,7 +95,7 @@ linear_map.ext reverse_apply
 
 @[simp] lemma involute_eq_id :
   (involute : clifford_algebra (0 : quadratic_form R unit) →ₐ[R] _) = alg_hom.id R _ :=
-by { ext, simp }
+by { ext1, simp }
 
 /-- The clifford algebra over a 0-dimensional vector space is isomorphic to its scalars. -/
 protected def equiv : clifford_algebra (0 : quadratic_form R unit) ≃ₐ[R] R :=