awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p : ULift.{u₁, 0} Prop } = { down := j₂ ∈ p } := ⋯
i : (j ∈ p) = (j₀ ∈ p)
rwa rwa₁ rwa₂ rwa₃ : j₀ ∈ p
⊢ j ∈ p

Tactic:
rwa [i]
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀

Tactic:
simp [a f]
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j : J), Membership.mem (γ := Set J) {j : J | F j = F j₀} j

Tactic:
have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
      change F j₁ = F j₀ ↔ F j₂ = F j₀
      simp [a f])
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), Membership.mem (γ := Set J) {j : J | F j = F j₀} j
j j' : J
rw : F j₀ = F j'
rw₁ rw₂ : F j₀ = F j₀
⊢ F j = F j'

Tactic:
rw [w j, w j']
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
h :
  ∀ (p : Set (ULiftHom (ULift.{u₂, u₁} J))),
    { down := Classical.choice ⋯ } ∈ p →
      (∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) →
        ∀ (j : ULiftHom (ULift.{u₂, u₁} J)), j ∈ p
j₀ : ULiftHom (ULift.{u₂, u₁} J)
⊢ IsConnected (ULiftHom (ULift.{u₂, u₁} J))

Tactic:
apply IsConnected.of_induct

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
simp : Membership.mem (γ := Set J) {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p} (Classical.choice ⋯)
⊢ Classical.choice ⋯ ∈ p'

Tactic:
simp only [p']
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
⊢ Membership.mem (γ := Set J) {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p} (Classical.choice ⋯)

Tactic:
hj₀

Premises used: Set.Mem, setOf
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
⊢ Membership.mem (γ := Set J) {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p} (Classical.choice ⋯)

Tactic:
exact hj₀
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
⊢ Classical.choice ⋯ ∈ p'

Tactic:
have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
      simp only [p']
      exact hj₀
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
hj₀' : Classical.choice ⋯ ∈ p'
⊢ { down := j : ULift.{u₂, u₁} J } ∈ p

Tactic:
apply induct_on_objects p' hj₀' fun f => h ((ULiftHomULiftCategory.equiv J).functor.map f)

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, CategoryTheory.ULiftHomULiftCategory.equiv, CategoryTheory.induct_on_objects
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} 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₁
⊢ Membership.mem (γ := Set J) {j : J | Nonempty.{u_1} (Z j)} j₂

Tactic:
⟨h₁ f y⟩

Premises used: Set.Mem, setOf, Nonempty.intro
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} 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₁
⊢ Membership.mem (γ := Set J) {j : J | Nonempty.{u_1} (Z j)} j₂

Tactic:
exact ⟨h₁ f y⟩
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} 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₂
⊢ Membership.mem (γ := Set J) {j : J | Nonempty.{u_1} (Z j)} j₁

Tactic:
⟨h₂ f y⟩

Premises used: Set.Mem, setOf, Nonempty.intro
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} 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₂
⊢ Membership.mem (γ := Set J) {j : J | Nonempty.{u_1} (Z j)} j₁

Tactic:
exact ⟨h₂ f y⟩
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
e : Equivalence.{v₁, v₂, u₁, u₂} J K
⊢ IsPreconnected.{v₁, u₁} J ↔ IsPreconnected.{v₂, u₂} K

Tactic:
⟨fun _ => isPreconnected_of_equivalent e, fun _ => isPreconnected_of_equivalent e.symm⟩

Premises used: CategoryTheory.isPreconnected_of_equivalent, Iff.intro, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
e : Equivalence.{v₁, v₂, u₁, u₂} J K
inst_2 : IsConnected.{v₁, u₁} J
⊢ Nonempty J

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
e : Equivalence.{v₁, v₂, u₁, u₂} J K
⊢ IsConnected.{v₁, u₁} J ↔ IsConnected.{v₂, u₂} K

Tactic:
⟨fun _ => isConnected_of_equivalent e, fun _ => isConnected_of_equivalent e.symm⟩

Premises used: Iff.intro, CategoryTheory.Equivalence.symm, CategoryTheory.isConnected_of_equivalent
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} Jᵒᵖ
⊢ IsPreconnected.{v₁, u₁} J

Tactic:
isPreconnected_of_equivalent (opOpEquivalence J)

Premises used: CategoryTheory.isPreconnected_of_equivalent, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsConnected.{v₁, u₁} Jᵒᵖ
⊢ IsConnected.{v₁, u₁} J

Tactic:
isConnected_of_equivalent (opOpEquivalence J)

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.isConnected_of_equivalent
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ IsConnected.{v₁, u₁} Jᵒᵖ ↔ IsConnected.{v₁, u₁} J

