case intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)} → j₂✝ ∈ {j | Nonempty (Z j)}
rintro ⟨y⟩
no goals
case intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}
exact ⟨h₁ f y⟩
case intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)} → j₁✝ ∈ {j | Nonempty (Z j)}
rintro ⟨y⟩
no goals
case intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}
exact ⟨h₂ f y⟩