case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ IsConnected J
apply zigzag_isConnected
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
j₁ j₂ : J
⊢ Zigzag j₁ j₂
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂
intro j₁ j₂
case h.intro.intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
j₁ j₂ : J
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ Zigzag j₁ j₂
case h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
j₁ j₂ : J
⊢ Zigzag j₁ j₂
rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩
no goals
case h.intro.intro
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
j₁ j₂ : J
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ Zigzag j₁ j₂
apply List.relationReflTransGen_of_exists_chain l hl₁ hl₂