Tactic:
⟨fun _ => isConnected_of_isConnected_op, fun _ => isConnected_op⟩

Premises used: CategoryTheory.isConnected_op, Iff.intro, CategoryTheory.isConnected_of_isConnected_op
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X : J
⊢ Zag.{v₁, u₁} X X

Tactic:
Or.inl ⟨𝟙 _⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, Or.inl, CategoryTheory.Zag
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Symmetric.{u₁ + 1} (α := J) Zag.{v₁, u₁}

Tactic:
fun _ _ h => h.symm

Premises used: Symmetric, Or.symm, CategoryTheory.Zag
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
h : Zag.{v₁, u₁} j₁ j₂
⊢ Zag.{v₁, u₁} j₂ j₁

Tactic:
zag_symmetric h

Premises used: CategoryTheory.zag_symmetric
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ Zag.{v₁, u₁} j₁ j₂

Tactic:
Or.inl ⟨f⟩

Premises used: Nonempty.intro, Or.inl, CategoryTheory.Zag
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
f : j₂ ⟶ j₁
⊢ Zag.{v₁, u₁} j₁ j₂

Tactic:
Or.inr ⟨f⟩

Premises used: Nonempty.intro, CategoryTheory.Zag, Or.inr
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Symmetric.{u₁ + 1} (α := J) Zigzag.{v₁, u₁}

Tactic:
Relation.ReflTransGen.symmetric zag_symmetric

Premises used: Relation.ReflTransGen.symmetric, CategoryTheory.Zigzag, CategoryTheory.zag_symmetric
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ _root_.Equivalence.{u₁ + 1} (α := J) Zigzag.{v₁, u₁}

Tactic:
⟨refl_of <| Relation.ReflTransGen _, (zigzag_symmetric ·), trans_of <| Relation.ReflTransGen _⟩

Premises used: refl_of, CategoryTheory.zigzag_symmetric, CategoryTheory.Zag, Equivalence.mk, trans_of, Relation.ReflTransGen
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X : J
⊢ Zigzag.{v₁, u₁} X X

Tactic:
zigzag_equivalence.refl _

Premises used: Equivalence.refl, CategoryTheory.zigzag_equivalence
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
h : Zigzag.{v₁, u₁} j₁ j₂
⊢ Zigzag.{v₁, u₁} j₂ j₁

Tactic:
zigzag_symmetric h

Premises used: CategoryTheory.zigzag_symmetric
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
h₁ : Zigzag.{v₁, u₁} j₁ j₂
h₂ : Zigzag.{v₁, u₁} j₂ j₃
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
zigzag_equivalence.trans h₁ h₂

Premises used: Equivalence.trans, CategoryTheory.zigzag_equivalence
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
h : Zag.{v₁, u₁} j₁ j₂
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
Relation.ReflTransGen.single h

Premises used: CategoryTheory.Zigzag, Relation.ReflTransGen.single
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
of_zag (Zag.of_hom f)

Premises used: CategoryTheory.Zigzag.of_zag, CategoryTheory.Zag.of_hom
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
f : j₂ ⟶ j₁
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
of_zag (Zag.of_inv f)

Premises used: CategoryTheory.Zigzag.of_zag, CategoryTheory.Zag.of_inv
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
h₁ : Zag.{v₁, u₁} j₁ j₂
h₂ : Zag.{v₁, u₁} j₂ j₃
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
trans (of_zag h₁) (of_zag h₂)

Premises used: CategoryTheory.Zigzag.of_zag, CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
f₁₂ : j₁ ⟶ j₂
f₂₃ : j₂ ⟶ j₃
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
(of_hom f₁₂).trans (of_hom f₂₃)

Premises used: CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_hom
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
f₁₂ : j₁ ⟶ j₂
f₃₂ : j₃ ⟶ j₂
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
(of_hom f₁₂).trans (of_inv f₃₂)

Premises used: CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_hom, CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
f₂₁ : j₂ ⟶ j₁
f₂₃ : j₂ ⟶ j₃
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
(of_inv f₂₁).trans (of_hom f₂₃)

Premises used: CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_hom, CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ j₃ : J
f₂₁ : j₂ ⟶ j₁
f₃₂ : j₃ ⟶ j₂
⊢ Zigzag.{v₁, u₁} j₁ j₃

Tactic:
(of_inv f₂₁).trans (of_inv f₃₂)

Premises used: CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : Prefunctor.{v₁, v₂, u₁, u₂} J K
j₁ j₂ : J
h : Zigzag.{v₁, u₁} j₁ j₂
⊢ Zigzag.{v₂, u₂} (F.obj j₁) (F.obj j₂)

