-- Mathlib/CategoryTheory/IsConnected.lean
theorem zigzag_isPreconnected (h : ∀ j₁ j₂ : J, Zigzag j₁ j₂) : IsPreconnected J

Proof state:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
h : Zigzag j j'
⊢ F j = F j'

Tactic:
induction' h with j₁ j₂ _ hj ih

Result:
case h.refl
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j

case h.tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
hj : Zag j₁ j₂
ih : F j = F j₁
⊢ F j = F j₂

Proof state:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'

Tactic:
intro α F hF j j'

Result:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j'

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsPreconnected J

Tactic:
apply IsPreconnected.of_constant_of_preserves_morphisms

Result:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'

Proof state:
case h.tail.inl.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
ih : F j = F j₁
hj : j₁ ⟶ j₂
⊢ F j₁ = F j₂

case h.tail.inr.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
ih : F j = F j₁
hj : j₂ ⟶ j₁
⊢ F j₁ = F j₂

Tactic:
exacts [hF hj, (hF hj).symm]

Result:
no goals

Proof state:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j'

Tactic:
specialize h j j'

Result:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
h : Zigzag j j'
⊢ F j = F j'

Proof state:
case h.refl
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j

Tactic:
rfl

Result:
no goals

Proof state:
case h.tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
hj : Zag j₁ j₂
ih : F j = F j₁
⊢ F j = F j₂

Tactic:
rw [ih]

Result:
case h.tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
hj : Zag j₁ j₂
ih : F j = F j₁
⊢ F j₁ = F j₂

Proof state:
case h.tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
hj : Zag j₁ j₂
ih : F j = F j₁
⊢ F j₁ = F j₂

Tactic:
rcases hj with (⟨⟨hj⟩⟩|⟨⟨hj⟩⟩)

Result:
case h.tail.inl.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
ih : F j = F j₁
hj : j₁ ⟶ j₂
⊢ F j₁ = F j₂

case h.tail.inr.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j j' j₁ j₂ : J
a✝ : Relation.ReflTransGen Zag j j₁
ih : F j = F j₁
hj : j₂ ⟶ j₁
⊢ F j₁ = F j₂