diff --git a/src/algebra/free_algebra.lean b/src/algebra/free_algebra.lean
index 0dd0cb1a592c4..636e5dbd452f4 100644
--- a/src/algebra/free_algebra.lean
+++ b/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.
diff --git a/src/algebra/ring_quot.lean b/src/algebra/ring_quot.lean
index 3c0b59d055a7e..231de20a65f7a 100644
--- a/src/algebra/ring_quot.lean
+++ b/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
diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index fb9fe1b2ed7eb..28701b84de5a0 100644
--- a/src/data/polynomial/eval.lean
+++ b/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₂
 
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index b670bd9a2e843..a10bd7d34f0f1 100644
--- a/src/linear_algebra/determinant.lean
+++ b/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) :
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index b3710244f1164..7fcadfd6b57f5 100644
--- a/src/linear_algebra/dimension.lean
+++ b/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''
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
index 22068faa614a8..f4acf825b69fe 100644
--- a/src/linear_algebra/finsupp.lean
+++ b/src/linear_algebra/finsupp.lean
@@ -953,14 +953,16 @@ variables (R)
 Pick some representation of `x : span R w` as a linear combination in `w`,
 using the axiom of choice.
 -/
-def span.repr (w : set M) (x : span R w) : w →₀ R :=
+@[irreducible] def span.repr (w : set M) (x : span R w) : w →₀ R :=
 ((finsupp.mem_span_iff_total _ _ _).mp x.2).some
 
 @[simp] lemma span.finsupp_total_repr {w : set M} (x : span R w) :
   finsupp.total w M R coe (span.repr R w x) = x :=
-((finsupp.mem_span_iff_total _ _ _).mp x.2).some_spec
+begin
+  rw span.repr,
+  exact ((finsupp.mem_span_iff_total _ _ _).mp x.2).some_spec
+end
 
-attribute [irreducible] span.repr
 
 end
 
diff --git a/src/linear_algebra/tensor_algebra/basic.lean b/src/linear_algebra/tensor_algebra/basic.lean
index 7ba9ed22644cd..2fe7d35868349 100644
--- a/src/linear_algebra/tensor_algebra/basic.lean
+++ b/src/linear_algebra/tensor_algebra/basic.lean
@@ -70,47 +70,56 @@ variables {M}
 /--
 The canonical linear map `M →ₗ[R] tensor_algebra R M`.
 -/