Tactic:
h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)

Premises used: Relation.ReflTransGen.lift, CategoryTheory.Zigzag, Prefunctor.map, Nonempty.map, Or.imp
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : Functor.{v₁, v₂, u₁, u₂} J K
j₁ j₂ : J
h : Zigzag.{v₁, u₁} j₁ j₂
⊢ Zigzag.{v₂, u₂} (F.obj j₁) (F.obj j₂)

Tactic:
zigzag_prefunctor_obj_of_zigzag F.toPrefunctor h

Premises used: CategoryTheory.Functor.toPrefunctor, CategoryTheory.zigzag_prefunctor_obj_of_zigzag
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
X : Type u_1
a b : Discrete X
h : Zag a b
⊢ a.as = b.as

Tactic:
h.elim (fun ⟨f⟩ ↦ Discrete.eq_of_hom f) (fun ⟨f⟩ ↦ (Discrete.eq_of_hom f).symm)

Premises used: _private.0.CategoryTheory.eq_of_zag.match_2, CategoryTheory.Discrete.as, CategoryTheory.Discrete.eq_of_hom, _private.0.CategoryTheory.eq_of_zag.match_1, Or.elim, Eq.symm, Eq
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
X : Type u_1
a b : Discrete X
⊢ a.as = a.as

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
X : Type u_1
a b b_1 c : Discrete X
h_1 : Relation.ReflTransGen Zag a b_1
h : Zag b_1 c
eq : a.as = b_1.as
⊢ a.as = c.as

Tactic:
eq.trans (eq_of_zag _ h)

Premises used: CategoryTheory.eq_of_zag, Eq.trans
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
X : Type u_1
a b b_1 c : Discrete X
h_1 : Relation.ReflTransGen Zag a b_1
h : Zag b_1 c
eq : a.as = b_1.as
⊢ a.as = c.as

Tactic:
exact eq.trans (eq_of_zag _ h)

Premises used: CategoryTheory.eq_of_zag, Eq.trans
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
X : Type u_1
a b : Discrete X
h : Zigzag a b
refl : a.as = a.as
tail : ∀ {b c : Discrete X}, Relation.ReflTransGen Zag a b → ∀ (h : Zag b c) (eq : a.as = b.as), a.as = c.as
⊢ a.as = b.as

Tactic:
induction h with
  | refl => rfl
  | tail _ h eq => exact eq.trans (eq_of_zag _ h)

Premises used: refl
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : Functor.{v₁, v₂, u₁, u₂} J K
inst_2 : F.Full
j₁ j₂ : J
h : Zag.{v₂, u₂} (F.obj j₁) (F.obj j₂)
⊢ Zag.{v₁, u₁} j₁ j₂

Tactic:
Or.imp (Nonempty.map F.preimage) (Nonempty.map F.preimage) h

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Zag, Nonempty.map, Or.imp
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
have : ∀ (z : ∀ (j : J), r j₁ j), r j₁ j₂
⊢ r j₁ j₂

Tactic:
have z : ∀ j : J, r j₁ j :=
    induct_on_objects {k | r j₁ k} (hr.1 j₁)
      fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
z : ∀ (j : J), r j₁ j
⊢ r j₁ j₂

Tactic:
z j₂
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
z : ∀ (j : J), r j₁ j
⊢ r j₁ j₂

Tactic:
exact z j₂
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
j₁ j₂ : J
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
equiv_relation _ zigzag_equivalence
    (fun f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _

Premises used: Nonempty.intro, Relation.ReflTransGen.single, CategoryTheory.equiv_relation, Or.inl, CategoryTheory.zigzag_equivalence
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
h₁ : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
⊢ IsPreconnected.{v₁, u₁} J

Tactic:
apply IsPreconnected.of_constant_of_preserves_morphisms

Premises used: CategoryTheory.IsPreconnected.of_constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ Zigzag.{v₁, u₁} j j'

Tactic:
specialize h j j'
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h_1 : Relation.ReflTransGen Zag.{v₁, u₁} j b
hj : Zag.{v₁, u₁} b c
ih : F j = F b
h : F b = F c
⊢ F j = F c

Tactic:
rw [ih]
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h_1 : Relation.ReflTransGen Zag.{v₁, u₁} j b
hj : Zag.{v₁, u₁} b c
ih : F j = F b
h : ∀ (hj : b ⟶ c), F b = F c
h₁ : ∀ (hj : c ⟶ b), F b = F c
⊢ F b = F c

Tactic:
rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h : Relation.ReflTransGen Zag.{v₁, u₁} j b
ih : F j = F b
hj : b ⟶ c
⊢ F b = F c

Tactic:
hF hj
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h : Relation.ReflTransGen Zag.{v₁, u₁} j b
ih : F j = F b
hj : c ⟶ b
⊢ F b = F c

Tactic:
(hF hj).symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h : Relation.ReflTransGen Zag.{v₁, u₁} j b
ih : F j = F b
hj : b ⟶ c
⊢ F b = F c

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

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
h : Zigzag.{v₁, u₁} j j'
h₁ : F j = F j
h₂ : ∀ {b c : J}, Relation.ReflTransGen Zag.{v₁, u₁} j b → ∀ (hj : Zag.{v₁, u₁} b c) (ih : F j = F b), F j = F c
⊢ F j = F j'

Tactic:
induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]

