J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₂
inst✝¹ : Category C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : ((Functor.const J).obj X).map f ≫ α.app x✝ = α.app x✝¹ ≫ ((Functor.const J).obj Y).map f
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₂
inst✝¹ : Category C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
have := α.naturality f
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₂
inst✝¹ : Category C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : α.app x✝ = α.app x✝¹
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₂
inst✝¹ : Category C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : ((Functor.const J).obj X).map f ≫ α.app x✝ = α.app x✝¹ ≫ ((Functor.const J).obj Y).map f
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
erw [id_comp, comp_id] at this
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₂
inst✝¹ : Category C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : α.app x✝ = α.app x✝¹
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
exact this.symm