[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]
