awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D : Type u₂
inst_2 : Category.{v₂, u₂} D
X : T
F : Functor.{v₂, v₁, u₂, u₁} D T
inst_3 : F.IsEquivalence
⊢ (toUnder X F).IsEquivalence

Tactic:
StructuredArrow.isEquivalence_pre _ _ _

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.StructuredArrow.isEquivalence_pre, CategoryTheory.Functor.comp, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.toUnder
-- 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 : Functor.{v₁, v₂, u₁, u₂} T D
Y : Over.{v₂, u₂} (F.obj X)
⊢ essImage (Over.post F) Y → F.essImage Y.left

Tactic:
fun ⟨Z, ⟨e⟩⟩ ↦ ⟨Z.left, ⟨(Over.forget _).mapIso e⟩⟩

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Over.left, _private.0.CategoryTheory.Functor.essImage.of_overPost.match_1, Exists.intro, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- 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 : Functor.{v₁, v₂, u₁, u₂} T D
Y : Under.{v₂, u₂} (F.obj X)
⊢ essImage (Under.post F) Y → F.essImage Y.right

Tactic:
fun ⟨Z, ⟨e⟩⟩ ↦ ⟨Z.right, ⟨(Under.forget _).mapIso e⟩⟩

Premises used: CategoryTheory.Under.right, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Under.forget, Exists.intro, _private.0.CategoryTheory.Functor.essImage.of_underPost.match_1, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
S : Type u₂
inst_1 : Category.{v₂, u₂} S
F : Functor.{v₂, v₁, u₂, u₁} S T
X : T
f : (Y : S) → F.obj Y ⟶ X
h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y
⊢ F.toOver X f ⋯ ⋙ Over.forget X = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
S : Type u₂
inst_1 : Category.{v₂, u₂} S
F : Functor.{v₂, v₁, u₂, u₁} S T
X : T
f : (Y : S) → X ⟶ F.obj Y
h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z
⊢ F.toUnder X f ⋯ ⋙ Under.forget X = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, 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₁} D T
Y : T
X : D
g : StructuredArrow X (proj Y F)
⊢ X ⟶ (proj X (proj Y F) ⋙ proj Y F).obj g

Tactic:
exact g.hom

Premises used: CategoryTheory.StructuredArrow.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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
Y_1 Z : StructuredArrow X (proj Y F)
m : Y_1 ⟶ Z
⊢ Y_1.hom ≫ (proj Y F).map (Hom.right m) = Z.hom

Tactic:
have := m.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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow X (proj Y F)} (g : Y_1 ⟶ Z),
    Eq (α :=
      Y ⟶
        (Under.forget X ⋙ F).obj
          (((proj X (proj Y F) ⋙ proj Y F).toUnder X (fun (g : StructuredArrow X (proj Y F)) ↦ g.hom) ⋯).obj Z))
      ((fun (f : StructuredArrow X (proj Y F)) ↦ f.right.hom) Y_1 ≫
        (Under.forget X ⋙ F).map
          (((proj X (proj Y F) ⋙ proj Y F).toUnder X (fun (g : StructuredArrow X (proj Y F)) ↦ g.hom) ⋯).map g))
      ((fun (f : StructuredArrow X (proj Y F)) ↦ f.right.hom) Z)

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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
g : StructuredArrow Y (Under.forget X ⋙ F)
⊢ Y ⟶ F.obj ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).obj g)

Tactic:
exact g.hom

Premises used: CategoryTheory.StructuredArrow.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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)
m : Y_1 ⟶ Z
⊢ Y_1.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z.hom

Tactic:
have := m.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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)} (g : Y_1 ⟶ Z),
    Eq (α :=
      X ⟶
        (proj Y F).obj
          (((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).toStructuredArrow Y F
                (fun (g : StructuredArrow Y (Under.forget X ⋙ F)) ↦ g.hom) ⋯).obj
            Z))
      ((fun (f : StructuredArrow Y (Under.forget X ⋙ F)) ↦ f.right.hom) Y_1 ≫
        (proj Y F).map
          (((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).toStructuredArrow Y F
                (fun (g : StructuredArrow Y (Under.forget X ⋙ F)) ↦ g.hom) ⋯).map
            g))
      ((fun (f : StructuredArrow Y (Under.forget X ⋙ F)) ↦ f.right.hom) Z)

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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow X (proj Y F)} (f : X_1 ⟶ Y_1),
    Eq (α :=
      Functor.obj (𝟭 (StructuredArrow X (proj Y F))) X_1 ⟶
        (ofStructuredArrowProjEquivalence.functor F Y X ⋙ ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1)
      (Functor.map (𝟭 (StructuredArrow X (proj Y F))) f ≫
        Iso.hom
          ((fun (x : StructuredArrow X (proj Y F)) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x) :
                Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x ≅ Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x))
            Y_1))
      (Iso.hom
          ((fun (x : StructuredArrow X (proj Y F)) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x) :
                Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x ≅ Functor.obj (𝟭 (StructuredArrow X (proj Y F))) x))
            X_1) ≫
        (ofStructuredArrowProjEquivalence.functor F Y X ⋙ ofStructuredArrowProjEquivalence.inverse F Y X).map 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 × T
