[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j : ConnectedComponents J
⊢ Nonempty (Component j)
[PROOFSTEP]
induction j using Quotient.inductionOn'
[GOAL]
case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
a✝ : J
⊢ Nonempty (Component (Quotient.mk'' a✝))
[PROOFSTEP]
exact ⟨⟨_, rfl⟩⟩
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j : ConnectedComponents J
⊢ IsConnected (Component j)
[PROOFSTEP]
apply isConnected_of_zigzag
[GOAL]
case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j : ConnectedComponents J
⊢ ∀ (j₁ j₂ : Component j), ∃ l, List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
[PROOFSTEP]
rintro ⟨j₁, hj₁⟩
  ⟨j₂, rfl⟩
      -- We know that the underlying objects j₁ j₂ have some zigzag between them in `J`
[GOAL]
case h.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
⊢ ∃ l,
    List.Chain Zag { obj := j₁, property := hj₁ } l ∧
      List.getLast ({ obj := j₁, property := hj₁ } :: l) (_ : { obj := j₁, property := hj₁ } :: l ≠ []) =
        { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
have h₁₂ : Zigzag j₁ j₂ := Quotient.exact' hj₁
[GOAL]
case h.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
⊢ ∃ l,
    List.Chain Zag { obj := j₁, property := hj₁ } l ∧
      List.getLast ({ obj := j₁, property := hj₁ } :: l) (_ : { obj := j₁, property := hj₁ } :: l ≠ []) =
        { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
rcases List.exists_chain_of_relationReflTransGen h₁₂ with
  ⟨l, hl₁, hl₂⟩
    -- Everything which has a zigzag to j₂ can be lifted to the same component as `j₂`.
[GOAL]
case h.mk.mk.intro.intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
⊢ ∃ l,
    List.Chain Zag { obj := j₁, property := hj₁ } l ∧
      List.getLast ({ obj := j₁, property := hj₁ } :: l) (_ : { obj := j₁, property := hj₁ } :: l ≠ []) =
        { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
let f : ∀ x, Zigzag x j₂ → Component (Quotient.mk'' j₂) := fun x h =>
  ⟨x, Quotient.sound' h⟩
    -- Everything in our chosen zigzag from `j₁` to `j₂` has a zigzag to `j₂`.
[GOAL]
case h.mk.mk.intro.intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
⊢ ∃ l,
    List.Chain Zag { obj := j₁, property := hj₁ } l ∧
      List.getLast ({ obj := j₁, property := hj₁ } :: l) (_ : { obj := j₁, property := hj₁ } :: l ≠ []) =
        { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
  intro i hi
  apply List.Chain.induction (fun t => Zigzag t j₂) _ hl₁ hl₂ _ _ _ (List.mem_of_mem_tail hi)
  · intro j k
    apply Relation.ReflTransGen.head
  · apply Relation.ReflTransGen.refl
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
⊢ ∀ (a : J), a ∈ l → Zigzag a j₂
[PROOFSTEP]
intro i hi
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
i : J
hi : i ∈ l
⊢ Zigzag i j₂
[PROOFSTEP]
apply List.Chain.induction (fun t => Zigzag t j₂) _ hl₁ hl₂ _ _ _ (List.mem_of_mem_tail hi)
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → (fun t => Zigzag t j₂) y → (fun t => Zigzag t j₂) x
[PROOFSTEP]
intro j k
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
i : J
hi : i ∈ l
j k : J
⊢ Zag j k → (fun t => Zigzag t j₂) k → (fun t => Zigzag t j₂) j
[PROOFSTEP]
apply Relation.ReflTransGen.head
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂
[PROOFSTEP]
apply Relation.ReflTransGen.refl
[GOAL]
case h.mk.mk.intro.intro
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
⊢ ∃ l,
    List.Chain Zag { obj := j₁, property := hj₁ } l ∧
      List.getLast ({ obj := j₁, property := hj₁ } :: l) (_ : { obj := j₁, property := hj₁ } :: l ≠ []) =
        { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
refine' ⟨l.pmap f hf, _, _⟩
[GOAL]
case h.mk.mk.intro.intro.refine'_1
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
⊢ List.Chain Zag { obj := j₁, property := hj₁ } (List.pmap f l hf)
[PROOFSTEP]
refine' @List.chain_pmap_of_chain _ _ _ _ _ f (fun x y _ _ h => _) _ _ hl₁ h₁₂ _
[GOAL]
case h.mk.mk.intro.intro.refine'_1
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
x y : J
x✝¹ : Zigzag x j₂
x✝ : Zigzag y j₂
h : Zag x y
⊢ Zag (f x x✝¹) (f y x✝)
[PROOFSTEP]
exact zag_of_zag_obj (Component.ι _) h
[GOAL]
case h.mk.mk.intro.intro.refine'_2
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
⊢ List.getLast ({ obj := j₁, property := hj₁ } :: List.pmap f l hf)
      (_ : { obj := j₁, property := hj₁ } :: List.pmap f l hf ≠ []) =
    { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
erw [List.getLast_pmap _ f (j₁ :: l) (by simpa [h₁₂] using hf) (List.cons_ne_nil _ _)]
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
⊢ ∀ (a : J), a ∈ j₁ :: l → Zigzag a j₂
[PROOFSTEP]
simpa [h₁₂] using hf
[GOAL]
case h.mk.mk.intro.intro.refine'_2
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j₁ j₂ : J
hj₁ : Quotient.mk'' j₁ = Quotient.mk'' j₂
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂
f : (x : J) → Zigzag x j₂ → Component (Quotient.mk'' j₂) :=
  fun x h => { obj := x, property := (_ : Quotient.mk'' x = Quotient.mk'' j₂) }
hf : ∀ (a : J), a ∈ l → Zigzag a j₂
⊢ f (List.getLast (j₁ :: l) (_ : j₁ :: l ≠ [])) (_ : Zigzag (List.getLast (j₁ :: l) (_ : j₁ :: l ≠ [])) j₂) =
    { obj := j₂, property := (_ : Quotient.mk'' j₂ = Quotient.mk'' j₂) }
[PROOFSTEP]
exact FullSubcategory.ext _ _ hl₂
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
⊢ {X Y : Decomposed J} → ((decomposedTo J).obj X ⟶ (decomposedTo J).obj Y) → (X ⟶ Y)
[PROOFSTEP]
rintro ⟨j', X, hX⟩ ⟨k', Y, hY⟩ f
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f :
  (decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj { fst := k', snd := { obj := Y, property := hY } }
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := { obj := Y, property := hY } }
[PROOFSTEP]
dsimp at f 
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := { obj := Y, property := hY } }
[PROOFSTEP]
have : j' = k'
[GOAL]
case this
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
⊢ j' = k'
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
this : j' = k'
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := { obj := Y, property := hY } }
[PROOFSTEP]
rw [← hX, ← hY, Quotient.eq'']
[GOAL]
case this
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
⊢ Setoid.r X Y
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
this : j' = k'
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := { obj := Y, property := hY } }
[PROOFSTEP]
exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
k' : ConnectedComponents J
Y : J
hY : Quotient.mk'' Y = k'
f : X ⟶ Y
this : j' = k'
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := { obj := Y, property := hY } }
[PROOFSTEP]
subst this
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
Y : J
f : X ⟶ Y
hY : Quotient.mk'' Y = j'
⊢ { fst := j', snd := { obj := X, property := hX } } ⟶ { fst := j', snd := { obj := Y, property := hY } }
[PROOFSTEP]
exact Sigma.SigmaHom.mk f
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
⊢ ∀ {X Y : Decomposed J} (f : (decomposedTo J).obj X ⟶ (decomposedTo J).obj Y),
    (decomposedTo J).map
        (Sigma.casesOn (motive := fun x =>
          {Y : Decomposed J} → ((decomposedTo J).obj x ⟶ (decomposedTo J).obj Y) → (x ⟶ Y)) X
          (fun j' snd =>
            @FullSubcategory.casesOn J (fun k => Quotient.mk'' k = j')
              (fun x =>
                {Y : Decomposed J} →
                  ((decomposedTo J).obj { fst := j', snd := x } ⟶ (decomposedTo J).obj Y) →
                    ({ fst := j', snd := x } ⟶ Y))
              snd fun X hX {Y} =>
              Sigma.casesOn (motive := fun x =>
                ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶ (decomposedTo J).obj x) →
                  ({ fst := j', snd := { obj := X, property := hX } } ⟶ x))
                Y fun k' snd =>
                FullSubcategory.casesOn (motive := fun x =>
                  ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
                      (decomposedTo J).obj { fst := k', snd := x }) →
                    ({ fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := x }))
                  snd fun Y hY f =>
                  Eq.ndrec (motive := fun k' =>
                    (hY : Quotient.mk'' Y = k') →
                      { fst := j', snd := { obj := X, property := hX } } ⟶
                        { fst := k', snd := { obj := Y, property := hY } })
                    (fun hY => Sigma.SigmaHom.mk f) (_ : j' = k') hY)
          f) =
      f
[PROOFSTEP]
rintro ⟨j', X, hX⟩ ⟨_, Y, rfl⟩ f
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
Y : J
f :
  (decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj
      { fst := Quotient.mk'' Y, snd := { obj := Y, property := (_ : Quotient.mk'' Y = Quotient.mk'' Y) } }
⊢ (decomposedTo J).map
      (Sigma.casesOn (motive := fun x =>
        {Y : Decomposed J} → ((decomposedTo J).obj x ⟶ (decomposedTo J).obj Y) → (x ⟶ Y))
        { fst := j', snd := { obj := X, property := hX } }
        (fun j' snd =>
          @FullSubcategory.casesOn J (fun k => Quotient.mk'' k = j')
            (fun x =>
              {Y : Decomposed J} →
                ((decomposedTo J).obj { fst := j', snd := x } ⟶ (decomposedTo J).obj Y) → ({ fst := j', snd := x } ⟶ Y))
            snd fun X hX {Y} =>
            Sigma.casesOn (motive := fun x =>
              ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶ (decomposedTo J).obj x) →
                ({ fst := j', snd := { obj := X, property := hX } } ⟶ x))
              Y fun k' snd =>
              FullSubcategory.casesOn (motive := fun x =>
                ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
                    (decomposedTo J).obj { fst := k', snd := x }) →
                  ({ fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := x }))
                snd fun Y hY f =>
                Eq.ndrec (motive := fun k' =>
                  (hY : Quotient.mk'' Y = k') →
                    { fst := j', snd := { obj := X, property := hX } } ⟶
                      { fst := k', snd := { obj := Y, property := hY } })
                  (fun hY => Sigma.SigmaHom.mk f) (_ : j' = k') hY)
        f) =
    f
[PROOFSTEP]
have : Quotient.mk'' Y = j' := by
  rw [← hX, Quotient.eq'']
  exact Relation.ReflTransGen.single (Or.inr ⟨f⟩)
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
Y : J
f :
  (decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj
      { fst := Quotient.mk'' Y, snd := { obj := Y, property := (_ : Quotient.mk'' Y = Quotient.mk'' Y) } }
⊢ Quotient.mk'' Y = j'
[PROOFSTEP]
rw [← hX, Quotient.eq'']
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
Y : J
f :
  (decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj
      { fst := Quotient.mk'' Y, snd := { obj := Y, property := (_ : Quotient.mk'' Y = Quotient.mk'' Y) } }
⊢ Setoid.r Y X
[PROOFSTEP]
exact Relation.ReflTransGen.single (Or.inr ⟨f⟩)
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j' : ConnectedComponents J
X : J
hX : Quotient.mk'' X = j'
Y : J
f :
  (decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj
      { fst := Quotient.mk'' Y, snd := { obj := Y, property := (_ : Quotient.mk'' Y = Quotient.mk'' Y) } }
this : Quotient.mk'' Y = j'
⊢ (decomposedTo J).map
      (Sigma.casesOn (motive := fun x =>
        {Y : Decomposed J} → ((decomposedTo J).obj x ⟶ (decomposedTo J).obj Y) → (x ⟶ Y))
        { fst := j', snd := { obj := X, property := hX } }
        (fun j' snd =>
          @FullSubcategory.casesOn J (fun k => Quotient.mk'' k = j')
            (fun x =>
              {Y : Decomposed J} →
                ((decomposedTo J).obj { fst := j', snd := x } ⟶ (decomposedTo J).obj Y) → ({ fst := j', snd := x } ⟶ Y))
            snd fun X hX {Y} =>
            Sigma.casesOn (motive := fun x =>
              ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶ (decomposedTo J).obj x) →
                ({ fst := j', snd := { obj := X, property := hX } } ⟶ x))
              Y fun k' snd =>
              FullSubcategory.casesOn (motive := fun x =>
                ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
                    (decomposedTo J).obj { fst := k', snd := x }) →
                  ({ fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := x }))
                snd fun Y hY f =>
                Eq.ndrec (motive := fun k' =>
                  (hY : Quotient.mk'' Y = k') →
                    { fst := j', snd := { obj := X, property := hX } } ⟶
                      { fst := k', snd := { obj := Y, property := hY } })
                  (fun hY => Sigma.SigmaHom.mk f) (_ : j' = k') hY)
        f) =
    f
[PROOFSTEP]
subst this
[GOAL]
case mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
X Y : J
hX : Quotient.mk'' X = Quotient.mk'' Y
f :
  (decomposedTo J).obj { fst := Quotient.mk'' Y, snd := { obj := X, property := hX } } ⟶
    (decomposedTo J).obj
      { fst := Quotient.mk'' Y, snd := { obj := Y, property := (_ : Quotient.mk'' Y = Quotient.mk'' Y) } }
⊢ (decomposedTo J).map
      (Sigma.casesOn (motive := fun x =>
        {Y : Decomposed J} → ((decomposedTo J).obj x ⟶ (decomposedTo J).obj Y) → (x ⟶ Y))
        { fst := Quotient.mk'' Y, snd := { obj := X, property := hX } }
        (fun j' snd =>
          @FullSubcategory.casesOn J (fun k => Quotient.mk'' k = j')
            (fun x =>
              {Y : Decomposed J} →
                ((decomposedTo J).obj { fst := j', snd := x } ⟶ (decomposedTo J).obj Y) → ({ fst := j', snd := x } ⟶ Y))
            snd fun X hX {Y} =>
            Sigma.casesOn (motive := fun x =>
              ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶ (decomposedTo J).obj x) →
                ({ fst := j', snd := { obj := X, property := hX } } ⟶ x))
              Y fun k' snd =>
              FullSubcategory.casesOn (motive := fun x =>
                ((decomposedTo J).obj { fst := j', snd := { obj := X, property := hX } } ⟶
                    (decomposedTo J).obj { fst := k', snd := x }) →
                  ({ fst := j', snd := { obj := X, property := hX } } ⟶ { fst := k', snd := x }))
                snd fun Y hY f =>
                Eq.ndrec (motive := fun k' =>
                  (hY : Quotient.mk'' Y = k') →
                    { fst := j', snd := { obj := X, property := hX } } ⟶
                      { fst := k', snd := { obj := Y, property := hY } })
                  (fun hY => Sigma.SigmaHom.mk f) (_ : j' = k') hY)
        f) =
    f
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
⊢ ∀ {X Y : Decomposed J}, Function.Injective (decomposedTo J).map
[PROOFSTEP]
rintro ⟨_, j, rfl⟩ ⟨_, k, hY⟩ ⟨f⟩ ⟨_⟩ rfl
[GOAL]
case mk.mk.mk.mk.mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₂
inst✝ : Category.{u₁, u₂} C
j k : J
hY : Quotient.mk'' k = Quotient.mk'' j
f : { obj := j, property := (_ : Quotient.mk'' j = Quotient.mk'' j) } ⟶ { obj := k, property := hY }
⊢ Sigma.SigmaHom.mk f = Sigma.SigmaHom.mk ((decomposedTo J).map (Sigma.SigmaHom.mk f))
[PROOFSTEP]
rfl
