[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f
[PROOFSTEP]
cases f
[GOAL]
case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }
[PROOFSTEP]
rfl
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g
[PROOFSTEP]
cases h
[GOAL]
case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f
[PROOFSTEP]
rfl
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
[PROOFSTEP]
let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ (𝟭 T).map (inv ff.left) ≫ f.hom = g.hom ≫ (𝟭 T).map (inv ff.right)
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
[PROOFSTEP]
apply Exists.intro inverse
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g
[PROOFSTEP]
aesop_cat
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.left = φ₂.left
[PROOFSTEP]
rw [h]
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.right = φ₂.right
[PROOFSTEP]
rw [h]
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
have eq := Arrow.hom.congr_right e.inv_hom_id
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
rw [Arrow.comp_right, Arrow.id_right] at eq 
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
erw [Arrow.w_assoc, eq, Category.comp_id]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ ∃ inv, sq.left ≫ inv = 𝟙 f.left ∧ inv ≫ sq.left = 𝟙 g.left
[PROOFSTEP]
apply Exists.intro (inv sq).left
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ (inv sq).left = 𝟙 f.left ∧ (inv sq).left ≫ sq.left = 𝟙 g.left
[PROOFSTEP]
simp only [← Comma.comp_left, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_left, eq_self_iff_true, and_self_iff]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (𝟙 f).left = 𝟙 f.left ∧ (𝟙 g).left = 𝟙 g.left
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ ∃ inv, sq.right ≫ inv = 𝟙 f.right ∧ inv ≫ sq.right = 𝟙 g.right
[PROOFSTEP]
apply Exists.intro (inv sq).right
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.right ≫ (inv sq).right = 𝟙 f.right ∧ (inv sq).right ≫ sq.right = 𝟙 g.right
[PROOFSTEP]
simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_right, eq_self_iff_true, and_self_iff]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (𝟙 f).right = 𝟙 f.right ∧ (𝟙 g).right = 𝟙 g.right
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ (inv sq).left = 𝟙 f.left
[PROOFSTEP]
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.right ≫ (inv sq).right = 𝟙 f.right
[PROOFSTEP]
rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ g.hom ≫ inv sq.right = f.hom
[PROOFSTEP]
simp only [← Category.assoc, IsIso.comp_inv_eq, w]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ inv sq.left ≫ f.hom ≫ sq.right = g.hom
[PROOFSTEP]
simp only [w, IsIso.inv_comp_eq]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
⊢ φ = ψ
[PROOFSTEP]
let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
  { left := φ
    right := φ ≫ f.hom }
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
⊢ φ = ψ
[PROOFSTEP]
have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g✝ : Arrow T
sq : f ⟶ g✝
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
g : Z ⟶ f.left
⊢ (aux g).right = g ≫ f.hom
[PROOFSTEP]
dsimp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ = ψ
[PROOFSTEP]
show (aux φ).left = (aux ψ).left
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ).left = (aux ψ).left
[PROOFSTEP]
congr 1
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ aux φ = aux ψ
[PROOFSTEP]
rw [← cancel_mono sq]
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ aux φ ≫ sq = aux ψ ≫ sq
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case e_self.left
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ ≫ sq).left = (aux ψ ≫ sq).left
[PROOFSTEP]
exact h
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ ≫ sq).right = (aux ψ ≫ sq).right
[PROOFSTEP]
rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ ≫ f.hom ≫ sq.right = ψ ≫ f.hom ≫ sq.right
[PROOFSTEP]
rw [← Arrow.w]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ ≫ sq.left ≫ g.hom = ψ ≫ sq.left ≫ g.hom
[PROOFSTEP]
simp only [← Category.assoc, h]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
⊢ φ = ψ
[PROOFSTEP]
let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
  { right := φ
    left := g.hom ≫ φ }
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ φ = ψ
[PROOFSTEP]
show (aux φ).right = (aux ψ).right
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (aux φ).right = (aux ψ).right
[PROOFSTEP]
congr 1
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ aux φ = aux ψ
[PROOFSTEP]
rw [← cancel_epi sq]
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ sq ≫ aux φ = sq ≫ aux ψ
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case e_self.left
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (sq ≫ aux φ).left = (sq ≫ aux ψ).left
[PROOFSTEP]
rw [Comma.comp_left, Comma.comp_left, Arrow.w_assoc, Arrow.w_assoc, h]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (sq ≫ aux φ).right = (sq ≫ aux ψ).right
[PROOFSTEP]
exact h
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
i : Arrow T
X Y : T
p : X ≅ Y
sq : i ⟶ mk p.hom
⊢ i.hom ≫ sq.right ≫ p.inv = sq.left
[PROOFSTEP]
simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ sq.left ≫ p.hom = sq.right
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom]
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
let w := f.w
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : (𝟭 C).map f.left ≫ Y✝.hom = X✝.hom ≫ (𝟭 C).map f.right := f.w
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
simp only [id_map] at w 
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
dsimp
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w
⊢ F.map f.left ≫ F.map Y✝.hom = F.map X✝.hom ≫ F.map f.right
[PROOFSTEP]
simp only [← F.map_comp, w]
