J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)
J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)
have h : f = 𝟙 j := by aesop_cat
J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)
rw [h]
no goals
J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
simp
no goals
J : Type v₁
C : Type u₂
inst✝ : Category C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j
aesop_cat