Theorem: Category.ΨΦ (CategoryTheory/Yoneda.lean)

State before:
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
⊢ Ψ (Φ η) = η
Tactic:
ext B
State after:
case app.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
⊢ NatTrans.app (Ψ (Φ η)) B = NatTrans.app η B

State before:
case app.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
⊢ NatTrans.app (Ψ (Φ η)) B = NatTrans.app η B
Tactic:
funext f
State after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f

State before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
have := congrFun (η.naturality f) (𝟙 A)
State after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : (NatTrans.app η B ∘ Functor.map (CoHom A) f) (𝟙 A) = (Functor.map F f ∘ NatTrans.app η A) (𝟙 A)
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f

State before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : (NatTrans.app η B ∘ Functor.map (CoHom A) f) (𝟙 A) = (Functor.map F f ∘ NatTrans.app η A) (𝟙 A)
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
simp at this
State after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : NatTrans.app η B f = Functor.map F f (NatTrans.app η A (𝟙 A))
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f

State before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : NatTrans.app η B f = Functor.map F f (NatTrans.app η A (𝟙 A))
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
exact this.symm
State after:
no goals