Premises used: refl
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
⊢ IsConnected.{v₁, u₁} J

Tactic:
{ zigzag_isPreconnected h with }

Premises used: CategoryTheory.zigzag_isPreconnected, CategoryTheory.IsConnected.mk
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsConnected.{v₁, u₁} J
j₁ j₂ : J
⊢ ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
List.exists_isChain_cons_of_relationReflTransGen (isPreconnected_zigzag _ _)

Premises used: CategoryTheory.isPreconnected_zigzag, List.exists_isChain_cons_of_relationReflTransGen
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
h₁ : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
⊢ IsPreconnected.{v₁, u₁} J

Tactic:
apply zigzag_isPreconnected

Premises used: CategoryTheory.zigzag_isPreconnected
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
h₁ : ∀ (l : List J) (hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)) (hl₂ : (j₁ :: l).getLast ⋯ = j₂), Zigzag.{v₁, u₁} j₁ j₂
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
apply List.relationReflTransGen_of_exists_isChain_cons l hl₁ hl₂

Premises used: List.relationReflTransGen_of_exists_isChain_cons
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{v₁, u₁} J

Tactic:
{ isPreconnected_of_zigzag h with }

Premises used: CategoryTheory.isPreconnected_of_zigzag, CategoryTheory.IsConnected.mk
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type w₂
inst_1 : Category.{w₁, w₂} C
inst_2 : IsPreconnected.{v₁, u₁} J
X Y : C
α : Quiver.Hom (V := Functor.{v₁, w₁, u₁, w₂} J C) (obj (const J) X) (obj (const J) Y)
x x_1 : J
f : x ⟶ x_1
⊢ Eq.{w₁ + 1} (α := X ⟶ Y) ((fun (j : J) ↦ α.app j) x) ((fun (j : J) ↦ α.app j) x_1)

Tactic:
simpa using (α.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type w₂
inst_2 : Category.{w₁, w₂} C
inst_3 : IsConnected.{v₁, u₁} J
X Y : C
f : Quiver.Hom (V := Functor.{v₁, w₁, u₁, w₂} J C) (obj (const J) X) (obj (const J) Y)
w : ∀ (j : J), NatTrans.app (map (const J) (f.app (Classical.arbitrary J))) j = f.app j
⊢ map (const J) (f.app (Classical.arbitrary J)) = f

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type w₂
inst_2 : Category.{w₁, w₂} C
inst_3 : IsConnected.{v₁, u₁} J
X Y : C
f : Quiver.Hom (V := Functor.{v₁, w₁, u₁, w₂} J C) (obj (const J) X) (obj (const J) Y)
j : J
⊢ NatTrans.app (map (const J) (f.app (Classical.arbitrary J))) j = f.app j

Tactic:
apply nat_trans_from_is_connected f (Classical.arbitrary J) j

Premises used: Classical.arbitrary, CategoryTheory.nat_trans_from_is_connected
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
G : Type u_1
inst : Groupoid.{u_2, u_1} G
inst_1 : IsPreconnected.{u_2, u_1} G
⊢ ∀ (x y : G), Nonempty.{u_2 + 1} (x ⟶ y)

Tactic:
equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro

Premises used: Nonempty.intro, CategoryTheory.equiv_relation
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
G : Type u_1
inst : Groupoid.{u_2, u_1} G
inst_1 : IsPreconnected.{u_2, u_1} G
refine : _root_.Equivalence fun (x y : G) ↦ Nonempty.{u_2 + 1} (x ⟶ y)
⊢ ∀ (x y : G), Nonempty.{u_2 + 1} (x ⟶ y)

Tactic:
refine equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro

Premises used: Nonempty.intro, CategoryTheory.equiv_relation