awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (Functor.fromPUnit X) left ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) b
h : Hom.right { left := left, right := b, w := w : CommaMorphism U V } = Hom.right g
let :
  ∀ (left_1 : U.left ⟶ V.left) (e : U.right ⟶ V.right)
    (w_1 : Functor.map (Functor.fromPUnit X) left_1 ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) e)
    (h :
      Hom.right { left := left, right := b, w := w : CommaMorphism U V } =
        Hom.right { left := left_1, right := e, w := w_1 }),
    { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }
⊢ { left := left, right := b, w := w : CommaMorphism U V } = g

Tactic:
let ⟨_,e,_⟩ := g
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (Functor.fromPUnit X) left ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) b
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (Functor.fromPUnit X) left_1 ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) e
h :
  Hom.right { left := left, right := b, w := w : CommaMorphism U V } =
    Hom.right { left := left_1, right := e, w := w_1 }
e_left : left = left_1
⊢ { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (Functor.fromPUnit X) left ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) b
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (Functor.fromPUnit X) left_1 ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) e
h :
  Hom.right { left := left, right := b, w := w : CommaMorphism U V } =
    Hom.right { left := left_1, right := e, w := w_1 }
⊢ left = left_1

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U : Under.{v₁, u₁} X
⊢ U.left = { as := PUnit.unit }

Tactic:
simp only
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U : Under.{v₁, u₁} X
⊢ Hom.right (𝟙 U) = 𝟙 U.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
a b c : Under.{v₁, u₁} X
f : a ⟶ b
g : b ⟶ c
⊢ Hom.right (f ≫ g) = Hom.right f ≫ Hom.right g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f : U ⟶ V
h : U.hom ≫ Hom.right f = V.hom
⊢ homMk (Hom.right f) h = f

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Under.homMk, CategoryTheory.Under.Hom, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
U V W : Under.{v₁, u₁} X
f : U.right ⟶ V.right
g : V.right ⟶ W.right
w_f : U.hom ≫ f = V.hom
w_g : V.hom ≫ g = W.hom
⊢ U.hom ≫ f ≫ g = W.hom