Y Z : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)
g : Y ⟶ Z
⊢ Eq (α := X.1 ⟶ Functor.obj (proj X (Functor.diag T)) Z)
    ((fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.1) Y ≫
      Functor.map (proj X (Functor.diag T)) g)
    ((fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.1) Z)

Tactic:
simp [← w g]

Premises used: CategoryTheory.StructuredArrow.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 × T
Y Z : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)
g : Y ⟶ Z
⊢ Eq (α :=
    X.2 ⟶
      Functor.obj (Under.forget X.1)
        (Functor.obj
          (Functor.toUnder (proj X (Functor.diag T)) X.1
            (fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.1) ⋯)
          Z))
    ((fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.2) Y ≫
      Functor.map (Under.forget X.1)
        (Functor.map
          (Functor.toUnder (proj X (Functor.diag T)) X.1
            (fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.1) ⋯)
          g))
    ((fun (f : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦ f.hom.2) Z)

Tactic:
simp [← w g]

Premises used: CategoryTheory.StructuredArrow.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 × T
Y Z : StructuredArrow (C := Under.{v₁, u₁} X.1) X.2 (Under.forget X.1)
m : Y ⟶ Z
⊢ Y.hom ≫ Functor.map (Under.forget X.1) (Hom.right m) = Z.hom

Tactic:
have := m.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 × T
⊢ ∀ {X_1 Y : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)} (f : X_1 ⟶ Y),
    Eq (α :=
      Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) X_1 ⟶
        Functor.obj (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X) Y)
      (Functor.map (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) f ≫
        Iso.hom
          ((fun (x : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x) :
                Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x ≅
                  Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x))
            Y))
      (Iso.hom
          ((fun (x : StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T)) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x) :
                Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x ≅
                  Functor.obj (𝟭 (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag T))) x))
            X_1) ≫
        Functor.map (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X) 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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
X Y : StructuredArrow c (Comma.fst F G)
f : X ⟶ Y
⊢ (Comma.left (T := T) (L := Under.forget c ⋙ F) (R := G)
          { left := Under.mk X.hom, right := X.right.right, hom := X.right.hom : Comma (Under.forget c ⋙ F) G }).hom ≫
      (Hom.right f).left =
    (Comma.left (T := T) (L := Under.forget c ⋙ F) (R := G)
        { left := Under.mk Y.hom, right := Y.right.right, hom := Y.right.hom }).hom

Tactic:
simp [dsimp% f.w]

Premises used: CategoryTheory.StructuredArrow.Hom.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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
X Y : StructuredArrow c (Comma.fst F G)
f : X ⟶ Y
⊢ (Under.forget c ⋙ F).map (Under.homMk (Hom.right f).left ⋯) ≫
      Comma.hom { left := Under.mk Y.hom, right := Y.right.right, hom := Y.right.hom : Comma (Under.forget c ⋙ F) G } =
    Comma.hom { left := Under.mk X.hom, right := X.right.right, hom := X.right.hom : Comma (Under.forget c ⋙ F) G } ≫
      G.map (Hom.right f).right

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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
Y Z : Comma (Under.forget c ⋙ F) G
x : Y ⟶ Z
⊢ Eq (α := c ⟶ (Comma.fst F G).obj (Functor.obj (Comma.preLeft (Under.forget c) F G) Z))
    ((fun (Y : Comma (Under.forget c ⋙ F) G) ↦ Y.left.hom) Y ≫
      (Comma.fst F G).map (Functor.map (Comma.preLeft (Under.forget c) F G) x))
    ((fun (Y : Comma (Under.forget c ⋙ F) G) ↦ Y.left.hom) Z)

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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
g : CostructuredArrow (proj F Y) X
⊢ (proj (proj F Y) X ⋙ proj F Y).obj g ⟶ X

