[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ NatTrans.app α.hom X ≫ NatTrans.app α.inv X = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.hom_inv_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ NatTrans.app (𝟙 F) X = 𝟙 (F.obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ NatTrans.app α.inv X ≫ NatTrans.app α.hom X = 𝟙 (G.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.inv_hom_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ NatTrans.app (𝟙 G) X = 𝟙 (G.obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ app α.hom X ≫ app α.inv X = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.hom_inv_id, ← id_app]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ app α.inv X ≫ app α.hom X = 𝟙 (G.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.inv_hom_id, ← id_app]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ app α.inv X ≫ app α.hom X = 𝟙 (G.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.inv_hom_id, ← id_app]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
⊢ app α.hom X ≫ app α.inv X = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← comp_app, Iso.hom_inv_id, ← id_app]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
Z : D
g g' : G.obj X ⟶ Z
⊢ app α.hom X ≫ g = app α.hom X ≫ g' ↔ g = g'
[PROOFSTEP]
simp only [cancel_epi, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : C
Z : D
g g' : F.obj X ⟶ Z
⊢ app α.inv X ≫ g = app α.inv X ≫ g' ↔ g = g'
[PROOFSTEP]
simp only [cancel_epi, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : D
Y : C
f f' : X ⟶ F.obj Y
⊢ f ≫ app α.hom Y = f' ≫ app α.hom Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
X : D
Y : C
f f' : X ⟶ G.obj Y
⊢ f ≫ app α.inv Y = f' ≫ app α.inv Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ F.obj Y
f' : W ⟶ X'
g' : X' ⟶ F.obj Y
⊢ f ≫ g ≫ app α.hom Y = f' ≫ g' ≫ app α.hom Y ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ G.obj Y
f' : W ⟶ X'
g' : X' ⟶ G.obj Y
⊢ f ≫ g ≫ app α.inv Y = f' ≫ g' ≫ app α.inv Y ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono, refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
α : F✝ ≅ G✝
F G : C ⥤ D
e : F ≅ G
X : C
⊢ inv (app e.inv X) = app e.hom X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ app α.inv X ≫ F.map f ≫ app α.hom Y = G.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ app α.hom X ≫ G.map f ≫ app α.inv Y = F.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (app α X)
⊢ inv (app α X) ≫ F.map f ≫ app α Y = G.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (app α Y)
⊢ app α X ≫ G.map f ≫ inv (app α Y) = F.map f
[PROOFSTEP]
rw [← Category.assoc, ← naturality, Category.assoc, IsIso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ app (inv α) X = inv (app α X)
[PROOFSTEP]
apply IsIso.eq_inv_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ app α X ≫ app (inv α) X = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← NatTrans.comp_app]
[GOAL]
case hom_inv_id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ app (α ≫ inv α) X = 𝟙 (F.obj X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G : C ⥤ D
X✝ Y✝ : C
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ inv (app (F.map e.inv) Z) = app (F.map e.hom) Z
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
[PROOFSTEP]
have h := congr_arg (fun f => (app X).inv ≫ f ≫ (app Y).inv) (naturality f).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝
X Y : C
f : X ⟶ Y
h :
  (fun f => (app X).inv ≫ f ≫ (app Y).inv) ((app X).hom ≫ G.map f) =
    (fun f => (app X).inv ≫ f ≫ (app Y).inv) (F.map f ≫ (app Y).hom)
⊢ G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, Iso.hom_inv_id, assoc, comp_id, cancel_mono] at h
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝
X Y : C
f : X ⟶ Y
h : G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f
⊢ G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
[PROOFSTEP]
exact h
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y : C
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
⊢ (ofComponents app').app X = app' X
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
α : F ⟶ G
inst✝ : ∀ (X : C), IsIso (app α X)
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ ((fun X => asIso (app α X)) Y).hom = ((fun X => asIso (app α X)) X).hom ≫ G.map f
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
⊢ F ⋙ H ≅ G ⋙ I
[PROOFSTEP]
refine' ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, _, _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
⊢ (α.hom ◫ β.hom) ≫ α.inv ◫ β.inv = 𝟙 (F ⋙ H)
[PROOFSTEP]
ext
[GOAL]
case refine'_1.w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
x✝ : C
⊢ app ((α.hom ◫ β.hom) ≫ α.inv ◫ β.inv) x✝ = app (𝟙 (F ⋙ H)) x✝
[PROOFSTEP]
rw [← NatTrans.exchange]
[GOAL]
case refine'_1.w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
x✝ : C
⊢ app ((α.hom ≫ α.inv) ◫ (β.hom ≫ β.inv)) x✝ = app (𝟙 (F ⋙ H)) x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
⊢ (α.inv ◫ β.inv) ≫ α.hom ◫ β.hom = 𝟙 (G ⋙ I)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
x✝ : C
⊢ app ((α.inv ◫ β.inv) ≫ α.hom ◫ β.hom) x✝ = app (𝟙 (G ⋙ I)) x✝
[PROOFSTEP]
rw [← NatTrans.exchange]
[GOAL]
case refine'_2.w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X Y : C
F G : C ⥤ D
H I : D ⥤ E
α : F ≅ G
β : H ≅ I
x✝ : C
⊢ app ((α.inv ≫ α.hom) ◫ (β.inv ≫ β.hom)) x✝ = app (𝟙 (G ⋙ I)) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ : C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
[PROOFSTEP]
revert F₁ F₂
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
[PROOFSTEP]
suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) by
  exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
this : ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
[PROOFSTEP]
exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
[PROOFSTEP]
intro F₁ F₂ e hf
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)
[PROOFSTEP]
refine' IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, _, _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ app e.inv Y ≫ inv (F₁.map f) ≫ app e.hom X = 𝟙 (F₂.obj X)
[PROOFSTEP]
simp only [NatTrans.naturality_assoc, IsIso.hom_inv_id_assoc, Iso.inv_hom_id_app]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ (app e.inv Y ≫ inv (F₁.map f) ≫ app e.hom X) ≫ F₂.map f = 𝟙 (F₂.obj Y)
[PROOFSTEP]
simp only [assoc, ← e.hom.naturality, IsIso.inv_hom_id_assoc, Iso.inv_hom_id_app]


[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


[GOAL]
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
⊢ hInv (Equivalence.symm T) R L (Equivalence.symm B) (hInv T L R B h) = h
[PROOFSTEP]
ext X
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ NatTrans.app iso'.hom X = NatTrans.app iso'.hom X
[PROOFSTEP]
erw [← cancel_mono (B.functor.map (L.map (T.unitIso.hom.app X))), ← h.iso'.hom.naturality (T.unitIso.hom.app X),
  hInv_iso'_hom_app, hInv_iso'_inv_app]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (NatTrans.app (Equivalence.symm B).unitIso.hom (R.obj ((Equivalence.symm T).inverse.obj X)) ≫
        (Equivalence.symm B).inverse.map
            (B.inverse.map (R.map (NatTrans.app T.counitIso.inv ((Equivalence.symm T).inverse.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (iso T.functor L R B.functor).hom
                    (T.inverse.obj ((Equivalence.symm T).inverse.obj X))) ≫
                NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj ((Equivalence.symm T).inverse.obj X)))) ≫
          (Equivalence.symm B).inverse.map (L.map (NatTrans.app (Equivalence.symm T).counitIso.hom X))) ≫
      B.functor.map (L.map (NatTrans.app T.unitIso.hom X)) =
    (T.functor ⋙ R).map (NatTrans.app T.unitIso.hom X) ≫ NatTrans.app iso'.hom ((T.functor ⋙ T.inverse).obj X)
[PROOFSTEP]
dsimp
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (NatTrans.app B.counitIso.inv (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (NatTrans.app T.counitIso.inv (T.functor.obj X))) ≫
              B.inverse.map (NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X))) ≫
                NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (NatTrans.app T.unitIso.inv X))) ≫
      B.functor.map (L.map (NatTrans.app T.unitIso.hom X)) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Equivalence.counitInv_app_functor,
  Functor.map_id]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ NatTrans.app B.counitIso.inv (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (NatTrans.app (Equivalence.unit T) X))) ≫
          B.inverse.map (NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X))) ≫
            NatTrans.app B.unitIso.inv (L.obj (T.inverse.obj (T.functor.obj X))) ≫
              𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
simp only [Functor.map_comp, Equivalence.fun_inv_map, assoc, Equivalence.counitInv_functor_comp, comp_id,
  Iso.inv_hom_id_app_assoc]
[GOAL]
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₅ : Type u_5
C₆ : Type u_6
inst✝⁵ : Category.{u_8, u_1} C₁
inst✝⁴ : Category.{u_9, u_2} C₂
inst✝³ : Category.{u_10, u_3} C₃
inst✝² : Category.{u_7, u_4} C₄
inst✝¹ : Category.{?u.18727, u_5} C₅
inst✝ : Category.{?u.18731, u_6} C₆
T✝ : C₁ ⥤ C₂
L✝ : C₁ ⥤ C₃
R✝ : C₂ ⥤ C₄
B✝ : C₃ ⥤ C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ R.map (T.functor.map (NatTrans.app (Equivalence.unit T) X)) ≫
      NatTrans.app (iso T.functor L R B.functor).hom (T.inverse.obj (T.functor.obj X)) =
    R.map (T.functor.map (NatTrans.app T.unitIso.hom X)) ≫ NatTrans.app iso'.hom (T.inverse.obj (T.functor.obj X))
[PROOFSTEP]
rfl