chore(*): remove after the fact attribute [irreducible] at several places (#18168)

Part of #18164

Author: sgouezel

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/determinant.lean

@@ -128,7 +128,7 @@ there is no good way to generalize over universe parameters, so we can't fully s
 type that it does not depend on the choice of basis. Instead you can use the `det_aux_def'` lemma,
 or avoid mentioning a basis at all using `linear_map.det`.
 -/
-def det_aux : trunc (basis ι A M) → (M →ₗ[A] M) →* A :=
+@[irreducible] def det_aux : trunc (basis ι A M) → (M →ₗ[A] M) →* A :=
 trunc.lift
   (λ b : basis ι A M,
     (det_monoid_hom).comp (to_matrix_alg_equiv b : (M →ₗ[A] M) →* matrix ι ι A))
@@ -140,10 +140,7 @@ See also `det_aux_def'` which allows you to vary the basis.
 -/
 lemma det_aux_def (b : basis ι A M) (f : M →ₗ[A] M) :
   linear_map.det_aux (trunc.mk b) f = matrix.det (linear_map.to_matrix b b f) :=
-rfl
-
--- Discourage the elaborator from unfolding `det_aux` and producing a huge term.
-attribute [irreducible] linear_map.det_aux
+by  { rw [det_aux], refl }
 
 lemma det_aux_def' {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (tb : trunc $ basis ι A M) (b' : basis ι' A M) (f : M →ₗ[A] M) :

src/linear_algebra/dimension.lean

@@ -105,7 +105,7 @@ In particular this agrees with the usual notion of the dimension of a vector spa
 The definition is marked as protected to avoid conflicts with `_root_.rank`,
 the rank of a linear map.
 -/
-protected def module.rank : cardinal :=
+@[irreducible] protected def module.rank : cardinal :=
 ⨆ ι : {s : set V // linear_independent K (coe : s → V)}, #ι.1
 
 end
@@ -136,6 +136,7 @@ theorem dim_le {n : ℕ}
   (H : ∀ s : finset M, linear_independent R (λ i : s, (i : M)) → s.card ≤ n) :
   module.rank R M ≤ n :=
 begin
+  rw module.rank,
   apply csupr_le',
   rintro ⟨s, li⟩,
   exact linear_independent_bounded_of_finset_linear_independent_bounded H _ li,
@@ -239,7 +240,7 @@ begin
   apply le_trans,
   { exact cardinal.lift_mk_le.mpr
       ⟨(equiv.of_injective _ hv.injective).to_embedding⟩, },
-  { simp only [cardinal.lift_le],
+  { simp only [cardinal.lift_le, module.rank],
     apply le_trans,
     swap,
     exact le_csupr (cardinal.bdd_above_range.{v v} _) ⟨range v, hv.coe_range⟩,
@@ -266,6 +267,7 @@ variables (R M)
 @[simp] lemma dim_punit : module.rank R punit = 0 :=
 begin
   apply le_bot_iff.mp,
+  rw module.rank,
   apply csupr_le',
   rintro ⟨s, li⟩,
   apply le_bot_iff.mpr,
@@ -775,6 +777,7 @@ theorem basis.mk_eq_dim'' {ι : Type v} (v : basis ι R M) :
   #ι = module.rank R M :=
 begin
   haveI := nontrivial_of_invariant_basis_number R,
+  rw module.rank,
   apply le_antisymm,
   { transitivity,
     swap,
@@ -786,10 +789,6 @@ begin
     apply linear_independent_le_basis v _ li, },
 end
 
--- By this stage we want to have a complete API for `module.rank`,
--- so we set it `irreducible` here, to keep ourselves honest.
-attribute [irreducible] module.rank
-
 theorem basis.mk_range_eq_dim (v : basis ι R M) :
   #(range v) = module.rank R M :=
 v.reindex_range.mk_eq_dim''