case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ ∀ (p : Set J), ?j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p

case j₀
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsConnected J
apply IsConnected.of_induct
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ j ∈ p

case j₀
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ ∀ (p : Set J), ?j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p

case j₀
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
intro p hp hjp j
no goals
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
this : ∀ (j₁ j₂ : J), Zigzag j₁ j₂ → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ j ∈ p

case j₀
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
rwa [this j (Classical.arbitrary J) (h _ _)]
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ : J
k : Zigzag j₁ j₂
⊢ j₁ ∈ p ↔ j₂ ∈ p
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂ → (j₁ ∈ p ↔ j₂ ∈ p)
introv k
case refl
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ : J
⊢ j₁ ∈ p ↔ j₁ ∈ p

case tail
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
zag : Zag b✝ c✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
⊢ j₁ ∈ p ↔ c✝ ∈ p
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ : J
k : Zigzag j₁ j₂
⊢ j₁ ∈ p ↔ j₂ ∈ p
induction' k with _ _ _ zag k_ih
no goals
case refl
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ : J
⊢ j₁ ∈ p ↔ j₁ ∈ p
rfl
case tail
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
zag : Zag b✝ c✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
⊢ b✝ ∈ p ↔ c✝ ∈ p
case tail
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
zag : Zag b✝ c✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
⊢ j₁ ∈ p ↔ c✝ ∈ p
rw [k_ih]
case tail.inl
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (b✝ ⟶ c✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p

case tail.inr
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (c✝ ⟶ b✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p
case tail
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
zag : Zag b✝ c✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
⊢ b✝ ∈ p ↔ c✝ ∈ p
cases' zag with zag zag
case tail.inr
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (c✝ ⟶ b✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p
case tail.inl
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (b✝ ⟶ c✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p

case tail.inr
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (c✝ ⟶ b✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p
apply hjp (Nonempty.some zag)
no goals
case tail.inr
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
p : Set J
hp : ?j₀ ∈ p
hjp : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j j₁ j₂ b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j₁ b✝
k_ih : j₁ ∈ p ↔ b✝ ∈ p
zag : Nonempty (c✝ ⟶ b✝)
⊢ b✝ ∈ p ↔ c✝ ∈ p
exact (hjp (Nonempty.some zag)).symm