[GOAL]
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : ↑X), f x = g x
⊢ f = g
[PROOFSTEP]
funext
[GOAL]
case h
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : ↑X), f x = g x
x✝ : ↑X
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h
[GOAL]
A B : FintypeCat
⊢ Function.LeftInverse
    (fun i =>
      { toFun := i.hom, invFun := i.inv, left_inv := (_ : ∀ (a : ↑A), i.inv (i.hom a) = a),
        right_inv := (_ : ∀ (a : ↑B), i.hom (i.inv a) = a) })
    fun e => Iso.mk ↑e ↑e.symm
[PROOFSTEP]
aesop_cat
[GOAL]
A B : FintypeCat
⊢ Function.RightInverse
    (fun i =>
      { toFun := i.hom, invFun := i.inv, left_inv := (_ : ∀ (a : ↑A), i.inv (i.hom a) = a),
        right_inv := (_ : ∀ (a : ↑B), i.hom (i.inv a) = a) })
    fun e => Iso.mk ↑e ↑e.symm
[PROOFSTEP]
aesop_cat
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.LeftInverse (fun x => (h.inv { down := x }).down) fun x => (h.hom { down := x }).down
[PROOFSTEP]
intro a
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (fun x => (h.inv { down := x }).down) ((fun x => (h.hom { down := x }).down) a) = a
[PROOFSTEP]
change ULift.down _ = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv { down := (fun x => (h.hom { down := x }).down) a }).down = a
[PROOFSTEP]
rw [ULift.up_down]
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv (h.hom { down := a })).down = a
[PROOFSTEP]
change ((h.hom ≫ h.inv) _).down = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ ((h.hom ≫ h.inv) { down := a }).down = a
[PROOFSTEP]
simp
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (𝟙 X { down := a }).down = a
[PROOFSTEP]
rfl
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.RightInverse (fun x => (h.inv { down := x }).down) fun x => (h.hom { down := x }).down
[PROOFSTEP]
intro a
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (fun x => (h.hom { down := x }).down) ((fun x => (h.inv { down := x }).down) a) = a
[PROOFSTEP]
change ULift.down _ = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom { down := (fun x => (h.inv { down := x }).down) a }).down = a
[PROOFSTEP]
rw [ULift.up_down]
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom (h.inv { down := a })).down = a
[PROOFSTEP]
change ((h.inv ≫ h.hom) _).down = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ ((h.inv ≫ h.hom) { down := a }).down = a
[PROOFSTEP]
simp
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (𝟙 Y { down := a }).down = a
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = n
[PROOFSTEP]
convert Finset.card_fin n
[GOAL]
case h.e'_2
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = Finset.card Finset.univ
[PROOFSTEP]
apply Fintype.ofEquiv_card
[GOAL]
⊢ IsEquivalence Skeleton.incl
[PROOFSTEP]
infer_instance


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


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono (hT.from A)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f ≫ IsTerminal.from hT A = g ≫ IsTerminal.from hT A
[PROOFSTEP]
apply hT.hom_ext
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono (terminal.from A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ diag A ≫ prod.fst = 𝟙 A
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
[PROOFSTEP]
rw [IsSubterminal.def] at hA
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ prod.fst = prod.snd
[PROOFSTEP]
simp [← cancel_epi (diag A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ f = g
[PROOFSTEP]
rw [← prod.lift_fst f g, this, prod.lift_snd]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ A ⨯ A ≅ A
[PROOFSTEP]
letI := IsSubterminal.isIso_diag hA
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
this : IsIso (diag A) := isIso_diag hA
⊢ A ⨯ A ≅ A
[PROOFSTEP]
apply (asIso (diag A)).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X✝ Y✝ : Subterminals C
f : X✝ ⟶ Y✝
⊢ f ≫
      MonoOver.arrow
        ((fun X => { obj := Over.mk (terminal.from X.obj), property := (_ : Mono (terminal.from X.obj)) }) Y✝) =
    MonoOver.arrow
      ((fun X => { obj := Over.mk (terminal.from X.obj), property := (_ : Mono (terminal.from X.obj)) }) X✝)
[PROOFSTEP]
ext1 ⟨⟨⟩⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X : MonoOver (⊤_ C)
Z : C
f g : Z ⟶ X.obj.left
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono X.arrow]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X : MonoOver (⊤_ C)
Z : C
f g : Z ⟶ X.obj.left
⊢ f ≫ MonoOver.arrow X = g ≫ MonoOver.arrow X
[PROOFSTEP]
apply Subsingleton.elim