[GOAL]
α : Type u₁
X : Discrete α
⊢ { as := X.as } = X
[PROOFSTEP]
ext
[GOAL]
case as
α : Type u₁
X : Discrete α
⊢ { as := X.as }.as = X.as
[PROOFSTEP]
rfl
[GOAL]
α : Type u₁
⊢ Function.LeftInverse Discrete.mk Discrete.as
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
⊢ Function.RightInverse Discrete.mk Discrete.as
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y Z : Discrete α
g : X ⟶ Y
f : Y ⟶ Z
⊢ X ⟶ Z
[PROOFSTEP]
cases X
[GOAL]
case mk
α : Type u₁
Y Z : Discrete α
f : Y ⟶ Z
as✝ : α
g : { as := as✝ } ⟶ Y
⊢ { as := as✝ } ⟶ Z
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
α : Type u₁
Z : Discrete α
as✝¹ as✝ : α
f : { as := as✝ } ⟶ Z
g : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝¹ } ⟶ Z
[PROOFSTEP]
cases Z
[GOAL]
case mk.mk.mk
α : Type u₁
as✝² as✝¹ : α
g : { as := as✝² } ⟶ { as := as✝¹ }
as✝ : α
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝² } ⟶ { as := as✝ }
[PROOFSTEP]
rcases f with ⟨⟨⟨⟩⟩⟩
[GOAL]
case mk.mk.mk.up.up.refl
α : Type u₁
as✝¹ as✝ : α
g : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝¹ } ⟶ { as := as✝ }
[PROOFSTEP]
exact g
[GOAL]
α : Type u₁
inst✝ : Subsingleton α
⊢ ∀ (a b : Discrete α), a = b
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
i j : Discrete I
f : i ⟶ j
⊢ f ≫ Discrete.eqToHom (_ : j.as = i.as) = 𝟙 i ∧ Discrete.eqToHom (_ : j.as = i.as) ≫ f = 𝟙 j
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ (F ∘ as) X ⟶ (F ∘ as) Y
[PROOFSTEP]
dsimp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ F X.as ⟶ F Y.as
[PROOFSTEP]
rcases f with ⟨⟨h⟩⟩
[GOAL]
case up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
h : X.as = Y.as
⊢ F X.as ⟶ F Y.as
[PROOFSTEP]
exact eqToHom (congrArg _ h)
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
⊢ (functor F).map f = 𝟙 (F i.as)
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X Y : Discrete I
x✝ : X ⟶ Y
g : X.as = Y.as
⊢ F.map { down := { down := g } } ≫ f Y = f X ≫ G.map { down := { down := g } }
[PROOFSTEP]
discrete_cases
[GOAL]
case mk.mk.up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝¹ as✝ : I
g down✝ : { as := as✝¹ }.as = { as := as✝ }.as
⊢ F.map { down := { down := g } } ≫ f { as := as✝ } = f { as := as✝¹ } ≫ G.map { down := { down := g } }
[PROOFSTEP]
rcases g
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } } ≫ f { as := as✝ } =
    f { as := as✝ } ≫ G.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } }
[PROOFSTEP]
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map (𝟙 { as := as✝ }) ≫ f { as := as✝ } = f { as := as✝ } ≫ G.map (𝟙 { as := as✝ })
[PROOFSTEP]
simp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X✝ Y✝ : Discrete I
x✝ : X✝ ⟶ Y✝
g : X✝.as = Y✝.as
⊢ F.map { down := { down := g } } ≫ (f Y✝).hom = (f X✝).hom ≫ G.map { down := { down := g } }
[PROOFSTEP]
discrete_cases
[GOAL]
case mk.mk.up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝¹ as✝ : I
g down✝ : { as := as✝¹ }.as = { as := as✝ }.as
⊢ F.map { down := { down := g } } ≫ (f { as := as✝ }).hom = (f { as := as✝¹ }).hom ≫ G.map { down := { down := g } }
[PROOFSTEP]
rcases g
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } } ≫ (f { as := as✝ }).hom =
    (f { as := as✝ }).hom ≫ G.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } }
[PROOFSTEP]
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map (𝟙 { as := as✝ }) ≫ (f { as := as✝ }).hom = (f { as := as✝ }).hom ≫ G.map (𝟙 { as := as✝ })
[PROOFSTEP]
simp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
⊢ (natIso f).app i = f i
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
i : Discrete I
⊢ (𝟭 (Discrete I)).obj i = (functor (mk ∘ ↑e) ⋙ functor (mk ∘ ↑e.symm)).obj i
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
j : Discrete J
⊢ (functor (mk ∘ ↑e.symm) ⋙ functor (mk ∘ ↑e)).obj j = (𝟭 (Discrete J)).obj j
[PROOFSTEP]
aesop_cat
[GOAL]
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a
[PROOFSTEP]
simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
[GOAL]
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : β
⊢ (as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a
[PROOFSTEP]
simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)
[PROOFSTEP]
have h : f = 𝟙 j := by aesop_cat
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)
[PROOFSTEP]
rw [h]
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
[PROOFSTEP]
simp
