[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
α : Type u₂
F : J ⥤ Discrete α
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (CategoryTheory.IsPreconnected.IsoConstantAux.liftToDiscrete F ⋙ Discrete.functor F.obj).map f ≫
        ((fun j => eqToIso (_ : F.obj (Function.invFun (fun x => F.obj x) (F.obj j)) = F.obj j)) Y).hom =
      ((fun j => eqToIso (_ : F.obj (Function.invFun (fun x => F.obj x) (F.obj j)) = F.obj j)) X).hom ≫ F.map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j : J
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((Functor.const J).obj ((CategoryTheory.IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙
              Discrete.functor F.obj).map
          f ≫
        ((fun j' => eqToIso (_ : F.obj (Function.invFun (fun x => F.obj x) (F.obj j)) = F.obj j)) Y).hom =
      ((fun j' => eqToIso (_ : F.obj (Function.invFun (fun x => F.obj x) (F.obj j)) = F.obj j)) X).hom ≫
        ((Functor.const J).obj (F.obj j)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ F.obj j = F.obj j'
[PROOFSTEP]
ext
[GOAL]
case as
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as
[PROOFSTEP]
exact ((isoConstant F j').hom.app j).down.1
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j'
[PROOFSTEP]
simpa using
  any_functor_const_on_obj
    { obj := Discrete.mk ∘ F
      map :=
        @fun _ _ f =>
          eqToHom
            (by
              ext
              exact h _ _ f) }
    j j'
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Discrete.mk ∘ F) x✝¹ = (Discrete.mk ∘ F) x✝
[PROOFSTEP]
ext
[GOAL]
case as
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Discrete.mk ∘ F) x✝¹).as = ((Discrete.mk ∘ F) x✝).as
[PROOFSTEP]
exact h _ _ f
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
x✝ : Type u₁
F : J ⥤ Discrete x✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ F.obj j₁✝ = F.obj j₂✝
[PROOFSTEP]
ext
[GOAL]
case as
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
x✝ : Type u₁
F : J ⥤ Discrete x✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as
[PROOFSTEP]
exact Discrete.eq_of_hom (F.map f)
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ j ∈ p
[PROOFSTEP]
let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).to_eq
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
⊢ j ∈ p
[PROOFSTEP]
injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.to_eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p
[PROOFSTEP]
rwa [i]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'
[PROOFSTEP]
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]; )
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ j₁ ∈ {j | F j = F j₀} ↔ j₂ ∈ {j | F j = F j₀}
[PROOFSTEP]
change F j₁ = F j₀ ↔ F j₂ = F j₀
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀
[PROOFSTEP]
simp [a f]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
[PROOFSTEP]
intro j j'
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j = F j'
[PROOFSTEP]
rw [w j, w j']
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
⊢ IsConnected (ULiftHom (ULift J))
[PROOFSTEP]
have : Nonempty (ULiftHom.{v₂} (ULift.{u₂} J)) := by simp [ULiftHom, hc.is_nonempty]
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
⊢ Nonempty (ULiftHom (ULift J))
[PROOFSTEP]
simp [ULiftHom, hc.is_nonempty]
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
⊢ IsConnected (ULiftHom (ULift J))
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
⊢ ∀ (p : Set (ULiftHom (ULift J))),
    ?j₀ ∈ p → (∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : ULiftHom (ULift J)), j ∈ p
case j₀
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
⊢ ULiftHom (ULift J)
[PROOFSTEP]
rintro p hj₀ h ⟨j⟩
[GOAL]
case h.up
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
p : Set (ULiftHom (ULift J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ { down := j } ∈ p
case j₀
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
⊢ ULiftHom (ULift J)
[PROOFSTEP]
let p' : Set J := {j : J | p ⟨j⟩}
[GOAL]
case h.up
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
p : Set (ULiftHom (ULift J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
p' : Set J := {j | p { down := j }}
⊢ { down := j } ∈ p
case j₀
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
⊢ ULiftHom (ULift J)
[PROOFSTEP]
have hj₀' : Classical.choice hc.is_nonempty ∈ p' :=
  by
  simp only [(eq_self p')]
  exact hj₀
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
p : Set (ULiftHom (ULift J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
p' : Set J := {j | p { down := j }}
⊢ Classical.choice (_ : Nonempty J) ∈ p'
[PROOFSTEP]
simp only [(eq_self p')]
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
p : Set (ULiftHom (ULift J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
p' : Set J := {j | p { down := j }}
⊢ Classical.choice (_ : Nonempty J) ∈ {j | p { down := j }}
[PROOFSTEP]
exact hj₀
[GOAL]
case h.up
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
this : Nonempty (ULiftHom (ULift J))
p : Set (ULiftHom (ULift J))
hj₀ : { down := Classical.choice (_ : Nonempty J) } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift J)}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
p' : Set J := {j | p { down := j }}
hj₀' : Classical.choice (_ : Nonempty J) ∈ p'
⊢ { down := j } ∈ p
[PROOFSTEP]
apply induct_on_objects p' hj₀' @fun _ _ f => h ((ULiftHomULiftCategory.equiv J).functor.map f)
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected 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₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)} → j₂✝ ∈ {j | Nonempty (Z j)}
[PROOFSTEP]
rintro ⟨y⟩
[GOAL]
case intro
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected 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₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}
[PROOFSTEP]
exact ⟨h₁ f y⟩
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected 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₂✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)} → j₁✝ ∈ {j | Nonempty (Z j)}
[PROOFSTEP]
rintro ⟨y⟩
[GOAL]
case intro
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected 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₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}
[PROOFSTEP]
exact ⟨h₂ f y⟩
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
e : J ≌ K
inst✝ : IsConnected J
⊢ Nonempty J
[PROOFSTEP]
infer_instance
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂
[PROOFSTEP]
have z : ∀ j : J, r (Classical.arbitrary J) j :=
  induct_on_objects {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))⟩
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂✝
[PROOFSTEP]
apply hr.3 (hr.2 (z _)) (z _)
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsConnected J
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
[PROOFSTEP]
intro p hp hjp j
[GOAL]
case h
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
[PROOFSTEP]
have : ∀ j₁ j₂ : J, Zigzag j₁ j₂ → (j₁ ∈ p ↔ j₂ ∈ p) :=
  by
  introv k
  induction' k with _ _ _ zag k_ih
  · rfl
  · rw [k_ih]
    cases' zag with zag zag
    apply hjp (Nonempty.some zag)
    exact (hjp (Nonempty.some zag)).symm
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)
[PROOFSTEP]
introv k
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
induction' k with _ _ _ zag k_ih
[GOAL]
case refl
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
rfl
[GOAL]
case tail
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
rw [k_ih]
[GOAL]
case tail
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
cases' zag with zag zag
[GOAL]
case tail.inl
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
apply hjp (Nonempty.some zag)
[GOAL]
case tail.inr
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
exact (hjp (Nonempty.some zag)).symm
[GOAL]
case h
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ J
[PROOFSTEP]
rwa [this j (Classical.arbitrary J) (h _ _)]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : Nonempty J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ IsConnected J
[PROOFSTEP]
apply zigzag_isConnected
[GOAL]
case h
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂
[PROOFSTEP]
intro j₁ j₂
[GOAL]
case h
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂
[PROOFSTEP]
rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩
[GOAL]
case h.intro.intro
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} 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₂
[PROOFSTEP]
apply List.relationReflTransGen_of_exists_chain l hl₁ hl₂
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₂
inst✝¹ : Category.{u₁, u₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (fun j => NatTrans.app α j) x✝¹ = (fun j => NatTrans.app α j) x✝
[PROOFSTEP]
have := α.naturality f
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₂
inst✝¹ : Category.{u₁, u₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : ((Functor.const J).obj X).map f ≫ NatTrans.app α x✝ = NatTrans.app α x✝¹ ≫ ((Functor.const J).obj Y).map f
⊢ (fun j => NatTrans.app α j) x✝¹ = (fun j => NatTrans.app α j) x✝
[PROOFSTEP]
erw [id_comp, comp_id] at this
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₂
inst✝¹ : Category.{u₁, u₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : NatTrans.app α x✝ = NatTrans.app α x✝¹
⊢ (fun j => NatTrans.app α j) x✝¹ = (fun j => NatTrans.app α j) x✝
[PROOFSTEP]
exact this.symm
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₂
inst✝¹ : Category.{u₁, u₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (Functor.const J).obj X✝ ⟶ (Functor.const J).obj Y✝
⊢ (Functor.const J).map ((fun {X Y} f => NatTrans.app f (Classical.arbitrary J)) f) = f
[PROOFSTEP]
ext j
[GOAL]
case w.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₂
inst✝¹ : Category.{u₁, u₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (Functor.const J).obj X✝ ⟶ (Functor.const J).obj Y✝
j : J
⊢ NatTrans.app ((Functor.const J).map ((fun {X Y} f => NatTrans.app f (Classical.arbitrary J)) f)) j = NatTrans.app f j
[PROOFSTEP]
apply nat_trans_from_is_connected f (Classical.arbitrary J) j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₂
inst✝² : Category.{u₁, u₂} C
G : Type ?u.28353
inst✝¹ : Groupoid G
inst✝ : IsConnected G
⊢ ∀ (x y : G), Nonempty (x ⟶ y)
[PROOFSTEP]
refine' equiv_relation _ _ @fun j₁ j₂ => Nonempty.intro
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₂
inst✝² : Category.{u₁, u₂} C
G : Type ?u.28353
inst✝¹ : Groupoid G
inst✝ : IsConnected G
⊢ _root_.Equivalence fun x y => Nonempty (x ⟶ y)
[PROOFSTEP]
exact ⟨fun j => ⟨𝟙 _⟩, @fun j₁ j₂ => Nonempty.map fun f => inv f, @fun _ _ _ => Nonempty.map2 (· ≫ ·)⟩