[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Over X
f g : U ⟶ V
h : f.left = g.left
⊢ f = g
[PROOFSTEP]
let ⟨_, b, _⟩ := f
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : (CommaMorphism.mk left✝ b).left = g.left
⊢ CommaMorphism.mk left✝ b = g
[PROOFSTEP]
let ⟨_, e, _⟩ := g
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ CommaMorphism.mk left✝¹ b = CommaMorphism.mk left✝ e
[PROOFSTEP]
congr
[GOAL]
case e_right
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ b = e
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Over X
⊢ U.right = { as := PUnit.unit }
[PROOFSTEP]
simp only
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Over X
f : A ⟶ B
⊢ f.left ≫ B.hom = A.hom
[PROOFSTEP]
have := f.w
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Over X
f : A ⟶ B
this : (𝟭 T).map f.left ≫ B.hom = A.hom ≫ (Functor.fromPUnit X).map f.right
⊢ f.left ≫ B.hom = A.hom
[PROOFSTEP]
aesop_cat
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
⊢ IsIso f
[PROOFSTEP]
let g : Z ⟶ Y := Over.homMk (inv ((forget X).map f)) ((asIso ((forget X).map f)).inv_comp_eq.2 (Over.w f).symm)
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ IsIso f
[PROOFSTEP]
dsimp [forget] at t 
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ IsIso f
[PROOFSTEP]
refine ⟨⟨g, ⟨?_, ?_⟩⟩⟩
[GOAL]
case refine_1
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ f ≫ g = 𝟙 Y
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
repeat (ext; simp)
[GOAL]
case refine_1
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ f ≫ g = 𝟙 Y
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
ext
[GOAL]
case refine_1.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ (f ≫ g).left = (𝟙 Y).left
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
ext
[GOAL]
case refine_2.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Over X
f : Y ⟶ Z
t : IsIso f.left
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ (g ≫ f).left = (𝟙 Z).left
[PROOFSTEP]
simp
[GOAL]

[PROOFSTEP]
ext
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
⊢ Mono k.left
[PROOFSTEP]
refine' ⟨fun {Y : T} l m a => _⟩
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
⊢ l = m
[PROOFSTEP]
let l' : mk (m ≫ f.hom) ⟶ f :=
  homMk l (by dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc])
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
⊢ l ≫ f.hom = (mk (m ≫ f.hom)).hom
[PROOFSTEP]
dsimp
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
⊢ l ≫ f.hom = m ≫ f.hom
[PROOFSTEP]
rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc]
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
l' : mk (m ≫ f.hom) ⟶ f := homMk l
⊢ l = m
[PROOFSTEP]
suffices l' = (homMk m : mk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left this
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
l' : mk (m ≫ f.hom) ⟶ f := homMk l
this : l' = homMk m
⊢ l = m
[PROOFSTEP]
apply congrArg CommaMorphism.left this
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
l' : mk (m ≫ f.hom) ⟶ f := homMk l
⊢ l' = homMk m
[PROOFSTEP]
rw [← cancel_mono k]
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
l' : mk (m ≫ f.hom) ⟶ f := homMk l
⊢ l' ≫ k = homMk m ≫ k
[PROOFSTEP]
ext
[GOAL]
case h
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ k.left = m ≫ k.left
l' : mk (m ≫ f.hom) ⟶ f := homMk l
⊢ (l' ≫ k).left = (homMk m ≫ k).left
[PROOFSTEP]
apply a
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ κ.left.left ≫ ((fun α => mk α.hom.left) Y✝).hom = ((fun α => mk α.hom.left) X✝).hom
[PROOFSTEP]
dsimp
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ κ.left.left ≫ Y✝.hom.left = X✝.hom.left
[PROOFSTEP]
rw [← Over.w κ]
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ κ.left.left ≫ Y✝.hom.left = (κ.left ≫ Y✝.hom).left
[PROOFSTEP]
rfl
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
X✝ Y✝ : Over X
f : X✝ ⟶ Y✝
⊢ F.map f.left ≫ ((fun Y => mk (F.map Y.hom)) Y✝).hom = ((fun Y => mk (F.map Y.hom)) X✝).hom
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : T ⥤ D
X_1 Y : Over X
f : X_1 ⟶ Y
⊢ F.map f.left ≫ F.map Y.hom = F.map X_1.hom
[PROOFSTEP]
erw [← F.map_comp, w]
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Under X
f g : U ⟶ V
h : f.right = g.right
⊢ f = g
[PROOFSTEP]
let ⟨_, b, _⟩ := f
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : (CommaMorphism.mk left✝ b).right = g.right
⊢ CommaMorphism.mk left✝ b = g
[PROOFSTEP]
let ⟨_, e, _⟩ := g
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : (CommaMorphism.mk left✝¹ b).right = (CommaMorphism.mk left✝ e).right
⊢ CommaMorphism.mk left✝¹ b = CommaMorphism.mk left✝ e
[PROOFSTEP]
congr
[GOAL]
case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X✝ X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : (CommaMorphism.mk left✝¹ b).right = (CommaMorphism.mk left✝ e).right
⊢ left✝¹ = left✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Under X
⊢ U.left = { as := PUnit.unit }
[PROOFSTEP]
simp only
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Under X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom
[PROOFSTEP]
have := f.w
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Under X
f : A ⟶ B
this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right
⊢ A.hom ≫ f.right = B.hom
[PROOFSTEP]
aesop_cat
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
⊢ IsIso f
[PROOFSTEP]
let g : Z ⟶ Y := Under.homMk (inv ((Under.forget X).map f)) ((IsIso.comp_inv_eq _).2 (Under.w f).symm)
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ IsIso f
[PROOFSTEP]
dsimp [forget] at t 
[GOAL]
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ IsIso f
[PROOFSTEP]
refine ⟨⟨g, ⟨?_, ?_⟩⟩⟩
[GOAL]
case refine_1
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ f ≫ g = 𝟙 Y
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
repeat (ext; simp)
[GOAL]
case refine_1
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ f ≫ g = 𝟙 Y
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
ext
[GOAL]
case refine_1.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ (f ≫ g).right = (𝟙 Y).right
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
case refine_2
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ g ≫ f = 𝟙 Z
[PROOFSTEP]
ext
[GOAL]
case refine_2.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y Z : Under X
f : Y ⟶ Z
t : IsIso f.right
g : Z ⟶ Y := homMk (inv ((forget X).map f))
⊢ (g ≫ f).right = (𝟙 Z).right
[PROOFSTEP]
simp
[GOAL]

[PROOFSTEP]
ext
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
⊢ Epi k.right
[PROOFSTEP]
refine' ⟨fun {Y : T} l m a => _⟩
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
⊢ l = m
[PROOFSTEP]
let l' : g ⟶ mk (g.hom ≫ m) :=
  homMk l
    (by dsimp; rw [← Under.w k, Category.assoc, a, Category.assoc])
      -- Porting note: add type ascription here to `homMk m`
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
⊢ g.hom ≫ l = (mk (g.hom ≫ m)).hom
[PROOFSTEP]
dsimp
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
[PROOFSTEP]
rw [← Under.w k, Category.assoc, a, Category.assoc]
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l
⊢ l = m
[PROOFSTEP]
suffices l' = (homMk m : g ⟶ mk (g.hom ≫ m)) by apply congrArg CommaMorphism.right this
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l
this : l' = homMk m
⊢ l = m
[PROOFSTEP]
apply congrArg CommaMorphism.right this
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l
⊢ l' = homMk m
[PROOFSTEP]
rw [← cancel_epi k]
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l
⊢ k ≫ l' = k ≫ homMk m
[PROOFSTEP]
ext
[GOAL]
case h
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X : T
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : k.right ≫ l = k.right ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l
⊢ (k ≫ l').right = (k ≫ homMk m).right
[PROOFSTEP]
apply a
[GOAL]
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
X✝¹ : T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
F : T ⥤ D
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ ((fun Y => mk (F.map Y.hom)) X✝).hom ≫ F.map f.right = ((fun Y => mk (F.map Y.hom)) Y✝).hom
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
T : Type u₁
inst : Category.{v₁, u₁} T
X_1 : T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
F : T ⥤ D
X_2 Y : Under X
f : X_2 ⟶ Y
⊢ F.map X_2.hom ≫ F.map f.right = F.map Y.hom
[PROOFSTEP]
erw [← F.map_comp, w]