Tactic:
exact g.hom

Premises used: CategoryTheory.CostructuredArrow.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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
Y_1 Z : CostructuredArrow (proj F Y) X
m : Y_1 ⟶ Z
⊢ (proj F Y).map m.left ≫ Z.hom = Y_1.hom ≫ Functor.map (Functor.fromPUnit X) m.right

Tactic:
have := m.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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (proj F Y) X} (g : Y_1 ⟶ Z),
    Eq (α :=
      (Over.forget X ⋙ F).obj
          (((proj (proj F Y) X ⋙ proj F Y).toOver X (fun (g : CostructuredArrow (proj F Y) X) ↦ g.hom) ⋯).obj Y_1) ⟶
        Y)
      ((Over.forget X ⋙ F).map
          (((proj (proj F Y) X ⋙ proj F Y).toOver X (fun (g : CostructuredArrow (proj F Y) X) ↦ g.hom) ⋯).map g) ≫
        (fun (f : CostructuredArrow (proj F Y) X) ↦ f.left.hom) Z)
      ((fun (f : CostructuredArrow (proj F Y) X) ↦ f.left.hom) Y_1)

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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
g : CostructuredArrow (Over.forget X ⋙ F) Y
⊢ F.obj ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).obj g) ⟶ Y

Tactic:
exact g.hom

Premises used: CategoryTheory.CostructuredArrow.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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y_1 ⟶ Z
⊢ (Over.forget X ⋙ F).map m.left ≫ Z.hom = Y_1.hom ≫ Functor.map (Functor.fromPUnit Y) m.right

Tactic:
have := m.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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y} (g : Y_1 ⟶ Z),
    Eq (α :=
      (proj F Y).obj
          (((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).toCostructuredArrow F Y
                (fun (g : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ g.hom) ⋯).obj
            Y_1) ⟶
        X)
      ((proj F Y).map
          (((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).toCostructuredArrow F Y
                (fun (g : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ g.hom) ⋯).map
            g) ≫
        (fun (f : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ f.left.hom) Z)
      ((fun (f : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ f.left.hom) Y_1)

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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (proj F Y) X} (f : X_1 ⟶ Y_1),
    Eq (α :=
      Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) X_1 ⟶
        (ofCostructuredArrowProjEquivalence.functor F Y X ⋙ ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1)
      (Functor.map (𝟭 (CostructuredArrow (proj F Y) X)) f ≫
        Iso.hom
          ((fun (x : CostructuredArrow (proj F Y) X) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x) :
                Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x ≅
                  Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x))
            Y_1))
      (Iso.hom
          ((fun (x : CostructuredArrow (proj F Y) X) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x) :
                Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x ≅
                  Functor.obj (𝟭 (CostructuredArrow (proj F Y) X)) x))
            X_1) ≫
        (ofCostructuredArrowProjEquivalence.functor F Y X ⋙ ofCostructuredArrowProjEquivalence.inverse F Y X).map 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 × T
g : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X
⊢ Functor.obj (proj (Functor.diag T) X) g ⟶ X.1

Tactic:
exact g.hom.1

Premises used: CategoryTheory.CostructuredArrow.hom, Prod.fst
-- 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 × T
Y Z : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X
m : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left).1 ⟶
      (Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right).1)
    ((fun
          (x :
            Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
              Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
        x.1)
      (Functor.map (Functor.diag T) m.left ≫ Z.hom))
    ((fun
          (x :
            Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
              Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
        x.1)
      (Y.hom ≫ Functor.map (Functor.fromPUnit X) m.right))

Tactic:
have := congrArg (·.1) m.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 × T
Y Z : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X
m : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left).2 ⟶
      (Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right).2)
    ((fun
          (x :
            Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
              Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
        x.2)
      (Functor.map (Functor.diag T) m.left ≫ Z.hom))
    ((fun
          (x :
            Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
              Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
        x.2)
      (Y.hom ≫ Functor.map (Functor.fromPUnit X) m.right))

Tactic:
have := congrArg (·.2) m.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 × T
Y Z : CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) X.2
m : Y ⟶ Z
⊢ Functor.map (Over.forget X.1) m.left ≫ Z.hom = Y.hom ≫ Functor.map (Functor.fromPUnit X.2) m.right

Tactic:
have := m.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 × T
⊢ ∀ {X_1 Y : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X} (f : X_1 ⟶ Y),
    Eq (α :=
      Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) X_1 ⟶
        Functor.obj (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X) Y)
      (Functor.map (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) f ≫
        Iso.hom
          ((fun (x : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x) :
                Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x ≅
                  Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x))
            Y))
      (Iso.hom
          ((fun (x : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x) :
                Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x ≅
                  Functor.obj (𝟭 (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X)) x))
            X_1) ≫
        Functor.map (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X) 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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