Tactic:
simp only [reassoc_of% w_f, w_g]
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V W : Under.{v₁, u₁} X
f : U.right ⟶ V.right
g : V.right ⟶ W.right
w_f : U.hom ≫ f = V.hom
w_g : V.hom ≫ g = W.hom
⊢ homMk (f ≫ g) ⋯ = homMk f w_f ≫ homMk g w_g

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Under.homMk, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
h : f = g
rw rw₁ : g.right = g.right
⊢ f.right = g.right

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
h : f = g
subst : Hom.right (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f : Under.{v₁, u₁} X
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
e : f ≅ g
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right

Tactic:
simp [← Under.comp_right]

Premises used: CategoryTheory.Under.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
e : f ≅ g
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right

Tactic:
simp [← Under.comp_right]

Premises used: CategoryTheory.Under.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
P : Under.{v₁, u₁} X → Prop
⊢ (∀ (Y : Under.{v₁, u₁} X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (mk f)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
S : T
X : Under.{v₁, u₁} S
⊢ ∃ (Y : T) (f : S ⟶ Y), mk f = X

Tactic:
⟨_, X.hom, rfl⟩

Premises used: CategoryTheory.Under.hom, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
S : T
X Y : Under.{v₁, u₁} S
f : X ⟶ Y
⊢ ∃ (hg : X.hom ≫ Hom.right f = Y.hom), homMk (Hom.right f) ⋯ = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U : Under.{v₁, u₁} X
⊢ Functor.obj (forget X) U = U.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f : U ⟶ V
⊢ Functor.map (forget X) f = Hom.right f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
U : Under.{v₁, u₁} Y
⊢ ((map f).obj U).right = U.right

Tactic:
rfl

Premises used: CategoryTheory.Under, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
U : Under.{v₁, u₁} Y
⊢ ((map f).obj U).hom = f ≫ U.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
U V : Under.{v₁, u₁} Y
g : U ⟶ V
⊢ Hom.right ((map f).map g) = Hom.right g

Tactic:
rfl

Premises used: CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ≅ Y
⊢ (mapIso f).functor = map f.hom

Tactic:
rfl

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ≅ Y
⊢ (mapIso f).inverse = map f.inv

Tactic:
rfl

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
Y : T
f : X ⟶ Y
U V : Under.{v₁, u₁} Y
g : U ⟶ V
inst_2 : IsIso f
⊢ (map f).IsEquivalence

Tactic:
(Under.mapIso <| asIso f).isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Under.mapIso, CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
simp : { left := x.left, right := x.right, hom := x.hom : Comma.{0, v₁, v₁, 0, u₁, u₁} (Functor.fromPUnit Y) (𝟭 T) } = x
⊢ Functor.obj (map (𝟙 Y)) x = Functor.obj (𝟭 (Under.{v₁, u₁} Y)) x

Tactic:
simp [map, Comma.mapLeft]

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
⊢ { left := x.left, right := x.right, hom := x.hom : Comma.{0, v₁, v₁, 0, u₁, u₁} (Functor.fromPUnit Y) (𝟭 T) } = x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
h : Hom.right (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.right (eqToHom ⋯)
⊢ NatTrans.app (Iso.hom (mapId Y)) x = eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
⊢ Hom.right (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.right (eqToHom ⋯)

Tactic:
simp [eqToHom_right]

Premises used: CategoryTheory.Under.eqToHom_right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ map f ⋙ forget X = forget Y

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Under, CategoryTheory.Under.forget, CategoryTheory.Under.Hom, CategoryTheory.Comma.snd, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
h_obj : ∀ (X_1 : Under.{v₁, u₁} Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1
h_map :
  autoParam
    (∀ (X_1 Y_1 : Under.{v₁, u₁} Z) (f_1 : X_1 ⟶ Y_1),
      (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1
⊢ map (f ≫ g) = map g ⋙ map f

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Under.{v₁, u₁} Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1

Tactic:
simp [Under.map, Comma.mapLeft]

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under.{v₁, u₁} Z
k : U ⟶ V
h_map : Hom.right ((map (f ≫ g)).map k) = Hom.right (eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯)
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under.{v₁, u₁} Z
k : U ⟶ V
⊢ Hom.right ((map (f ≫ g)).map k) = Hom.right (eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g_1 : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g_1
X Y : T
f g : X ⟶ Y
h : f = g
A : Under.{v₁, u₁} Y
rw rw₁ : (map g).obj A = (map g).obj A
⊢ (map f).obj A = (map g).obj A

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Under.{v₁, u₁} X
rw : Hom.right (homMk Y.hom ⋯) = Y.hom
⊢ Hom.right (Limits.IsInitial.to mkIdInitial Y) = Y.hom

Tactic:
rw [mkIdInitial.hom_ext (mkIdInitial.to Y) (homMk Y.hom)]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Under.homMk, CategoryTheory.Under.mkIdInitial, CategoryTheory.Under.hom, CategoryTheory.Limits.IsInitial.to
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Under.{v₁, u₁} X
⊢ Hom.right (homMk Y.hom ⋯) = Y.hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
k : f ⟶ g
hk : Mono (Hom.right k)
⊢ Mono k

Tactic:
(forget X).mono_of_mono_map hk

Premises used: CategoryTheory.Under.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
U V : Under.{v₁, u₁} X
f : U.right ⟶ V.right
inst_2 : Mono f
w : U.hom ≫ f = V.hom
⊢ Mono (homMk f w)

Tactic:
(forget X).mono_of_mono_map ‹_›

Premises used: CategoryTheory.Under.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
k : f ⟶ g
hk : Epi (Hom.right k)
⊢ Epi k

Tactic:
(forget X).epi_of_epi_map hk

Premises used: CategoryTheory.Under.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
U V : Under.{v₁, u₁} X
f : U.right ⟶ V.right
inst_2 : Epi f
w : U.hom ≫ f = V.hom
⊢ Epi (homMk f w)

Tactic:
(forget X).epi_of_epi_map ‹_›

Premises used: CategoryTheory.Under.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
⊢ Epi (Hom.right k)

Tactic:
⟨fun {Y : T} l m a => ?_⟩

Premises used: CategoryTheory.Epi.mk
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
refine : ∀ {Y : T} (l m : g.right ⟶ Y) (a : Hom.right k ≫ l = Hom.right k ≫ m), l = m
⊢ Epi (Hom.right k)

Tactic:
refine ⟨fun {Y : T} l m a => ?_⟩
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
dsimp : g.hom ≫ l = g.hom ≫ m
⊢ g.hom ≫ l = (mk (g.hom ≫ m)).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
rw : (f.hom ≫ Hom.right k) ≫ l = (f.hom ≫ Hom.right k) ≫ m
rw₁ : f.hom ≫ Hom.right k ≫ l = (f.hom ≫ Hom.right k) ≫ m
rw₂ : f.hom ≫ Hom.right k ≫ m = (f.hom ≫ Hom.right k) ≫ m
rw₃ rw₄ : f.hom ≫ Hom.right k ≫ m = f.hom ≫ Hom.right k ≫ m
⊢ g.hom ≫ l = g.hom ≫ m

Tactic:
rw [← Under.w k, Category.assoc, a, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
this : l' = homMk m ⋯
⊢ l = m

Tactic:
apply congrArg CommaMorphism.right this

Premises used: congrArg, CategoryTheory.CommaMorphism.right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
suffices : l' = homMk m ⋯
⊢ l = m

Tactic:
suffices l' = (homMk m) by apply congrArg CommaMorphism.right this
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
rw : k ≫ l' = k ≫ homMk m ⋯
⊢ l' = homMk m ⋯

Tactic:
rw [← cancel_epi k]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
h : Hom.right (k ≫ l') = Hom.right (k ≫ homMk m ⋯)
⊢ k ≫ l' = k ≫ homMk m ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ Hom.right (k ≫ l') = Hom.right (k ≫ homMk m ⋯)

Tactic:
apply a
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
X_2 Y : Under.{v₁, u₁} X
f : X_2 ⟶ Y
⊢ (mk (F.map X_2.hom)).hom ≫ F.map (Hom.right f) = (mk (F.map Y.hom)).hom

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
⊢ Eq (α := Under.{v₁, u₁} X ⥤ Under.{v_1, u_1} ((F ⋙ G).obj X)) (post (F ⋙ G)) (post F ⋙ post G)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Under.homMk, CategoryTheory.Functor.comp, CategoryTheory.Under.mk, CategoryTheory.StructuredArrow.mk, CategoryTheory.Under.post, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} T D
X : T
⊢ post F ⋙ forget (F.obj X) = forget X ⋙ F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Under.mk, CategoryTheory.Under, CategoryTheory.Under.forget, CategoryTheory.StructuredArrow.mk, CategoryTheory.Under.post, CategoryTheory.Comma.snd, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
X_1 Y : Under.{v₁, u₁} X
f : X_1 ⟶ Y
h :
  Eq (α := (Functor.obj (post (F ⋙ G)) X_1).right ⟶ (Functor.obj (post F ⋙ post G) Y).right)
    (Hom.right
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            Y)))
    (Hom.right
      (Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            X_1) ≫
        Functor.map (post F ⋙ post G) f))
⊢ Eq (α := Functor.obj (post (F ⋙ G)) X_1 ⟶ Functor.obj (post F ⋙ post G) Y)
    (Functor.map (post (F ⋙ G)) f ≫
      Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          Y))
    (Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          X_1) ≫
      Functor.map (post F ⋙ post G) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
X_1 Y : Under.{v₁, u₁} X
f : X_1 ⟶ Y
h :
  Hom.right (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).right =
    𝟙 (Functor.obj (post (F ⋙ G)) X_1).right ≫ Hom.right (Functor.map (post F ⋙ post G) f)
⊢ Eq (α := (Functor.obj (post (F ⋙ G)) X_1).right ⟶ (Functor.obj (post F ⋙ post G) Y).right)
    (Hom.right
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            Y)))
    (Hom.right
      (Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            X_1) ≫
        Functor.map (post F ⋙ post G) f))

Tactic:
dsimp only [Iso.refl_hom, Under.comp_right, Under.id_right]

Premises used: CategoryTheory.Under.id_right, CategoryTheory.Iso.refl_hom, CategoryTheory.Under.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
X_1 Y : Under.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ Hom.right (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).right =
    𝟙 (Functor.obj (post (F ⋙ G)) X_1).right ≫ Hom.right (Functor.map (post F ⋙ post G) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Under.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
h₁ : Hom.right f = Hom.right g
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Under.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
⊢ Hom.right f = Hom.right g

Tactic:
F.map_injective (congrArg CommaMorphism.right h)

Premises used: congrArg, CategoryTheory.CommaMorphism.right, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Under.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
⊢ Hom.right f = Hom.right g

Tactic:
exact F.map_injective (congrArg CommaMorphism.right h)

Premises used: congrArg, CategoryTheory.CommaMorphism.right, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
obtain : ∀ (a : A.right ⟶ B.right) (ha : F.map a = Hom.right f), ∃ (a : A ⟶ B), Functor.map (post F) a = f
⊢ ∃ (a : A ⟶ B), Functor.map (post F) a = f

Tactic:
obtain ⟨a, ha⟩ := F.map_surjective f.right

Premises used: CategoryTheory.Under.Hom.right, CategoryTheory.Functor.map_surjective