-def ι : M →ₗ[R] (tensor_algebra R M) :=
+@[irreducible] def ι : M →ₗ[R] (tensor_algebra R M) :=
 { to_fun := λ m, (ring_quot.mk_alg_hom R _ (free_algebra.ι R m)),
   map_add' := λ x y, by { rw [←alg_hom.map_add], exact ring_quot.mk_alg_hom_rel R rel.add, },
   map_smul' := λ r x, by { rw [←alg_hom.map_smul], exact ring_quot.mk_alg_hom_rel R rel.smul, } }
 
 lemma ring_quot_mk_alg_hom_free_algebra_ι_eq_ι (m : M) :
-  ring_quot.mk_alg_hom R (rel R M) (free_algebra.ι R m) = ι R m := rfl
+  ring_quot.mk_alg_hom R (rel R M) (free_algebra.ι R m) = ι R m :=
+by { rw [ι], refl }
 
 /--
 Given a linear map `f : M → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
 of `f` to a morphism of `R`-algebras `tensor_algebra R M → A`.
 -/
-@[simps symm_apply]
+@[irreducible, simps symm_apply]
 def lift {A : Type*} [semiring A] [algebra R A] : (M →ₗ[R] A) ≃ (tensor_algebra R M →ₐ[R] A) :=
 { to_fun := ring_quot.lift_alg_hom R ∘ λ f,
-    ⟨free_algebra.lift R ⇑f, λ x y (h : rel R M x y), by induction h; simp [algebra.smul_def]⟩,
+    ⟨free_algebra.lift R ⇑f, λ x y (h : rel R M x y), by induction h;
+        simp only [algebra.smul_def, free_algebra.lift_ι_apply, linear_map.map_smulₛₗ,
+          ring_hom.id_apply, map_mul, alg_hom.commutes, map_add]⟩,
   inv_fun := λ F, F.to_linear_map.comp (ι R),
-  left_inv := λ f, linear_map.ext $ λ x,
-    (ring_quot.lift_alg_hom_mk_alg_hom_apply _ _ _ _).trans (free_algebra.lift_ι_apply f x),
-  right_inv := λ F, ring_quot.ring_quot_ext' _ _ _ $ free_algebra.hom_ext $ funext $ λ x,
-    (ring_quot.lift_alg_hom_mk_alg_hom_apply _ _ _ _).trans (free_algebra.lift_ι_apply _ _) }
+  left_inv := λ f, begin
+    rw [ι],
+    ext1 x,
+    exact (ring_quot.lift_alg_hom_mk_alg_hom_apply _ _ _ _).trans (free_algebra.lift_ι_apply f x),
+  end,
+  right_inv := λ F, ring_quot.ring_quot_ext' _ _ _ $ free_algebra.hom_ext $ funext $ λ x, begin
+    rw [ι],
+    exact (ring_quot.lift_alg_hom_mk_alg_hom_apply _ _ _ _).trans (free_algebra.lift_ι_apply _ _)
+  end }
 
 variables {R}
 
 @[simp]
 theorem ι_comp_lift {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) :
-  (lift R f).to_linear_map.comp (ι R) = f := (lift R).symm_apply_apply f
+  (lift R f).to_linear_map.comp (ι R) = f :=
+by { convert (lift R).symm_apply_apply f, simp only [lift, equiv.coe_fn_symm_mk] }
 
 @[simp]
 theorem lift_ι_apply {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A) (x) :
-  lift R f (ι R x) = f x := by { dsimp [lift, ι], refl, }
+  lift R f (ι R x) = f x :=
+by { conv_rhs { rw ← ι_comp_lift f}, refl }
 
 @[simp]
 theorem lift_unique {A : Type*} [semiring A] [algebra R A] (f : M →ₗ[R] A)
   (g : tensor_algebra R M →ₐ[R] A) : g.to_linear_map.comp (ι R) = f ↔ g = lift R f :=
-(lift R).symm_apply_eq
+by { rw ← (lift R).symm_apply_eq, simp only [lift, equiv.coe_fn_symm_mk] }
 
 -- Marking `tensor_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.
-attribute [irreducible] ι lift
 
 @[simp]
 theorem lift_comp_ι {A : Type*} [semiring A] [algebra R A] (g : tensor_algebra R M →ₐ[R] A) :
diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean
index a21333f01c18a..5c57984864bb2 100644
--- a/src/measure_theory/integral/bochner.lean
+++ b/src/measure_theory/integral/bochner.lean
@@ -608,34 +608,54 @@ variables {𝕜}
 def integral_clm : (α →₁[μ] E) →L[ℝ] E := integral_clm' ℝ
 
 /-- The Bochner integral in L1 space -/
-def integral (f : α →₁[μ] E) : E := integral_clm f
+@[irreducible] def integral (f : α →₁[μ] E) : E := integral_clm f
 
-lemma integral_eq (f : α →₁[μ] E) : integral f = integral_clm f := rfl
+lemma integral_eq (f : α →₁[μ] E) : integral f = integral_clm f :=
+by simp only [integral]
 
 lemma integral_eq_set_to_L1 (f : α →₁[μ] E) :
   integral f = set_to_L1 (dominated_fin_meas_additive_weighted_smul μ) f :=
-rfl
+by { simp only [integral], refl }
 
 @[norm_cast] lemma simple_func.integral_L1_eq_integral (f : α →₁ₛ[μ] E) :
   integral (f : α →₁[μ] E) = (simple_func.integral f) :=
-set_to_L1_eq_set_to_L1s_clm (dominated_fin_meas_additive_weighted_smul μ) f
+begin
+  simp only [integral],
+  exact set_to_L1_eq_set_to_L1s_clm (dominated_fin_meas_additive_weighted_smul μ) f
+end
 
 variables (α E)
 @[simp] lemma integral_zero : integral (0 : α →₁[μ] E) = 0 :=
-map_zero integral_clm
+begin
+  simp only [integral],
+  exact map_zero integral_clm
+end
+
 variables {α E}
 
 lemma integral_add (f g : α →₁[μ] E) : integral (f + g) = integral f + integral g :=
-map_add integral_clm f g
+begin
+  simp only [integral],
+  exact map_add integral_clm f g
+end
 
 lemma integral_neg (f : α →₁[μ] E) : integral (-f) = - integral f :=
-map_neg integral_clm f
+begin
+  simp only [integral],
+  exact map_neg integral_clm f
+end
 
 lemma integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - integral g :=
-map_sub integral_clm f g
+begin
+  simp only [integral],
+  exact map_sub integral_clm f g
+end
 
 lemma integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f :=
-show (integral_clm' 𝕜) (c • f) = c • (integral_clm' 𝕜) f, from map_smul (integral_clm' 𝕜) c f
+begin
+  simp only [integral],
+  show (integral_clm' 𝕜) (c • f) = c • (integral_clm' 𝕜) f, from map_smul (integral_clm' 𝕜) c f
+end
 
 local notation (name := integral_clm) `Integral` := @integral_clm α E _ _ μ _ _
 local notation (name := simple_func.integral_clm') `sIntegral` :=
@@ -645,14 +665,17 @@ lemma norm_Integral_le_one : ‖Integral‖ ≤ 1 :=
 norm_set_to_L1_le (dominated_fin_meas_additive_weighted_smul μ) zero_le_one
 
 lemma norm_integral_le (f : α →₁[μ] E) : ‖integral f‖ ≤ ‖f‖ :=
-calc ‖integral f‖ = ‖Integral f‖ : rfl
+calc ‖integral f‖ = ‖Integral f‖ : by simp only [integral]
   ... ≤ ‖Integral‖ * ‖f‖ : le_op_norm _ _
   ... ≤ 1 * ‖f‖ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _
   ... = ‖f‖ : one_mul _
 
 @[continuity]
 lemma continuous_integral : continuous (λ (f : α →₁[μ] E), integral f) :=
-L1.integral_clm.continuous
+begin
+  simp only [integral],
+  exact L1.integral_clm.continuous
+end
 
 section pos_part
 
@@ -663,7 +686,8 @@ begin
   refine @is_closed_property _ _ _ (coe : (α →₁ₛ[μ] ℝ) → (α →₁[μ] ℝ))
     (λ f : α →₁[μ] ℝ, integral f = ‖Lp.pos_part f‖ - ‖Lp.neg_part f‖)
     (simple_func.dense_range one_ne_top) (is_closed_eq _ _) _ f,
-  { exact cont _ },
+  { simp only [integral],
+    exact cont _ },
   { refine continuous.sub (continuous_norm.comp Lp.continuous_pos_part)
       (continuous_norm.comp Lp.continuous_neg_part) },
   -- Show that the property holds for all simple functions in the `L¹` space.
@@ -694,7 +718,7 @@ section
 open_locale classical
 
 /-- The Bochner integral -/
-def integral {m : measurable_space α} (μ : measure α) (f : α → E) : E :=
+@[irreducible] def integral {m : measurable_space α} (μ : measure α) (f : α → E) : E :=
 if hf : integrable f μ then L1.integral (hf.to_L1 f) else 0
 
 end
@@ -715,17 +739,20 @@ variables {f g : α → E} {m : measurable_space α} {μ : measure α}
 
 lemma integral_eq (f : α → E) (hf : integrable f μ) :
   ∫ a, f a ∂μ = L1.integral (hf.to_L1 f) :=
-@dif_pos _ (id _) hf _ _ _
+by { rw [integral], exact @dif_pos _ (id _) hf _ _ _ }
 
 lemma integral_eq_set_to_fun (f : α → E) :
   ∫ a, f a ∂μ = set_to_fun μ (weighted_smul μ) (dominated_fin_meas_additive_weighted_smul μ) f :=
-rfl
+by { simp only [integral, L1.integral], refl }
 
 lemma L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a ∂μ :=
-(L1.set_to_fun_eq_set_to_L1 (dominated_fin_meas_additive_weighted_smul μ) f).symm
+begin
+  simp only [integral, L1.integral],
+  exact (L1.set_to_fun_eq_set_to_L1 (dominated_fin_meas_additive_weighted_smul μ) f).symm
+end
 
 lemma integral_undef (h : ¬ integrable f μ) : ∫ a, f a ∂μ = 0 :=
-@dif_neg _ (id _) h _ _ _
+by { rw [integral], exact @dif_neg _ (id _) h _ _ _ }
 
 lemma integral_non_ae_strongly_measurable (h : ¬ ae_strongly_measurable f μ) : ∫ a, f a ∂μ = 0 :=
 integral_undef $ not_and_of_not_left _ h
@@ -733,7 +760,10 @@ integral_undef $ not_and_of_not_left _ h
 variables (α E)
 
 lemma integral_zero : ∫ a : α, (0:E) ∂μ = 0 :=
-set_to_fun_zero (dominated_fin_meas_additive_weighted_smul μ)
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_zero (dominated_fin_meas_additive_weighted_smul μ)
+end
 
 @[simp] lemma integral_zero' : integral μ (0 : α → E) = 0 :=
 integral_zero α E
@@ -742,7 +772,10 @@ variables {α E}
 
 lemma integral_add (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
-set_to_fun_add (dominated_fin_meas_additive_weighted_smul μ) hf hg
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_add (dominated_fin_meas_additive_weighted_smul μ) hf hg
+end
 
 lemma integral_add' (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, (f + g) a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
@@ -750,17 +783,26 @@ integral_add hf hg
 
 lemma integral_finset_sum {ι} (s : finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, integrable (f i) μ) :
   ∫ a, ∑ i in s, f i a ∂μ = ∑ i in s, ∫ a, f i a ∂μ :=
-set_to_fun_finset_sum (dominated_fin_meas_additive_weighted_smul _) s hf
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_finset_sum (dominated_fin_meas_additive_weighted_smul _) s hf
+end
 
 lemma integral_neg (f : α → E) : ∫ a, -f a ∂μ = - ∫ a, f a ∂μ :=
-set_to_fun_neg (dominated_fin_meas_additive_weighted_smul μ) f
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_neg (dominated_fin_meas_additive_weighted_smul μ) f
+end
 
 lemma integral_neg' (f : α → E) : ∫ a, (-f) a ∂μ = - ∫ a, f a ∂μ :=
 integral_neg f
 
 lemma integral_sub (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ :=
-set_to_fun_sub (dominated_fin_meas_additive_weighted_smul μ) hf hg
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_sub (dominated_fin_meas_additive_weighted_smul μ) hf hg
+end
 
 lemma integral_sub' (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, (f - g) a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ :=
@@ -768,7 +810,10 @@ integral_sub hf hg
 
 lemma integral_smul (c : 𝕜) (f : α → E) :
   ∫ a, c • (f a) ∂μ = c • ∫ a, f a ∂μ :=
-set_to_fun_smul (dominated_fin_meas_additive_weighted_smul μ) weighted_smul_smul c f
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_smul (dominated_fin_meas_additive_weighted_smul μ) weighted_smul_smul c f
+end
 
 lemma integral_mul_left {L : Type*} [is_R_or_C L] (r : L) (f : α → L) :
   ∫ a, r * (f a) ∂μ = r * ∫ a, f a ∂μ :=
@@ -783,15 +828,24 @@ lemma integral_div {L : Type*} [is_R_or_C L] (r : L) (f : α → L) :
 by simpa only [←div_eq_mul_inv] using integral_mul_right r⁻¹ f
 
 lemma integral_congr_ae (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ :=
-set_to_fun_congr_ae (dominated_fin_meas_additive_weighted_smul μ) h
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_congr_ae (dominated_fin_meas_additive_weighted_smul μ) h
+end
 
 @[simp] lemma L1.integral_of_fun_eq_integral {f : α → E} (hf : integrable f μ) :
   ∫ a, (hf.to_L1 f) a ∂μ = ∫ a, f a ∂μ :=
-set_to_fun_to_L1 (dominated_fin_meas_additive_weighted_smul μ) hf
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_to_L1 (dominated_fin_meas_additive_weighted_smul μ) hf
+end
 
 @[continuity]
 lemma continuous_integral : continuous (λ (f : α →₁[μ] E), ∫ a, f a ∂μ) :=
-continuous_set_to_fun (dominated_fin_meas_additive_weighted_smul μ)
+begin
+  simp only [integral, L1.integral],
+  exact continuous_set_to_fun (dominated_fin_meas_additive_weighted_smul μ)
+end
 
 lemma norm_integral_le_lintegral_norm (f : α → E) :
   ‖∫ a, f a ∂μ‖ ≤ ennreal.to_real (∫⁻ a, (ennreal.of_real ‖f a‖) ∂μ) :=
@@ -836,7 +890,10 @@ lemma tendsto_integral_of_L1 {ι} (f : α → E) (hfi : integrable f μ)
   {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ i in l, integrable (F i) μ)
   (hF : tendsto (λ i, ∫⁻ x, ‖F i x - f x‖₊ ∂μ) l (𝓝 0)) :
   tendsto (λ i, ∫ x, F i x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) :=
-tendsto_set_to_fun_of_L1 (dominated_fin_meas_additive_weighted_smul μ) f hfi hFi hF
+begin
+  simp only [integral, L1.integral],
+  exact tendsto_set_to_fun_of_L1 (dominated_fin_meas_additive_weighted_smul μ) f hfi hFi hF
+end
 
 /-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
   everywhere convergence of a sequence of functions implies the convergence of their integrals.
@@ -849,8 +906,11 @@ theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → E} {f : α
   (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
   tendsto (λn, ∫ a, F n a ∂μ) at_top (𝓝 $ ∫ a, f a ∂μ) :=
-tendsto_set_to_fun_of_dominated_convergence (dominated_fin_meas_additive_weighted_smul μ) bound
-  F_measurable bound_integrable h_bound h_lim
+begin
+  simp only [integral, L1.integral],
+  exact tendsto_set_to_fun_of_dominated_convergence (dominated_fin_meas_additive_weighted_smul μ)
+    bound F_measurable bound_integrable h_bound h_lim
+end
 
 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
@@ -861,8 +921,11 @@ lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
   (bound_integrable : integrable bound μ)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) l (𝓝 (f a))) :
   tendsto (λn, ∫ a, F n a ∂μ) l (𝓝 $ ∫ a, f a ∂μ) :=
-tendsto_set_to_fun_filter_of_dominated_convergence (dominated_fin_meas_additive_weighted_smul μ)
-  bound hF_meas h_bound bound_integrable h_lim
+begin
+  simp only [integral, L1.integral],
+  exact tendsto_set_to_fun_filter_of_dominated_convergence
+    (dominated_fin_meas_additive_weighted_smul μ) bound hF_meas h_bound bound_integrable h_lim
+end
 
 /-- Lebesgue dominated convergence theorem for series. -/
 lemma has_sum_integral_of_dominated_convergence {ι} [countable ι]
@@ -902,16 +965,22 @@ lemma continuous_within_at_of_dominated {F : X → α → E} {x₀ : X} {bound :
   (bound_integrable : integrable bound μ)
   (h_cont : ∀ᵐ a ∂μ, continuous_within_at (λ x, F x a) s x₀) :
   continuous_within_at (λ x, ∫ a, F x a ∂μ) s x₀ :=
-continuous_within_at_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas
-  h_bound bound_integrable h_cont
+begin
+  simp only [integral, L1.integral],
+  exact continuous_within_at_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ)
+    hF_meas h_bound bound_integrable h_cont
+end
 
 lemma continuous_at_of_dominated {F : X → α → E} {x₀ : X} {bound : α → ℝ}
   (hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) μ)
   (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a)
   (bound_integrable : integrable bound μ) (h_cont : ∀ᵐ a ∂μ, continuous_at (λ x, F x a) x₀) :
   continuous_at (λ x, ∫ a, F x a ∂μ) x₀ :=
-continuous_at_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas h_bound
-  bound_integrable h_cont
+begin
+  simp only [integral, L1.integral],
+  exact continuous_at_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas
+    h_bound bound_integrable h_cont
+end
 
 lemma continuous_on_of_dominated {F : X → α → E} {bound : α → ℝ} {s : set X}
   (hF_meas : ∀ x ∈ s, ae_strongly_measurable (F x) μ)
@@ -919,15 +988,21 @@ lemma continuous_on_of_dominated {F : X → α → E} {bound : α → ℝ} {s :
   (bound_integrable : integrable bound μ)
   (h_cont : ∀ᵐ a ∂μ, continuous_on (λ x, F x a) s) :
   continuous_on (λ x, ∫ a, F x a ∂μ) s :=
-continuous_on_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas
-  h_bound bound_integrable h_cont
+begin
+  simp only [integral, L1.integral],
+  exact continuous_on_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas
+    h_bound bound_integrable h_cont
+end
 
 lemma continuous_of_dominated {F : X → α → E} {bound : α → ℝ}
   (hF_meas : ∀ x, ae_strongly_measurable (F x) μ) (h_bound : ∀ x, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a)
   (bound_integrable : integrable bound μ) (h_cont : ∀ᵐ a ∂μ, continuous (λ x, F x a)) :
   continuous (λ x, ∫ a, F x a ∂μ) :=
-continuous_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas h_bound
-  bound_integrable h_cont
+begin
+  simp only [integral, L1.integral],
+  exact continuous_set_to_fun_of_dominated (dominated_fin_meas_additive_weighted_smul μ) hF_meas
+    h_bound bound_integrable h_cont
+end
 
 /-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
   integral of the positive part of `f` and the integral of the negative part of `f`.  -/
@@ -1014,8 +1089,11 @@ begin
 end
 
 lemma integral_nonneg_of_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ a, f a ∂μ :=
-set_to_fun_nonneg (dominated_fin_meas_additive_weighted_smul μ)
-  (λ s _ _, weighted_smul_nonneg s) hf
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_nonneg (dominated_fin_meas_additive_weighted_smul μ)
+    (λ s _ _, weighted_smul_nonneg s) hf
+end
 
 lemma lintegral_coe_eq_integral (f : α → ℝ≥0) (hfi : integrable (λ x, (f x : ℝ)) μ) :
   ∫⁻ a, f a ∂μ = ennreal.of_real ∫ a, f a ∂μ :=
@@ -1136,8 +1214,11 @@ end normed_add_comm_group
 
 lemma integral_mono_ae {f g : α → ℝ} (hf : integrable f μ) (hg : integrable g μ) (h : f ≤ᵐ[μ] g) :
   ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
-set_to_fun_mono (dominated_fin_meas_additive_weighted_smul μ) (λ s _ _, weighted_smul_nonneg s)
-  hf hg h
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_mono (dominated_fin_meas_additive_weighted_smul μ)
+    (λ s _ _, weighted_smul_nonneg s) hf hg h
+end
 
 @[mono] lemma integral_mono {f g : α → ℝ} (hf : integrable f μ) (hg : integrable g μ) (h : f ≤ g) :
   ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
@@ -1200,6 +1281,7 @@ by { rw [← f.integral_eq_integral hfi, simple_func.integral, ← simple_func.i
 begin
   cases (@le_top _ _ _ (μ univ)).lt_or_eq with hμ hμ,
   { haveI : is_finite_measure μ := ⟨hμ⟩,
+    simp only [integral, L1.integral],
     exact set_to_fun_const (dominated_fin_meas_additive_weighted_smul _) _, },
   { by_cases hc : c = 0,
     { simp [hc, integral_zero] },
@@ -1223,7 +1305,7 @@ lemma tendsto_integral_approx_on_of_measurable
   tendsto (λ n, (simple_func.approx_on f hfm s y₀ h₀ n).integral μ) at_top (𝓝 $ ∫ x, f x ∂μ) :=
 begin
   have hfi' := simple_func.integrable_approx_on hfm hfi h₀ h₀i,
-  simp only [simple_func.integral_eq_integral _ (hfi' _)],
+  simp only [simple_func.integral_eq_integral _ (hfi' _), integral, L1.integral],
   exact tendsto_set_to_fun_approx_on_of_measurable (dominated_fin_meas_additive_weighted_smul μ)
     hfi hfm hs h₀ h₀i,
 end
@@ -1264,7 +1346,10 @@ end
 
 @[simp] lemma integral_zero_measure {m : measurable_space α} (f : α → E) :
   ∫ x, f x ∂(0 : measure α) = 0 :=
-set_to_fun_measure_zero (dominated_fin_meas_additive_weighted_smul _) rfl
+begin
+  simp only [integral, L1.integral],
+  exact set_to_fun_measure_zero (dominated_fin_meas_additive_weighted_smul _) rfl
+end
 
 theorem integral_finset_sum_measure {ι} {m : measurable_space α} {f : α → E}
   {μ : ι → measure α} {s : finset ι} (hf : ∀ i ∈ s, integrable f (μ i)) :
@@ -1522,8 +1607,6 @@ mk_simp_attribute integral_simps "Simp set for integral rules."
 attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub
   L1.integral_smul L1.integral_neg
 
-attribute [irreducible] integral L1.integral
-
 section integral_trim
 
 variables {H β γ : Type*} [normed_add_comm_group H]
diff --git a/src/number_theory/padics/ring_homs.lean b/src/number_theory/padics/ring_homs.lean
index e8153eb6910c8..9961c7552ad74 100644
--- a/src/number_theory/padics/ring_homs.lean
+++ b/src/number_theory/padics/ring_homs.lean
@@ -290,7 +290,7 @@ end
 
 /-- `appr n x` gives a value `v : ℕ` such that `x` and `↑v : ℤ_p` are congruent mod `p^n`.
 See `appr_spec`. -/
-noncomputable def appr : ℤ_[p] → ℕ → ℕ
+@[irreducible] noncomputable def appr : ℤ_[p] → ℕ → ℕ
 | x 0     := 0
 | x (n+1) :=
 let y := x - appr x n in
@@ -382,8 +382,6 @@ begin
     exact (dvd_pow_self (p : ℤ_[p]) hc0.ne').mul_left _, },
 end
 
-attribute [irreducible] appr
-
 /-- A ring hom from `ℤ_[p]` to `zmod (p^n)`, with underlying function `padic_int.appr n`. -/
 def to_zmod_pow (n : ℕ) : ℤ_[p] →+* zmod (p ^ n) :=
 to_zmod_hom (p^n) (λ x, appr x n)
diff --git a/src/ring_theory/class_group.lean b/src/ring_theory/class_group.lean
index 5e913eba6f342..446a8b7cdbbb8 100644
--- a/src/ring_theory/class_group.lean
+++ b/src/ring_theory/class_group.lean
@@ -54,17 +54,15 @@ def to_principal_ideal : Kˣ →* (fractional_ideal R⁰ K)ˣ :=
     (by simp only [units.coe_mk, units.coe_mul, span_singleton_mul_span_singleton]),
   map_one' := ext (by simp only [span_singleton_one, units.coe_mk, units.coe_one]) }
 
-local attribute [semireducible] to_principal_ideal
-
 variables {R K}
 
 @[simp] lemma coe_to_principal_ideal (x : Kˣ) :
   (to_principal_ideal R K x : fractional_ideal R⁰ K) = span_singleton _ x :=
-rfl
+by { simp only [to_principal_ideal], refl }
 
 @[simp] lemma to_principal_ideal_eq_iff {I : (fractional_ideal R⁰ K)ˣ} {x : Kˣ} :
   to_principal_ideal R K x = I ↔ span_singleton R⁰ (x : K) = I :=
-units.ext_iff
+by { simp only [to_principal_ideal], exact units.ext_iff }
 
 lemma mem_principal_ideals_iff {I : (fractional_ideal R⁰ K)ˣ} :
   I ∈ (to_principal_ideal R K).range ↔ ∃ x : K, span_singleton R⁰ x = I :=
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
index c17ff5cdfe2bc..458ac481a7a8f 100644
--- a/src/ring_theory/fractional_ideal.lean
+++ b/src/ring_theory/fractional_ideal.lean
@@ -428,31 +428,47 @@ so by making definitions irreducible, we hope to avoid deep unfolds.
 def mul (I J : fractional_ideal S P) : fractional_ideal S P :=
 ⟨I * J, I.is_fractional.mul J.is_fractional⟩
 
-local attribute [semireducible] mul
+-- local attribute [semireducible] mul
 
 instance : has_mul (fractional_ideal S P) := ⟨λ I J, mul I J⟩
 
 @[simp] lemma mul_eq_mul (I J : fractional_ideal S P) : mul I J = I * J := rfl
 
+lemma mul_def (I J : fractional_ideal S P) : I * J = ⟨I * J, I.is_fractional.mul J.is_fractional⟩ :=
+by simp only [← mul_eq_mul, mul]
+
 @[simp, norm_cast]
-lemma coe_mul (I J : fractional_ideal S P) : (↑(I * J) : submodule R P) = I * J := rfl
+lemma coe_mul (I J : fractional_ideal S P) : (↑(I * J) : submodule R P) = I * J :=
+by { simp only [mul_def], refl }
 
 @[simp, norm_cast]
 lemma coe_ideal_mul (I J : ideal R) : (↑(I * J) : fractional_ideal S P) = I * J :=
-coe_to_submodule_injective $ coe_submodule_mul _ _ _
+begin
+  simp only [mul_def],
+  exact coe_to_submodule_injective (coe_submodule_mul _ _ _)
+end
 
 lemma mul_left_mono (I : fractional_ideal S P) : monotone ((*) I) :=
-λ J J' h, mul_le.mpr (λ x hx y hy, mul_mem_mul hx (h hy))
+begin
+  intros J J' h,
+  simp only [mul_def],
+  exact mul_le.mpr (λ x hx y hy, mul_mem_mul hx (h hy))
+end
 
 lemma mul_right_mono (I : fractional_ideal S P) : monotone (λ J, J * I) :=
-λ J J' h, mul_le.mpr (λ x hx y hy, mul_mem_mul (h hx) hy)
+begin
+  intros J J' h,
+  simp only [mul_def],
+  exact mul_le.mpr (λ x hx y hy, mul_mem_mul (h hx) hy)
+end
 
 lemma mul_mem_mul {I J : fractional_ideal S P} {i j : P} (hi : i ∈ I) (hj : j ∈ J) :
-  i * j ∈ I * J := submodule.mul_mem_mul hi hj
+  i * j ∈ I * J :=
+by { simp only [mul_def], exact submodule.mul_mem_mul hi hj }
 
 lemma mul_le {I J K : fractional_ideal S P} :
   I * J ≤ K ↔ (∀ (i ∈ I) (j ∈ J), i * j ∈ K) :=
-submodule.mul_le
+by { simp only [mul_def], exact submodule.mul_le }
 
 instance : has_pow (fractional_ideal S P) ℕ := ⟨λ I n, ⟨I^n, I.is_fractional.pow n⟩⟩
 
@@ -464,7 +480,10 @@ lemma coe_pow (I : fractional_ideal S P) (n : ℕ) : ↑(I ^ n) = (I ^ n : submo
   {C : P → Prop} {r : P} (hr : r ∈ I * J)
   (hm : ∀ (i ∈ I) (j ∈ J), C (i * j))
   (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
-submodule.mul_induction_on hr hm ha
+begin
+  simp only [mul_def] at hr,
+  exact submodule.mul_induction_on hr hm ha
+end
 
 instance : has_nat_cast (fractional_ideal S P) := ⟨nat.unary_cast⟩
 
@@ -606,7 +625,10 @@ map_coe_ideal g 0
 coe_to_submodule_injective (submodule.map_sup _ _ _)
 
 @[simp] lemma map_mul : (I * J).map g = I.map g * J.map g :=
-coe_to_submodule_injective (submodule.map_mul _ _ _)
+begin
+  simp only [mul_def],
+  exact coe_to_submodule_injective (submodule.map_mul _ _ _)
+end
 
 @[simp] lemma map_map_symm (g : P ≃ₐ[R] P') :
   (I.map (g : P →ₐ[R] P')).map (g.symm : P' →ₐ[R] P) = I :=
diff --git a/src/ring_theory/localization/fraction_ring.lean b/src/ring_theory/localization/fraction_ring.lean
index f9b263c6817a5..f726dc02c6f05 100644
--- a/src/ring_theory/localization/fraction_ring.lean
+++ b/src/ring_theory/localization/fraction_ring.lean
@@ -112,12 +112,10 @@ mk' K ↑(sec (non_zero_divisors A) z).2
    mem_non_zero_divisors_iff_ne_zero.2 $ λ h0, h $
     eq_zero_of_fst_eq_zero (sec_spec (non_zero_divisors A) z) h0⟩
 
-local attribute [semireducible] is_fraction_ring.inv
-
 protected lemma mul_inv_cancel (x : K) (hx : x ≠ 0) :
   x * is_fraction_ring.inv A x = 1 :=
-show x * dite _ _ _ = 1, begin
-  rw [dif_neg hx, ←is_unit.mul_left_inj
+begin
+  rw [is_fraction_ring.inv, dif_neg hx, ←is_unit.mul_left_inj
     (map_units K ⟨(sec _ x).1, mem_non_zero_divisors_iff_ne_zero.2 $
       λ h0, hx $ eq_zero_of_fst_eq_zero (sec_spec (non_zero_divisors A) x) h0⟩),
     one_mul, mul_assoc],
@@ -131,7 +129,11 @@ See note [reducible non-instances]. -/
 noncomputable def to_field : field K :=
 { inv := is_fraction_ring.inv A,
   mul_inv_cancel := is_fraction_ring.mul_inv_cancel A,
-  inv_zero := dif_pos rfl,
+  inv_zero := begin
+    change is_fraction_ring.inv A (0 : K) = 0,
+    rw [is_fraction_ring.inv],
+    exact dif_pos rfl
+  end,
   .. is_fraction_ring.is_domain A,
   .. show comm_ring K, by apply_instance }
 
diff --git a/src/ring_theory/polynomial_algebra.lean b/src/ring_theory/polynomial_algebra.lean
index f41aa6cf97f72..c77c47dce0826 100644
--- a/src/ring_theory/polynomial_algebra.lean
+++ b/src/ring_theory/polynomial_algebra.lean
@@ -55,8 +55,7 @@ linear_map.to_span_singleton A _ (aeval (polynomial.X : A[X])).to_linear_map
 lemma to_fun_bilinear_apply_eq_sum (a : A) (p : R[X]) :
   to_fun_bilinear R A a p = p.sum (λ n r, monomial n (a * algebra_map R A r)) :=
 begin
-  dsimp [to_fun_bilinear_apply_apply, aeval_def, eval₂_eq_sum, polynomial.sum],
-  rw finset.smul_sum,
+  simp only [to_fun_bilinear_apply_apply, aeval_def, eval₂_eq_sum, polynomial.sum, finset.smul_sum],
   congr' with i : 1,
   rw [← algebra.smul_def, ←C_mul', mul_smul_comm, C_mul_X_pow_eq_monomial, ←algebra.commutes,
       ← algebra.smul_def, smul_monomial],
diff --git a/src/ring_theory/power_basis.lean b/src/ring_theory/power_basis.lean
index e442b65f7bd2e..610f5a9153783 100644
--- a/src/ring_theory/power_basis.lean
+++ b/src/ring_theory/power_basis.lean
@@ -319,8 +319,6 @@ noncomputable def alg_hom.fintype (pb : power_basis A S) :
 by letI := classical.dec_eq B; exact
 fintype.of_equiv _ pb.lift_equiv'.symm
 
-local attribute [irreducible] power_basis.lift
-
 /-- `pb.equiv_of_root pb' h₁ h₂` is an equivalence of algebras with the same power basis,
 where "the same" means that `pb` is a root of `pb'`s minimal polynomial and vice versa.
 
diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean
index 949efba5a60ef..4467295b0d38c 100644
--- a/src/topology/algebra/polynomial.lean
+++ b/src/topology/algebra/polynomial.lean
@@ -46,7 +46,7 @@ variables {R S : Type*} [semiring R] [topological_space R] [topological_semiring
 protected lemma continuous_eval₂ [semiring S] (p : S[X]) (f : S →+* R) :
   continuous (λ x, p.eval₂ f x) :=
 begin
-  dsimp only [eval₂_eq_sum, finsupp.sum],
+  simp only [eval₂_eq_sum, finsupp.sum],
   exact continuous_finset_sum _ (λ c hc, continuous_const.mul (continuous_pow _))
 end
 
diff --git a/src/topology/omega_complete_partial_order.lean b/src/topology/omega_complete_partial_order.lean
index 4049204fba2aa..b85acf2d4ae6d 100644
--- a/src/topology/omega_complete_partial_order.lean
+++ b/src/topology/omega_complete_partial_order.lean
@@ -33,7 +33,6 @@ lemma is_ωSup_iff_is_lub {α : Type u} [preorder α] {c : chain α} {x : α} :
 by simp [is_ωSup, is_lub, is_least, upper_bounds, lower_bounds]
 
 variables (α : Type u) [omega_complete_partial_order α]
-local attribute [irreducible] set
 
 /-- The characteristic function of open sets is monotone and preserves
 the limits of chains. -/
@@ -41,8 +40,7 @@ def is_open (s : set α) : Prop :=
 continuous' (λ x, x ∈ s)
 
 theorem is_open_univ : is_open α univ :=
-⟨λ x y h hx, mem_univ _,
-  by { convert @complete_lattice.top_continuous α Prop _ _, exact rfl }⟩
+⟨λ x y h hx, mem_univ _, @complete_lattice.top_continuous α Prop _ _⟩
 
 theorem is_open.inter (s t : set α) : is_open α s → is_open α t → is_open α (s ∩ t) :=
 complete_lattice.inf_continuous'
@@ -55,8 +53,7 @@ begin
     simp only [Sup_apply, set_of_bijective.surjective.exists, exists_prop, mem_preimage,
       set_coe.exists, supr_Prop_eq, mem_set_of_eq, subtype.coe_mk, mem_sUnion] },
   { intros p hp,
-    convert hs (set_of p) (mem_preimage.1 hp),
-    simp only [mem_set_of_eq] },
+    exact hs (set_of p) (mem_preimage.1 hp) },
 end
 
 end Scott