X Y : CostructuredArrow (Comma.fst F G) c
f : X ⟶ Y
⊢ f.left.left ≫
      (Comma.left (T := T) (L := Over.forget c ⋙ F) (R := G)
          { left := Over.mk Y.hom, right := Y.left.right, hom := Y.left.hom : Comma (Over.forget c ⋙ F) G }).hom =
    (Comma.left (T := T) (L := Over.forget c ⋙ F) (R := G)
        { left := Over.mk X.hom, right := X.left.right, hom := X.left.hom }).hom

Tactic:
simpa using f.w

Premises used: CategoryTheory.CommaMorphism.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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
X Y : CostructuredArrow (Comma.fst F G) c
f : X ⟶ Y
⊢ (Over.forget c ⋙ F).map (Over.homMk f.left.left ⋯) ≫
      Comma.hom { left := Over.mk Y.hom, right := Y.left.right, hom := Y.left.hom : Comma (Over.forget c ⋙ F) G } =
    Comma.hom { left := Over.mk X.hom, right := X.left.right, hom := X.left.hom : Comma (Over.forget c ⋙ F) G } ≫
      G.map f.left.right

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
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₁, u₃, u₁} C T
G : Functor.{v₂, v₁, u₂, u₁} D T
c : C
Y Z : Comma (Over.forget c ⋙ F) G
x : Y ⟶ Z
⊢ Eq (α := (Comma.fst F G).obj (Functor.obj (Comma.preLeft (Over.forget c) F G) Y) ⟶ c)
    ((Comma.fst F G).map (Functor.map (Comma.preLeft (Over.forget c) F G) x) ≫
      (fun (Y : Comma (Over.forget c ⋙ F) G) ↦ Y.left.hom) Z)
    ((fun (Y : Comma (Over.forget c ⋙ F) G) ↦ Y.left.hom) Y)

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
Z Y : Over.{v₁, u₁} (op X)
f : Z ⟶ Y
dsimp : Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop
⊢ (unop (op (Under.mk Y.hom.unop))).hom ≫ (Hom.left f).unop = (unop (op (Under.mk Z.hom.unop))).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
Z Y : Over.{v₁, u₁} (op X)
f : Z ⟶ Y
rw : (Hom.left f ≫ Y.hom).unop = Z.hom.unop
rw₁ rw₂ : Z.hom.unop = Z.hom.unop
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop

Tactic:
rw [← unop_comp, Over.w]

Premises used: CategoryTheory.unop_comp, 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
Z Y : (Under.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
dsimp : (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op
⊢ Eq.{v₁ + 1} (α := left.{v₁, u₁} (X := op X) (mk (unop Z).hom.op) ⟶ op X)
    ((Under.Hom.right f.unop).op ≫ hom (mk (unop Y).hom.op)) (hom (mk (unop Z).hom.op))

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
Z Y : (Under.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
rw : (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = ((unop Y).hom ≫ Under.Hom.right f.unop).op
rw₁ rw₂ :
  Eq.{v₁ + 1} (α := op (unop Z).right ⟶ op X) ((Under.Hom.right f.unop).op ≫ (unop Y).hom.op)
    ((Under.Hom.right f.unop).op ≫ (unop Y).hom.op)
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op

Tactic:
rw [← Under.w f.unop, op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.unop, 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
Z Y : Under.{v₁, u₁} (op X)
f : Z ⟶ Y
dsimp : (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop
⊢ (Hom.right f).unop ≫ (unop (op (Over.mk Z.hom.unop))).hom = (unop (op (Over.mk Y.hom.unop))).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
Z Y : Under.{v₁, u₁} (op X)
f : Z ⟶ Y
rw : (Z.hom ≫ Hom.right f).unop = Y.hom.unop
rw₁ rw₂ : Y.hom.unop = Y.hom.unop
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop

Tactic:
rw [← unop_comp, Under.w]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Under.w