no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
α : Type u₁
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j'
simpa using
  any_functor_const_on_obj
    { obj := Discrete.mk ∘ F
      map := @fun _ _ f =>
        eqToHom
          (by
            ext
            exact h _ _ f) }
    j j'
case as
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
α : Type u₁
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Discrete.mk ∘ F) x✝¹).as = ((Discrete.mk ∘ F) x✝).as
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
α : Type u₁
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Discrete.mk ∘ F) x✝¹ = (Discrete.mk ∘ F) x✝
ext
no goals
case as
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
α : Type u₁
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Discrete.mk ∘ F) x✝¹).as = ((Discrete.mk ∘ F) x✝).as
exact h _ _ f