J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
⊢ j ∈ p
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ j ∈ p
let aux (j₁ j₂ : J) (f : j₁ ⟶  j₂) := congrArg ULift.up <| (h1 f).to_eq
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
⊢ j ∈ p
injection constant_of_preserves_morphisms (fun k => ULift.up (k ∈ p)) aux j j₀ with i
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p
rwa [i]