chore(CategoryTheory/DiscreteCategory): remove unecessary line in pro…

…of (#12382)
leanprover-community · Apr 23, 2024 · f0ba14a · f0ba14a
1 parent ec75ee1
commit f0ba14a
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -54,7 +54,6 @@ structure Discrete (α : Type u₁) where
 
 @[simp]
 theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X := by
-  ext
   rfl
 #align category_theory.discrete.mk_as CategoryTheory.Discrete.mk_as