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

State before:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ Φ (Ψ x) = x
Tactic:
unfold Φ Ψ
State after:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ NatTrans.app
      { app := fun B f => Functor.map F f x,
        naturality :=
          (_ :
            ∀ {B C : α} (f : B ⟶ C),
              (fun B f => Functor.map F f x) C ∘ Functor.map (CoHom A) f =
                Functor.map F f ∘ (fun B f => Functor.map F f x) B) }
      A (𝟙 A) =
    x

State before:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ NatTrans.app
      { app := fun B f => Functor.map F f x,
        naturality :=
          (_ :
            ∀ {B C : α} (f : B ⟶ C),
              (fun B f => Functor.map F f x) C ∘ Functor.map (CoHom A) f =
                Functor.map F f ∘ (fun B f => Functor.map F f x) B) }
      A (𝟙 A) =
    x
Tactic:
simp
State after:
no goals