awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : StructuredArrow S T
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.right (f ≫ g) = Hom.right f ≫ Hom.right g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X : StructuredArrow S T
⊢ Hom.right (𝟙 X) = 𝟙 X.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y_1 Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
h : X = Y
rw rw₁ : Y.right = Y.right
⊢ X.right = Y.right

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
h : X = Y
subst : Hom.right (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X : StructuredArrow S T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, id_right]

Premises used: CategoryTheory.StructuredArrow.id_right, CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f : X ⟶ Y
⊢ f.left = 𝟙 X.left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f f' : StructuredArrow S T
φ : f ⟶ f'
⊢ ∃ (ψ : f.right ⟶ f'.right) (hψ : f.hom ≫ T.map ψ = f'.hom), φ = homMk ψ hψ

Tactic:
⟨φ.right, StructuredArrow.w φ, rfl⟩

Premises used: CategoryTheory.StructuredArrow.w, Exists.intro, rfl, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
⊢ f.homMk' (𝟙 f.right) = eqToHom ⋯

Tactic:
simp [eqToHom_right]

Premises used: CategoryTheory.StructuredArrow.eqToHom_right
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ mk f = mk ((mk f).hom ≫ T.map (𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ (mk f).homMk' (𝟙 Y) = eqToHom ⋯

Tactic:
homMk'_id _

Premises used: CategoryTheory.StructuredArrow.homMk'_id
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f.hom ≫ T.map g)).hom ≫ T.map g') = mk (f.hom ≫ T.map (g ≫ g'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y' Y'' : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ f.homMk' (g ≫ g') = f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯

Tactic:
simp [eqToHom_right]

Premises used: CategoryTheory.StructuredArrow.eqToHom_right
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f ≫ T.map g)).hom ≫ T.map g') = mk ((mk f).hom ≫ T.map (g ≫ g'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y Y' Y'' : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (mk f).homMk' (g ≫ g') = (mk f).homMk' g ≫ (mk (f ≫ T.map g)).homMk' g' ≫ eqToHom ⋯

Tactic:
homMk'_comp _ _ _

Premises used: CategoryTheory.StructuredArrow.homMk'_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ mk f = mk (f ≫ T.map (𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ mkPostcomp f (𝟙 Y) = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((f ≫ T.map g) ≫ T.map g') = mk (f ≫ T.map (g ≫ g'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y Y' Y'' : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f f' : StructuredArrow S T
g : f.right ≅ f'.right
w : f.hom ≫ T.map g.hom = f'.hom
⊢ f.left = f'.left

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
f f' : StructuredArrow S T
g : f.right ≅ f'.right
w : f.hom ≫ T.map g.hom = f'.hom
⊢ Functor.map (Functor.fromPUnit S) (Iso.hom (eqToIso ⋯)) ≫ f'.hom = f.hom ≫ T.map g.hom

Tactic:
simpa using w.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
x y : StructuredArrow S T
hr : x.right = y.right
hh : x.hom ≫ T.map (eqToHom hr) = y.hom
mk :
  ∀ (left : Discrete PUnit.{1}) (right : C) (hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right)
    (hr : StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y.right)
    (hh :
      StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
          T.map (eqToHom hr) =
        y.hom),
    { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
y : StructuredArrow S T
left : Discrete PUnit.{1}
right : C
hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right
hr : StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y.right
hh :
  StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
      T.map (eqToHom hr) =
    y.hom
mk :
  ∀ (left_1 : Discrete PUnit.{1}) (right_1 : C)
    (hom_1 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right_1)
    (hr :
      StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
        StructuredArrow.right { left := left_1, right := right_1, hom := hom_1 : Comma (Functor.fromPUnit S) T })
    (hh :
      StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
          T.map (eqToHom hr) =
        StructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 }),
    { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
      { left := left_1, right := right_1, hom := hom_1 }
⊢ { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
left : Discrete PUnit.{1}
right : C
hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right
left_1 : Discrete PUnit.{1}
right_1 : C
hom_1 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right_1
hr :
  StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    StructuredArrow.right { left := left_1, right := right_1, hom := hom_1 : Comma (Functor.fromPUnit S) T }
hh :
  StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
      T.map (eqToHom hr) =
    StructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 }
mk :
  ∀ (hom_2 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right)
    (hh :
      StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
          T.map (eqToHom ⋯) =
        StructuredArrow.hom { left := left_1, right := right, hom := hom_2 }),
    { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
      { left := left_1, right := right, hom := hom_2 }
⊢ { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    { left := left_1, right := right_1, hom := hom_1 }

Tactic:
cases hr
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f g : A ⟶ B
⊢ Hom.right f = Hom.right g → f = g

Tactic:
CommaMorphism.ext (Subsingleton.elim _ _)

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.CommaMorphism.ext, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f g : A ⟶ B
⊢ f = g ↔ Hom.right f = Hom.right g

Tactic:
⟨fun h => h ▸ rfl, ext f g⟩

Premises used: CategoryTheory.StructuredArrow.ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f : A ⟶ B
h : Mono (Hom.right f)
⊢ Mono f

Tactic:
(proj S T).mono_of_mono_map h

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.StructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f : A ⟶ B
h : Epi (Hom.right f)
⊢ Epi f

Tactic:
(proj S T).epi_of_epi_map h

Premises used: CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.StructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f : A.right ⟶ B.right
w : A.hom ≫ T.map f = B.hom
h : Mono f
⊢ Mono (homMk f w)

Tactic:
(proj S T).mono_of_mono_map h

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.StructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f : A.right ⟶ B.right
w : A.hom ≫ T.map f = B.hom
h : Epi f
⊢ Epi (homMk f w)

Tactic:
(proj S T).epi_of_epi_map h

Premises used: CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.StructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
⊢ f = mk f.hom

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.mk, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
⊢ ∃ (Y : C) (g : S ⟶ T.obj Y), f = mk g

Tactic:
⟨_, _, eq_mk f⟩

Premises used: CategoryTheory.StructuredArrow.eq_mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S' ⟶ T.obj Y
g : S ⟶ S'
⊢ Functor.obj (map g) (mk f) = mk (g ≫ f)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
rw : Functor.obj (map (𝟙 S)) (mk f.hom) = mk f.hom
⊢ Functor.obj (map (𝟙 S)) f = f

Tactic:
rw [eq_mk f]

Premises used: CategoryTheory.StructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
⊢ Functor.obj (map (𝟙 S)) (mk f.hom) = mk f.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
rw : Functor.obj (map (f ≫ f')) (mk h.hom) = Functor.obj (map f) (Functor.obj (map f') (mk h.hom))
⊢ Functor.obj (map (f ≫ f')) h = Functor.obj (map f) (Functor.obj (map f') h)

Tactic:
rw [eq_mk h]

Premises used: CategoryTheory.StructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ Functor.obj (map (f ≫ f')) (mk h.hom) = Functor.obj (map f) (Functor.obj (map f') (mk h.hom))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A B : StructuredArrow S T
f : A ⟶ B
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) ⋯ = 𝟙 A ∧ homMk (inv ((proj S T).map f)) ⋯ ≫ f = 𝟙 B

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
left : m.left = (homMk (T.preimage c.pt.hom) ⋯).left
right : m.right = (homMk (T.preimage c.pt.hom) ⋯).right
⊢ m = homMk (T.preimage c.pt.hom) ⋯

Tactic:
apply CommaMorphism.ext

Premises used: CategoryTheory.CommaMorphism.ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
⊢ m.left = (homMk (T.preimage c.pt.hom) ⋯).left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
right : T.map m.right = T.map (homMk (T.preimage c.pt.hom) ⋯).right
⊢ m.right = (homMk (T.preimage c.pt.hom) ⋯).right

Tactic:
apply T.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
⊢ T.map m.right = T.map (homMk (T.preimage c.pt.hom) ⋯).right

Tactic:
simpa only [homMk_right, T.map_preimage, ← w m] using (Category.id_comp _).symm

Premises used: CategoryTheory.StructuredArrow.homMk_right, CategoryTheory.StructuredArrow.w, Eq.symm, CategoryTheory.Functor.map_preimage, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : D
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Faithful
⊢ (pre S F G).Faithful

Tactic:
show (Comma.preRight _ _ _).Faithful from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, inferInstance, CategoryTheory.StructuredArrow.pre, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : D
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
⊢ (pre S F G).Full

Tactic:
show (Comma.preRight _ _ _).Full from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, inferInstance, CategoryTheory.StructuredArrow.pre, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : D
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.EssSurj
⊢ (pre S F G).EssSurj

Tactic:
show (Comma.preRight _ _ _).EssSurj from inferInstance

Premises used: CategoryTheory.StructuredArrow.Hom, inferInstance, CategoryTheory.StructuredArrow.pre, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : D
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.IsEquivalence
⊢ (pre S F G).IsEquivalence

Tactic:
Comma.isEquivalence_preRight _ _ _

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Comma.isEquivalence_preRight, CategoryTheory.StructuredArrow.pre, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : C
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 : StructuredArrow S F
f : X ⟶ Y_1
⊢ Eq (α := G.obj S ⟶ (F ⋙ G).obj (mk (G.map Y_1.hom)).right)
    ((mk (G.map X.hom)).hom ≫ (F ⋙ G).map (Hom.right f) : G.obj S ⟶ (F ⋙ G).obj (mk (G.map Y_1.hom)).right)
    ((mk (G.map Y_1.hom)).hom : G.obj S ⟶ (F ⋙ G).obj (mk (G.map Y_1.hom)).right)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : C
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
x x_1 : StructuredArrow S F
x_2 x_3 : x ⟶ x_1
h : (post S F G).map x_2 = (post S F G).map x_3
⊢ x_2 = x_3

Tactic:
simpa [ext_iff] using h

Premises used: CategoryTheory.StructuredArrow.ext_iff
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : C
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.Faithful
X Y_1 : StructuredArrow S F
f : (post S F G).obj X ⟶ (post S F G).obj Y_1
⊢ G.map (X.hom ≫ F.map (Hom.right f)) = G.map Y_1.hom

Tactic:
simpa using f.w

Premises used: CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : C
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.Faithful
X Y_1 : StructuredArrow S F
f : (post S F G).obj X ⟶ (post S F G).obj Y_1
⊢ (post S F G).map (homMk (Hom.right f) ⋯) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S_1 S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
S : C
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.Full
h : StructuredArrow (G.obj S) (F ⋙ G)
⊢ ((post S F G).obj (mk (G.preimage h.hom))).hom ≫
      (F ⋙ G).map (Iso.hom (Iso.refl ((post S F G).obj (mk (G.preimage h.hom))).right)) =
    h.hom

Tactic:
simp