[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv
[PROOFSTEP]
rw [Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = (α.inv ≫ α.hom) ≫ β.inv
[PROOFSTEP]
rw [Category.assoc, ← w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ (α.inv ≫ α.hom) ≫ β.inv = β.inv
[PROOFSTEP]
rw [Iso.inv_hom_id, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
this : α.inv = β.inv
⊢ α = β
[PROOFSTEP]
cases α
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
β : X ≅ Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝ inv✝).hom = β.hom
this : (mk hom✝ inv✝).inv = β.inv
⊢ mk hom✝ inv✝ = β
[PROOFSTEP]
cases β
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
hom✝¹ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝¹ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝¹ = 𝟙 Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝¹ inv✝¹).hom = (mk hom✝ inv✝).hom
this : (mk hom✝¹ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝¹ inv✝¹ = mk hom✝ inv✝
[PROOFSTEP]
cases w
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
hom✝ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝ = 𝟙 Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
this : (mk hom✝ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝ inv✝¹ = mk hom✝ inv✝
[PROOFSTEP]
cases this
[GOAL]
case mk.mk.refl.refl
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝¹ : inv✝ ≫ hom✝ = 𝟙 Y
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ mk hom✝ inv✝ = mk hom✝ inv✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
α : X ≅ Y
⊢ α.symm.symm = α
[PROOFSTEP]
cases α
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ (mk hom✝ inv✝).symm.symm = mk hom✝ inv✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
[PROOFSTEP]
simp only [trans_hom, Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
⊢ refl X ≪≫ α = α
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
[PROOFSTEP]
apply Category.id_comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
⊢ α ≪≫ refl Y = α
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ α.symm ≪≫ α ≪≫ β = β
[PROOFSTEP]
rw [← trans_assoc, symm_self_id, refl_trans]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β
[PROOFSTEP]
rw [← trans_assoc, self_symm_id, refl_trans]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : α.inv ≫ f = g
⊢ f = α.hom ≫ g
[PROOFSTEP]
simp [H.symm]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : f = α.hom ≫ g
⊢ α.inv ≫ f = g
[PROOFSTEP]
simp [H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f ≫ α.inv = g
⊢ f = g ≫ α.hom
[PROOFSTEP]
simp [H.symm]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f = g ≫ α.hom
⊢ f ≫ α.inv = g
[PROOFSTEP]
simp [H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ g✝ : X ≅ Y
X✝ Y✝ : C
f g : X✝ ≅ Y✝
h : f.hom = g.hom
⊢ f.inv = g.inv
[PROOFSTEP]
rw [ext h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Y ⟶ X
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv
[PROOFSTEP]
rw [← eq_inv_comp, comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Y ⟶ X
⊢ f ≫ α.hom = 𝟙 Y ↔ f = α.inv
[PROOFSTEP]
rw [← eq_comp_inv, id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv
[PROOFSTEP]
erw [inv_eq_inv α.symm β, eq_comm]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z✝ : C
f : X ⟶ Y
I : IsIso f
Z : C
g : X ⟶ Z
⊢ f ≫ inv f ≫ g = g
[PROOFSTEP]
simp [← Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z✝ : C
f : X ⟶ Y
I : IsIso f
Z : C
g : Y ⟶ Z
⊢ inv f ≫ f ≫ g = g
[PROOFSTEP]
simp [← Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
rw [← Category.comp_id g, ← Category.comp_id h, ← IsIso.hom_inv_id f, ← Category.assoc, w, ← Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ inv f = g
[PROOFSTEP]
apply (cancel_epi f).mp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ f ≫ inv f = f ≫ g
[PROOFSTEP]
simp [hom_inv_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
inv_hom_id : g ≫ f = 𝟙 Y
⊢ inv f = g
[PROOFSTEP]
apply (cancel_mono f).mp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
inv_hom_id : g ≫ f = 𝟙 Y
⊢ inv f ≫ f = g ≫ f
[PROOFSTEP]
simp [inv_hom_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X ∧ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ≅ Y
⊢ f.hom ≫ f.inv = 𝟙 X ∧ f.inv ≫ f.hom = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ inv (𝟙 X) = 𝟙 X
[PROOFSTEP]
apply inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ inv (f ≫ h) = inv h ≫ inv f
[PROOFSTEP]
apply inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (inv f) = f
[PROOFSTEP]
apply inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ g : X ⟶ Y
h : Y ⟶ Z
f : X ≅ Y
⊢ inv f.inv = f.hom
[PROOFSTEP]
apply inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ g : X ⟶ Y
h : Y ⟶ Z
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ g : X ⟶ Y
h : Y ⟶ Z
f : X ≅ Y
⊢ inv f.hom = f.inv
[PROOFSTEP]
apply inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ g : X ⟶ Y
h : Y ⟶ Z
f : X ≅ Y
⊢ f.hom ≫ f.inv = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso g
[PROOFSTEP]
rw [← id_comp g, ← inv_hom_id f, assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso g
inst✝ : IsIso (f ≫ g)
⊢ IsIso f
[PROOFSTEP]
rw [← comp_id f, ← hom_inv_id g, ← assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso g
inst✝ : IsIso (f ≫ g)
⊢ IsIso ((f ≫ g) ≫ inv g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso h
w : f ≫ g = h
⊢ IsIso g
[PROOFSTEP]
rw [← w] at hh
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g
[PROOFSTEP]
haveI := hh
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso g
[PROOFSTEP]
exact of_isIso_comp_left f g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso h
w : f ≫ g = h
⊢ IsIso f
[PROOFSTEP]
rw [← w] at hh
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso f
[PROOFSTEP]
haveI := hh
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso f
[PROOFSTEP]
exact of_isIso_comp_right f g
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ f = g
[PROOFSTEP]
apply (cancel_epi (inv f)).1
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ inv f ≫ f = inv f ≫ g
[PROOFSTEP]
erw [inv_hom_id, p, inv_hom_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso f
[PROOFSTEP]
rw [(hom_comp_eq_id _).mp h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso f
[PROOFSTEP]
rw [(comp_hom_eq_id _).mp h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso (inv g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ≅ Y
g g' : Y ⟶ Z
⊢ f.hom ≫ g = f.hom ≫ g' ↔ g = g'
[PROOFSTEP]
simp only [cancel_epi]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : Y ≅ X
g g' : Y ⟶ Z
⊢ f.inv ≫ g = f.inv ≫ g' ↔ g = g'
[PROOFSTEP]
simp only [cancel_epi]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f f' : X ⟶ Y
g : Y ≅ Z
⊢ f ≫ g.hom = f' ≫ g.hom ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f f' : X ⟶ Y
g : Z ≅ Y
⊢ f ≫ g.inv = f' ≫ g.inv ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Y ≅ Z
⊢ f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Z ≅ Y
⊢ f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
i : X ≅ Y
⊢ F.map i.hom ≫ F.map i.inv = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← map_comp, Iso.hom_inv_id, ← map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
i : X ≅ Y
⊢ F.map i.inv ≫ F.map i.hom = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← map_comp, Iso.inv_hom_id, ← map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
[PROOFSTEP]
apply Functor.map_comp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) = inv (F.map f)
[PROOFSTEP]
apply eq_inv_of_hom_inv_id
[GOAL]
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y)
[PROOFSTEP]
simp


[GOAL]
w : EssSurj uliftFunctor.{u, v}
a : Type (max u v)
⊢ Small.{v, max u v} a
[PROOFSTEP]
obtain ⟨a', ⟨m⟩⟩ := w.mem_essImage a
[GOAL]
case intro.intro
w : EssSurj uliftFunctor.{u, v}
a : Type (max u v)
a' : Type v
m : uliftFunctor.{u, v}.obj a' ≅ a
⊢ Small.{v, max u v} a
[PROOFSTEP]
exact ⟨a', ⟨(Iso.toEquiv m).symm.trans Equiv.ulift⟩⟩