[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
[PROOFSTEP]
rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
[PROOFSTEP]
rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ ↑(homCongr α β) f = α.inv ≫ f ≫ β.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ ↑(homCongr α γ) (f ≫ g) = ↑(homCongr α β) f ≫ ↑(homCongr β γ) g
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ↑(homCongr (refl X) (refl Y)) f = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ↑(homCongr (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)) f = ↑((homCongr α₁ β₁).trans (homCongr α₂ β₂)) f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ ↑(conj (refl X)) f = f
[PROOFSTEP]
rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ ↑(conj α.symm) (↑(conj α) f) = f
[PROOFSTEP]
rw [← trans_conj, α.self_symm_id, refl_conj]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
⊢ ↑(conjAut α) f = α.symm ≪≫ f ≪≫ α
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : Aut X
⊢ ↑(conjAut (α ≪≫ β)) f = ↑(conjAut β) (↑(conjAut α) f)
[PROOFSTEP]
simp only [conjAut_apply, Iso.trans_symm, Iso.trans_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map (↑(Iso.homCongr α β) f) = ↑(Iso.homCongr (F.mapIso α) (F.mapIso β)) (F.map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F✝ F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (↑(Iso.conjAut α) f) = ↑(Iso.conjAut (F.mapIso α)) (F.mapIso f)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F✝ F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (↑(Iso.conjAut α) f)).hom = (↑(Iso.conjAut (F.mapIso α)) (F.mapIso f)).hom
[PROOFSTEP]
simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]