feat(tactic/lint): linter for @[class] def (#6061)

Also cleaning up some uses of `@[class] def` that were missed in #6028.


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

archive/100-theorems-list/83_friendship_graphs.lean

@@ -242,8 +242,8 @@ begin
   have p_dvd_d_pred := (zmod.nat_coe_zmod_eq_zero_iff_dvd _ _).mpr (d - 1).min_fac_dvd,
   have dpos : 0 < d := by linarith,
   have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast,
-  haveI : fact p.prime := nat.min_fac_prime (by linarith),
-  have hp2 : 2 ≤ p, { apply nat.prime.two_le, assumption },
+  haveI : fact p.prime := ⟨nat.min_fac_prime (by linarith)⟩,
+  have hp2 : 2 ≤ p := (fact.out p.prime).two_le,
   have dmod : (d : zmod p) = 1,
   { rw [← nat.succ_pred_eq_of_pos dpos, nat.succ_eq_add_one, nat.pred_eq_sub_one],
     simp only [add_left_eq_self, nat.cast_add, nat.cast_one],
@@ -253,8 +253,7 @@ begin
   have := zmod.trace_pow_card (G.adj_matrix (zmod p)),
   contrapose! this, clear this,
   -- the trace is 0 mod p when computed one way
-  rw [trace_adj_matrix, zero_pow],
-  swap, { apply nat.prime.pos, assumption, },
+  rw [trace_adj_matrix, zero_pow (fact.out p.prime).pos],
   -- but the trace is 1 mod p when computed the other way
   rw adj_matrix_pow_mod_p_of_regular hG dmod hd hp2,
   dunfold fintype.card at Vmod,

src/algebra/category/Algebra/basic.lean

@@ -145,5 +145,5 @@ instance Algebra.forget_reflects_isos : reflects_isomorphisms (forget (Algebra.{
     resetI,
     let i := as_iso ((forget (Algebra.{u} R)).map f),
     let e : X ≃ₐ[R] Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Algebra_iso,
+    exact ⟨(is_iso.of_iso e.to_Algebra_iso).1⟩,
   end }

src/algebra/category/CommRing/basic.lean

@@ -202,7 +202,7 @@ instance Ring.forget_reflects_isos : reflects_isomorphisms (forget Ring.{u}) :=
     resetI,
     let i := as_iso ((forget Ring).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Ring_iso,
+    exact ⟨(is_iso.of_iso e.to_Ring_iso).1⟩,
   end }
 
 instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.{u}) :=
@@ -211,7 +211,7 @@ instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.
     resetI,
     let i := as_iso ((forget CommRing).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_CommRing_iso,
+    exact ⟨(is_iso.of_iso e.to_CommRing_iso).1⟩,
   end }
 
 example : reflects_isomorphisms (forget₂ Ring AddCommGroup) := by apply_instance

src/algebra/category/Group/abelian.lean

@@ -39,7 +39,7 @@ end
 
 /-- The category of abelian groups is abelian. -/
 instance : abelian AddCommGroup :=
-{ has_finite_products := by { dsimp [has_finite_products], apply_instance },
+{ has_finite_products := ⟨by apply_instance⟩,
   normal_mono := λ X Y, normal_mono,
   normal_epi := λ X Y, normal_epi }
 

src/algebra/category/Group/basic.lean

@@ -250,7 +250,7 @@ instance Group.forget_reflects_isos : reflects_isomorphisms (forget Group.{u}) :
     resetI,
     let i := as_iso ((forget Group).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Group_iso,
+    exact ⟨(is_iso.of_iso e.to_Group_iso).1⟩,
   end }
 
 @[to_additive]
@@ -260,5 +260,5 @@ instance CommGroup.forget_reflects_isos : reflects_isomorphisms (forget CommGrou
     resetI,
     let i := as_iso ((forget CommGroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_CommGroup_iso,
+    exact ⟨(is_iso.of_iso e.to_CommGroup_iso).1⟩,
   end }

src/algebra/category/Module/abelian.lean

@@ -68,7 +68,7 @@ def normal_epi (hf : epi f) : normal_epi f :=
 
 /-- The category of R-modules is abelian. -/
 instance : abelian (Module R) :=
-{ has_finite_products := by { dsimp [has_finite_products], apply_instance },
+{ has_finite_products := ⟨by apply_instance⟩,
   has_kernels := by apply_instance,
   has_cokernels := has_cokernels_Module,
   normal_mono := λ X Y, normal_mono,

src/algebra/category/Mon/basic.lean

@@ -179,7 +179,7 @@ instance Mon.forget_reflects_isos : reflects_isomorphisms (forget Mon.{u}) :=
     resetI,
     let i := as_iso ((forget Mon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Mon_iso,
+    exact ⟨(is_iso.of_iso e.to_Mon_iso).1⟩,
   end }
 
 @[to_additive]
@@ -189,7 +189,7 @@ instance CommMon.forget_reflects_isos : reflects_isomorphisms (forget CommMon.{u
     resetI,
     let i := as_iso ((forget CommMon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_CommMon_iso,
+    exact ⟨(is_iso.of_iso e.to_CommMon_iso).1⟩,
   end }
 
 /-!

src/algebra/category/Semigroup/basic.lean

@@ -170,7 +170,7 @@ instance Magma.forget_reflects_isos : reflects_isomorphisms (forget Magma.{u}) :
     resetI,
     let i := as_iso ((forget Magma).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Magma_iso,
+    exact ⟨(is_iso.of_iso e.to_Magma_iso).1⟩,
   end }
 
 @[to_additive]
@@ -180,7 +180,7 @@ instance Semigroup.forget_reflects_isos : reflects_isomorphisms (forget Semigrou
     resetI,
     let i := as_iso ((forget Semigroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact is_iso.of_iso e.to_Semigroup_iso,
+    exact ⟨(is_iso.of_iso e.to_Semigroup_iso).1⟩,
   end }
 
 /-!

src/algebra/char_p/basic.lean

@@ -112,18 +112,18 @@ theorem dvd {x : ℕ} (hx : (x : R) = 0) : ring_char R ∣ x :=
 
 end ring_char
 
-theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : ℕ} [fact p.prime]
+theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : ℕ} [hp : fact p.prime]
   [char_p R p] (x y : R) (h : commute x y) :
   (x + y)^p = x^p + y^p :=
 begin
   rw [commute.add_pow h, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
   rw [nat.cast_one, mul_one, mul_one], congr' 1,
   convert finset.sum_eq_single 0 _ _, { simp },
-  swap, { intro h1, contrapose! h1, rw finset.mem_range, apply nat.prime.pos, assumption },
+  swap, { intro h1, contrapose! h1, rw finset.mem_range, exact hp.1.pos },
   intros b h1 h2,
   suffices : (p.choose b : R) = 0, { rw this, simp },
   rw char_p.cast_eq_zero_iff R p,
-  refine nat.prime.dvd_choose_self (pos_iff_ne_zero.mpr h2) _ (by assumption),
+  refine nat.prime.dvd_choose_self (pos_iff_ne_zero.mpr h2) _ hp.1,
   rwa ← finset.mem_range
 end
 
@@ -185,7 +185,7 @@ begin
   rw [show (2 : R) = (2 : ℕ), by norm_cast] at h,
   have := (char_p.cast_eq_zero_iff R p 2).mp h,
   have := nat.le_of_dvd dec_trivial this,
-  rw fact at *, linarith,
+  rw fact_iff at *, linarith,
 end
 
 lemma ring_hom.char_p_iff_char_p {K L : Type*} [field K] [field L] (f : K →+* L) (p : ℕ) :
@@ -201,14 +201,14 @@ section frobenius
 section comm_semiring
 
 variables (R : Type u) [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) (g : R →+* S)
-  (p : ℕ) [fact p.prime] [char_p R p]  [char_p S p] (x y : R)
+  (p : ℕ) [fact p.prime] [char_p R p] [char_p S p] (x y : R)
 
 /-- The frobenius map that sends x to x^p -/
 def frobenius : R →+* R :=
 { to_fun := λ x, x^p,
   map_one' := one_pow p,
   map_mul' := λ x y, mul_pow x y p,
-  map_zero' := zero_pow (lt_trans zero_lt_one ‹nat.prime p›.one_lt),
+  map_zero' := zero_pow (lt_trans zero_lt_one (fact.out (nat.prime p)).one_lt),
   map_add' := add_pow_char R }
 
 variable {R}
@@ -262,7 +262,7 @@ end comm_semiring
 section comm_ring
 
 variables (R : Type u) [comm_ring R] {S : Type v} [comm_ring S] (f : R →* S) (g : R →+* S)
-  (p : ℕ) [fact p.prime] [char_p R p]  [char_p S p] (x y : R)
+  (p : ℕ) [fact p.prime] [char_p R p] [char_p S p] (x y : R)
 
 theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x := (frobenius R p).map_neg x
 
@@ -342,7 +342,7 @@ match p, hc with
 end
 
 lemma char_is_prime_of_pos (p : ℕ) [h : fact (0 < p)] [char_p R p] : fact p.prime :=
-(char_p.char_is_prime_or_zero R _).resolve_right (pos_iff_ne_zero.1 h)
+⟨(char_p.char_is_prime_or_zero R _).resolve_right (pos_iff_ne_zero.1 h.1)⟩
 
 end nontrivial
 
@@ -416,7 +416,7 @@ begin
   obtain ⟨c, hc⟩ := char_p.exists R, resetI,
   have hcpn : c ∣ p ^ n,
   { rw [← char_p.cast_eq_zero_iff R c, ← hn, char_p.cast_card_eq_zero], },
-  obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i, by rwa nat.dvd_prime_pow hp at hcpn,
+  obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i, by rwa nat.dvd_prime_pow hp.1 at hcpn,
   obtain rfl : i = n,
   { apply hR i hi, rw [← nat.cast_pow, ← hc, char_p.cast_eq_zero] },
   rwa ← hc

src/algebra/char_p/invertible.lean

@@ -36,7 +36,7 @@ invertible_of_nonzero (λ h, not_dvd ((char_p.cast_eq_zero_iff K p t).mp h))
 
 instance invertible_of_pos [char_zero K] (n : ℕ) [h : fact (0 < n)] :
   invertible (n : K) :=
-invertible_of_nonzero $ by simpa [pos_iff_ne_zero] using h
+invertible_of_nonzero $ by simpa [pos_iff_ne_zero] using h.out
 
 end field
 

src/algebra/char_p/quotient.lean

@@ -20,7 +20,7 @@ theorem quotient (R : Type u) [comm_ring R] (p : ℕ) [hp1 : fact p.prime] (hp2
 have hp0 : (p : (ideal.span {p} : ideal R).quotient) = 0,
   from (ideal.quotient.mk (ideal.span {p} : ideal R)).map_nat_cast p ▸
     ideal.quotient.eq_zero_iff_mem.2 (ideal.subset_span $ set.mem_singleton _),
-ring_char.of_eq $ or.resolve_left ((nat.dvd_prime hp1).1 $ ring_char.dvd hp0) $ λ h1,
+ring_char.of_eq $ or.resolve_left ((nat.dvd_prime hp1.1).1 $ ring_char.dvd hp0) $ λ h1,
 hp2 $ is_unit_iff_dvd_one.2 $ ideal.mem_span_singleton.1 $ ideal.quotient.eq_zero_iff_mem.1 $
 @@subsingleton.elim (@@char_p.subsingleton _ $ ring_char.of_eq h1) _ _
 

src/algebra/homology/exact.lean

@@ -86,7 +86,7 @@ lemma exact_comp_mono [exact f g] [mono h] : exact f (g ≫ h) :=
 begin
   refine ⟨by simp, _⟩,
   letI : is_iso (kernel.lift (g ≫ h) (kernel.ι g) (by simp)) :=
-    ⟨kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]), by tidy⟩,
+    ⟨⟨kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]), by tidy⟩⟩,
   rw image_to_kernel_map_comp_right f g h exact.w,
   exact epi_comp _ _
 end
@@ -95,8 +95,8 @@ lemma exact_kernel : exact (kernel.ι f) f :=
 begin
   refine ⟨kernel.condition _, _⟩,
   letI : is_iso (image_to_kernel_map (kernel.ι f) f (kernel.condition f)) :=
-    ⟨factor_thru_image (kernel.ι f),
-      ⟨by simp [←cancel_mono (image.ι (kernel.ι f))], by tidy⟩⟩,
+    ⟨⟨factor_thru_image (kernel.ι f),
+      ⟨by simp [←cancel_mono (image.ι (kernel.ι f))], by tidy⟩⟩⟩,
   apply_instance
 end
 

src/analysis/calculus/darboux.lean

@@ -75,19 +75,19 @@ theorem convex_image_has_deriv_at {s : set ℝ} (hs : convex s)
   (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) :
   convex (f' '' s) :=
 begin
-  refine real.convex_iff_ord_connected.2 _,
+  refine real.convex_iff_ord_connected.2 ⟨_⟩,
   rintros _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩,
   cases eq_or_lt_of_le hma with hma hma,
     by exact hma ▸ mem_image_of_mem f' ha,
   cases eq_or_lt_of_le hmb with hmb hmb,
     by exact hmb.symm ▸ mem_image_of_mem f' hb,
   cases le_total a b with hab hab,
-  { have : Icc a b ⊆ s, from hs.ord_connected ha hb,
+  { have : Icc a b ⊆ s, from hs.ord_connected.out ha hb,
     rcases exists_has_deriv_within_at_eq_of_gt_of_lt hab
       (λ x hx, (hf x $ this hx).has_deriv_within_at) hma hmb
       with ⟨c, cmem, hc⟩,
     exact ⟨c, this cmem, hc⟩ },
-  { have : Icc b a ⊆ s, from hs.ord_connected hb ha,
+  { have : Icc b a ⊆ s, from hs.ord_connected.out hb ha,
     rcases exists_has_deriv_within_at_eq_of_lt_of_gt hab
       (λ x hx, (hf x $ this hx).has_deriv_within_at) hmb hma
       with ⟨c, cmem, hc⟩,
@@ -102,6 +102,6 @@ theorem deriv_forall_lt_or_forall_gt_of_forall_ne {s : set ℝ} (hs : convex s)
 begin
   contrapose! hf',
   rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩,
-  exact (convex_image_has_deriv_at hs hf).ord_connected (mem_image_of_mem f' ha)
+  exact (convex_image_has_deriv_at hs hf).ord_connected.out (mem_image_of_mem f' ha)
     (mem_image_of_mem f' hb) ⟨hma, hmb⟩
 end

src/analysis/calculus/mean_value.lean

@@ -773,7 +773,7 @@ theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f
   ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
 begin
   assume x y hx hy hxy,
-  have hxyD : Icc x y ⊆ D, from hD.ord_connected hx hy,
+  have hxyD : Icc x y ⊆ D, from hD.ord_connected.out hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
   obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
@@ -801,7 +801,7 @@ theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f
 begin
   assume x y hx hy hxy,
   cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
-  have hxyD : Icc x y ⊆ D, from hD.ord_connected hx hy,
+  have hxyD : Icc x y ⊆ D, from hD.ord_connected.out hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
   obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
@@ -946,7 +946,7 @@ convex_on_real_of_slope_mono_adjacent hD
 begin
   intros x y z hx hz hxy hyz,
   -- First we prove some trivial inclusions
-  have hxzD : Icc x z ⊆ D, from hD.ord_connected hx hz,
+  have hxzD : Icc x z ⊆ D, from hD.ord_connected.out hx hz,
   have hxyD : Icc x y ⊆ D, from subset.trans (Icc_subset_Icc_right $ le_of_lt hyz) hxzD,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,

src/category_theory/adjunction/fully_faithful.lean

@@ -30,7 +30,7 @@ See
 instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunction.unit h) :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.unit h) $ λ X,
 @yoneda.is_iso _ _ _ _ ((adjunction.unit h).app X)
-⟨{ app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
+⟨⟨{ app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
   ⟨begin
     ext x f, dsimp,
     apply L.map_injective,
@@ -40,7 +40,7 @@ instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunct
     simp only [adjunction.hom_equiv_counit, preimage_comp, preimage_map, category.assoc],
     rw ←h.unit_naturality,
     simp,
-  end⟩⟩
+  end⟩⟩⟩
 
 /--
 If the right adjoint is fully faithful, then the counit is an isomorphism.
@@ -51,7 +51,7 @@ instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjun
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.counit h) $ λ X,
 @is_iso_of_op _ _ _ _ _ $
 @coyoneda.is_iso _ _ _ _ ((adjunction.counit h).app X).op
-⟨{ app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
+⟨⟨{ app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
   ⟨begin
     ext x f, dsimp,
     apply R.map_injective,
@@ -61,7 +61,7 @@ instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjun
     simp only [adjunction.hom_equiv_unit, preimage_comp, preimage_map],
     rw ←h.counit_naturality,
     simp,
-  end⟩⟩
+  end⟩⟩⟩
 
 -- TODO also prove the converses?
 -- def L_full_of_unit_is_iso [is_iso (adjunction.unit h)] : full L := sorry

src/category_theory/adjunction/mates.lean

@@ -213,18 +213,18 @@ The converse is given in `transfer_nat_trans_self_of_iso`.
 -/
 instance transfer_nat_trans_self_iso (f : L₂ ⟶ L₁) [is_iso f] :
   is_iso (transfer_nat_trans_self adj₁ adj₂ f) :=
-⟨transfer_nat_trans_self adj₂ adj₁ (inv f),
-  ⟨transfer_nat_trans_self_comm _ _ (by simp), transfer_nat_trans_self_comm _ _ (by simp)⟩⟩
+⟨⟨transfer_nat_trans_self adj₂ adj₁ (inv f),
+  ⟨transfer_nat_trans_self_comm _ _ (by simp), transfer_nat_trans_self_comm _ _ (by simp)⟩⟩⟩
 
 /--
 If `f` is an isomorphism, then the un-transferred natural transformation is an isomorphism.
 The converse is given in `transfer_nat_trans_self_symm_of_iso`.
 -/
 instance transfer_nat_trans_self_symm_iso (f : R₁ ⟶ R₂) [is_iso f] :
   is_iso ((transfer_nat_trans_self adj₁ adj₂).symm f) :=
-⟨(transfer_nat_trans_self adj₂ adj₁).symm (inv f),
+⟨⟨(transfer_nat_trans_self adj₂ adj₁).symm (inv f),
   ⟨transfer_nat_trans_self_symm_comm _ _ (by simp),
-   transfer_nat_trans_self_symm_comm _ _ (by simp)⟩⟩
+   transfer_nat_trans_self_symm_comm _ _ (by simp)⟩⟩⟩
 
 /--
 If `f` is a natural transformation whose transferred natural transformation is an isomorphism,

src/category_theory/discrete_category.lean

@@ -70,7 +70,7 @@ lemma eq_of_hom {X Y : discrete α} (i : X ⟶ Y) : X = Y := i.down.down
 variables {C : Type u₂} [category.{v₂} C]
 
 instance {I : Type u₁} {i j : discrete I} (f : i ⟶ j) : is_iso f :=
-⟨eq_to_hom (eq_of_hom f).symm, by tidy⟩
+⟨⟨eq_to_hom (eq_of_hom f).symm, by tidy⟩⟩
 
 /--
 Any function `I → C` gives a functor `discrete I ⥤ C`.

src/category_theory/epi_mono.lean

@@ -83,7 +83,7 @@ instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi
 
 /-- A split mono which is epi is an iso. -/
 lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
-⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩
+⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩
 
 /--
 The chosen section of a split epimorphism.
@@ -99,7 +99,7 @@ instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (
 
 /-- A split epi which is mono is an iso. -/
 lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
-⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩
+⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩
 
 /-- Every iso is a split mono. -/
 @[priority 100]
@@ -126,12 +126,12 @@ instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
 /-- Every split mono whose retraction is mono is an iso. -/
 lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
   : is_iso f :=
-⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩
+⟨⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩⟩
 
 /-- Every split epi whose section is epi is an iso. -/
 lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
   : is_iso f :=
-⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩
+⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩
 
 instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [epi f] : mono f.unop :=
 ⟨λ Z g h eq, has_hom.hom.op_inj ((cancel_epi f).1 (has_hom.hom.unop_inj eq))⟩

src/category_theory/fully_faithful.lean

@@ -82,8 +82,8 @@ If the image of a morphism under a fully faithful functor in an isomorphism,
 then the original morphisms is also an isomorphism.
 -/
 lemma is_iso_of_fully_faithful (f : X ⟶ Y) [is_iso (F.map f)] : is_iso f :=
-⟨F.preimage (inv (F.map f)),
-  ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩
+⟨⟨F.preimage (inv (F.map f)),
+  ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩
 
 /-- If `F` is fully faithful, we have an equivalence of hom-sets `X ⟶ Y` and `F X ⟶ F Y`. -/
 def equiv_of_fully_faithful {X Y} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y) :=