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 : Over.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b
h : Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left g
let :
  ∀ (left_1 : U.left ⟶ V.left) (e : U.right ⟶ V.right)
    (w_1 : Functor.map (𝟭 T) left_1 ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) e)
    (h :
      Hom.left { left := left, right := b, w := w : CommaMorphism U V } =
        Hom.left { 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 : Over.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (𝟭 T) left_1 ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) e
h :
  Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left { left := left_1, right := e, w := w_1 }
e_right : b = e
⊢ { 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 : Over.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (𝟭 T) left_1 ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) e
h :
  Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left { left := left_1, right := e, w := w_1 }
⊢ b = e

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 : Over.{v₁, u₁} X
⊢ U.right = { as := PUnit.unit }

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

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 : Over.{v₁, u₁} X
f : a ⟶ b
g : b ⟶ c
⊢ Hom.left (f ≫ g) = Hom.left f ≫ Hom.left g

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
U V W : Over.{v₁, u₁} X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ (f ≫ g) ≫ W.hom = U.hom

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V W : Over.{v₁, u₁} X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
h : Hom.left (homMk (f ≫ g) ⋯) = Hom.left (homMk f w_f ≫ homMk g w_g)
⊢ homMk (f ≫ g) ⋯ = homMk f w_f ≫ homMk g w_g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V W : Over.{v₁, u₁} X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ Hom.left (homMk (f ≫ g) ⋯) = Hom.left (homMk f w_f ≫ homMk g w_g)

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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
h : f = g
rw rw₁ : g.left = g.left
⊢ f.left = g.left

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

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

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

Tactic:
simp [← Over.comp_left]

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

Tactic:
simp [← Over.comp_left]

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

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

Tactic:
⟨_, X.hom, rfl⟩

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

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Over.{v₁, u₁} X
f : U ⟶ V
⊢ Functor.map (forget X) f = Hom.left 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 : Over.{v₁, u₁} X
⊢ ((map f).obj U).left = U.left

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
U : Over.{v₁, u₁} X
⊢ ((map f).obj U).hom = U.hom ≫ 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 V : Over.{v₁, u₁} X
g : U ⟶ V
⊢ Hom.left ((map f).map g) = Hom.left g

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, 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.Over.map, CategoryTheory.Comma.mapRight, 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.Over.map, CategoryTheory.Comma.mapRight, 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
Y : T
f : X ⟶ Y
U V : Over.{v₁, u₁} X
g : U ⟶ V
inst_2 : IsIso f
⊢ (map f).IsEquivalence

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

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

Tactic:
simp [map, Comma.mapRight]

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Over.{v₁, u₁} Y
h : Hom.left (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.left (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 : Over.{v₁, u₁} Y
⊢ Hom.left (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.left (eqToHom ⋯)

Tactic:
simp [eqToHom_left]

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

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.Comma.fst, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, 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
x : Over.{v₁, u₁} X
⊢ (map (f ≫ g)).obj x = (map f ⋙ map g).obj x

Tactic:
simp [map, Comma.mapRight]

Premises used: CategoryTheory.Over.map, CategoryTheory.Comma.mapRight
-- 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 : Over.{v₁, u₁} X
h : Hom.left ((mapComp f g).hom.app x) = Hom.left (eqToHom ⋯)
⊢ (mapComp f g).hom.app x = 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
x : Over.{v₁, u₁} X
⊢ Hom.left ((mapComp f g).hom.app x) = Hom.left (eqToHom ⋯)

Tactic:
simp [eqToHom_left]

Premises used: CategoryTheory.Over.eqToHom_left
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ mapCongr f f ⋯ = Iso.refl (map f)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.Over.mapCongr, CategoryTheory.NatTrans.id, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Over.{v₁, u₁} X
rw : Hom.left (homMk Y.hom ⋯) = Y.hom
⊢ Hom.left (Limits.IsTerminal.from mkIdTerminal Y) = Y.hom

Tactic:
rw [mkIdTerminal.hom_ext (mkIdTerminal.from Y) (homMk Y.hom)]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Over.homMk, CategoryTheory.Over.mkIdTerminal, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Over.{v₁, u₁} X
⊢ Hom.left (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 : Over.{v₁, u₁} X
k : f ⟶ g
hk : Epi (Hom.left k)
⊢ Epi k

Tactic:
(forget X).epi_of_epi_map hk

Premises used: CategoryTheory.Over.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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
U V : Over.{v₁, u₁} X
f : U.left ⟶ V.left
inst_2 : Epi f
w : f ≫ V.hom = U.hom
⊢ Epi (homMk f w)

Tactic:
(forget X).epi_of_epi_map ‹_›

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

Tactic:
(forget X).mono_of_mono_map hk

Premises used: CategoryTheory.Over.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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
U V : Over.{v₁, u₁} X
f : U.left ⟶ V.left
inst_2 : Mono f
w : f ≫ V.hom = U.hom
⊢ Mono (homMk f w)

Tactic:
(forget X).mono_of_mono_map ‹_›

Premises used: CategoryTheory.Over.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_1 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
⊢ Mono (Hom.left k)

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

Premises used: CategoryTheory.Mono.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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
refine : ∀ {Y : T} (l m : Y ⟶ f.left) (a : l ≫ Hom.left k = m ≫ Hom.left k), l = m
⊢ Mono (Hom.left 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
dsimp : l ≫ f.hom = m ≫ f.hom
⊢ l ≫ f.hom = (mk (m ≫ f.hom)).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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
rw : l ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₁ : (l ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₂ : (m ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₃ rw₄ : m ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
⊢ l ≫ f.hom = m ≫ f.hom

Tactic:
rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc]

Premises used: CategoryTheory.Category.assoc, congrArg, CategoryTheory.Over.w, CategoryTheory.CategoryStruct.comp, CategoryTheory.Over.hom
-- 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
this : l' = homMk m ⋯
⊢ l = m

Tactic:
apply congrArg CommaMorphism.left this

Premises used: congrArg, CategoryTheory.CommaMorphism.left
-- 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
suffices : l' = homMk m ⋯
⊢ l = m

Tactic:
suffices l' = (homMk m : mk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
rw : l' ≫ k = homMk m ⋯ ≫ k
⊢ l' = homMk m ⋯

Tactic:
rw [← cancel_mono k]

Premises used: CategoryTheory.cancel_mono
-- 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
h : Hom.left (l' ≫ k) = Hom.left (homMk m ⋯ ≫ k)
⊢ l' ≫ k = homMk m ⋯ ≫ k

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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
⊢ Hom.left (l' ≫ k) = Hom.left (homMk m ⋯ ≫ k)

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 : T
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
f : Over.{v₁, u₁} X
X_1 Y : Over f
κ : X_1 ⟶ Y
dsimp : Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left X_1.hom
⊢ Hom.left (Hom.left κ) ≫ (mk (Hom.left Y.hom)).hom = (mk (Hom.left X_1.hom)).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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
f : Over.{v₁, u₁} X
X_1 Y : Over f
κ : X_1 ⟶ Y
rw : Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left (Hom.left κ ≫ Y.hom)
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left X_1.hom

Tactic:
rw [← Over.w κ]

Premises used: CategoryTheory.Over.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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
f : Over.{v₁, u₁} X
X_1 Y : Over f
κ : X_1 ⟶ Y
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left (Hom.left κ ≫ Y.hom)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f : Over.{v₁, u₁} X
⊢ f.iteratedSliceBackward ⋙ forget f = map f.hom

Tactic:
rfl

Premises used: CategoryTheory.Over.map, CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.Functor.comp, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Comma.mapRight, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f : Over.{v₁, u₁} X
⊢ f.iteratedSliceForward ⋙ forget f.left = forget f ⋙ forget X

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.Comma.fst, CategoryTheory.Over.mk, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.Over.iteratedSliceForward, CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f : Over.{v₁, u₁} X
⊢ f.iteratedSliceBackward ⋙ forget f ⋙ forget X = forget f.left

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.Comma.fst, CategoryTheory.Over.mk, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.mk, 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
X_1 Y : Over.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ F.map (Hom.left f) ≫ (mk (F.map Y.hom)).hom = (mk (F.map X_1.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 (α := Over.{v₁, u₁} X ⥤ Over.{v_1, u_1} ((F ⋙ G).obj X)) (post (F ⋙ G)) (post F ⋙ post G)

Tactic:
rfl

Premises used: CategoryTheory.Over.mk, CategoryTheory.Functor.comp, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, CategoryTheory.Over.post, CategoryTheory.CostructuredArrow.mk, 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.Over, CategoryTheory.Comma.fst, CategoryTheory.Over.mk, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.CostructuredArrow, CategoryTheory.Over.post, CategoryTheory.CostructuredArrow.mk, 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 : Over.{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 : Over.{v₁, u₁} X
f : X_1 ⟶ Y
h :
  Eq (α := (Functor.obj (post (F ⋙ G)) X_1).left ⟶ (Functor.obj (post F ⋙ post G) Y).left)
    (Hom.left
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Over.{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.left
      (Iso.hom
          ((fun (X_2 : Over.{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 : Over.{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 : Over.{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 : Over.{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 : Over.{v₁, u₁} X
f : X_1 ⟶ Y
h :
  Hom.left (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).left =
    𝟙 (Functor.obj (post (F ⋙ G)) X_1).left ≫ Hom.left (Functor.map (post F ⋙ post G) f)
⊢ Eq (α := (Functor.obj (post (F ⋙ G)) X_1).left ⟶ (Functor.obj (post F ⋙ post G) Y).left)
    (Hom.left
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Over.{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.left
      (Iso.hom
          ((fun (X_2 : Over.{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, Over.comp_left, Over.id_left]

Premises used: CategoryTheory.Over.comp_left, CategoryTheory.Over.id_left, CategoryTheory.Iso.refl_hom
-- 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 : Over.{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 : Over.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ Hom.left (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).left =
    𝟙 (Functor.obj (post (F ⋙ G)) X_1).left ≫ Hom.left (Functor.map (post F ⋙ post G) f)

Tactic:
simp