J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsConnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
z : ∀ (j : J), r (Classical.arbitrary J) j
⊢ ∀ (j₁ j₂ : J), r j₁ j₂
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsConnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
⊢ ∀ (j₁ j₂ : J), r j₁ j₂
have z : ∀ j : J, r (Classical.arbitrary J) j :=
  induct_on_objects (fun k => r (Classical.arbitrary J) k) (hr.1 (Classical.arbitrary J))
    fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsConnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
z : ∀ (j : J), r (Classical.arbitrary J) j
j₁✝ j₂✝ : J
⊢ r j₁✝ j₂✝
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsConnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
z : ∀ (j : J), r (Classical.arbitrary J) j
⊢ ∀ (j₁ j₂ : J), r j₁ j₂
intros
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : IsConnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
z : ∀ (j : J), r (Classical.arbitrary J) j
j₁✝ j₂✝ : J
⊢ r j₁✝ j₂✝
apply hr.3 (hr.2 (z _)) (z _)