awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.EssSurj
inst_7 : F₂.EssSurj
inst_8 : F.Full
inst_9 : IsIso α
inst_10 : IsIso β
X : Comma L' R'
simp :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
      X.hom ≫
        CategoryStruct.comp (Y := R'.obj (F₂.obj (F₂.objPreimage X.right)))
          (R'.map (Iso.inv (F₂.objObjPreimageIso X.right))) (R'.map (Iso.hom (F₂.objObjPreimageIso X.right))))
⊢ Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (CategoryStruct.comp (Y := R'.obj (F₂.obj (F₂.objPreimage X.right)))
      (α.app (F₁.objPreimage X.left) ≫
        F.map
            (F.preimage
              ((inv α).app (F₁.objPreimage X.left) ≫
                L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
                  X.hom ≫ R'.map (Iso.inv (F₂.objObjPreimageIso X.right)) ≫ (inv β).app (F₂.objPreimage X.right))) ≫
          β.app (F₂.objPreimage X.right))
      (R'.map (Iso.hom (F₂.objObjPreimageIso X.right))))

Tactic:
simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.map_preimage, assoc,
              IsIso.inv_hom_id, comp_id, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.EssSurj
inst_7 : F₂.EssSurj
inst_8 : F.Full
inst_9 : IsIso α
inst_10 : IsIso β
X : Comma L' R'
rw :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
      X.hom ≫
        R'.map
          (CategoryStruct.comp (Y := F₂.obj (F₂.objPreimage X.right)) (Iso.inv (F₂.objObjPreimageIso X.right))
            (Iso.hom (F₂.objObjPreimageIso X.right))))
rw₁ :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom ≫ R'.map (𝟙 X.right))
rw₂ :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom ≫ 𝟙 (R'.obj X.right))
rw₃ rw₄ :
  Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom) (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
⊢ Eq (α := L'.obj (F₁.obj (F₁.objPreimage X.left)) ⟶ R'.obj X.right)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom)
    (L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫
      X.hom ≫
        CategoryStruct.comp (Y := R'.obj (F₂.obj (F₂.objPreimage X.right)))
          (R'.map (Iso.inv (F₂.objObjPreimageIso X.right))) (R'.map (Iso.hom (F₂.objObjPreimageIso X.right))))

Tactic:
rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ map α β ⋙ fst L' R' = fst L R ⋙ F₁

Tactic:
rfl

Premises used: CategoryTheory.Comma.fst, CategoryTheory.Functor.comp, CategoryTheory.Comma.map, rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ ∀ {X Y : Comma L R} (f : X ⟶ Y),
    (map α β ⋙ fst L' R').map f ≫
        Iso.hom
          ((fun (x : Comma L R) ↦
              (Iso.refl ((map α β ⋙ fst L' R').obj x) : (map α β ⋙ fst L' R').obj x ≅ (map α β ⋙ fst L' R').obj x))
            Y) =
      Iso.hom
          ((fun (x : Comma L R) ↦
              (Iso.refl ((map α β ⋙ fst L' R').obj x) : (map α β ⋙ fst L' R').obj x ≅ (map α β ⋙ fst L' R').obj x))
            X) ≫
        (fst L R ⋙ F₁).map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ map α β ⋙ snd L' R' = snd L R ⋙ F₂

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comma.map, CategoryTheory.Comma.snd, rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ ∀ {X Y : Comma L R} (f : X ⟶ Y),
    (map α β ⋙ snd L' R').map f ≫
        Iso.hom
          ((fun (x : Comma L R) ↦
              (Iso.refl ((map α β ⋙ snd L' R').obj x) : (map α β ⋙ snd L' R').obj x ≅ (map α β ⋙ snd L' R').obj x))
            Y) =
      Iso.hom
          ((fun (x : Comma L R) ↦
              (Iso.refl ((map α β ⋙ snd L' R').obj x) : (map α β ⋙ snd L' R').obj x ≅ (map α β ⋙ snd L' R').obj x))
            X) ≫
        (snd L R ⋙ F₂).map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
F : Functor.{v₄, v₁, u₄, u₁} C A
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma (F ⋙ L) R
f : X ⟶ Y
⊢ L.map (F.map f.left) ≫ { left := F.obj Y.left, right := Y.right, hom := Y.hom : Comma L R }.hom =
    { left := F.obj X.left, right := X.right, hom := X.hom : Comma L R }.hom ≫ R.map f.right

Tactic:
simpa using f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
F : Functor.{v₄, v₁, u₄, u₁} C A
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.Faithful
⊢ (preLeft F L R).Faithful

Tactic:
Functor.Faithful.of_iso (preLeftIso F L R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preLeftIso, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
F : Functor.{v₄, v₁, u₄, u₁} C A
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.Full
⊢ (preLeft F L R).Full

Tactic:
Functor.Full.of_iso (preLeftIso F L R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preLeftIso, CategoryTheory.Functor.Full.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
F : Functor.{v₄, v₁, u₄, u₁} C A
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.EssSurj
⊢ (preLeft F L R).EssSurj

Tactic:
Functor.essSurj_of_iso (preLeftIso F L R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preLeftIso, CategoryTheory.Functor.essSurj_of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
F : Functor.{v₄, v₂, u₄, u₂} C B
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.Faithful
⊢ (preRight L F R).Faithful

Tactic:
Functor.Faithful.of_iso (preRightIso L F R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preRightIso, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
F : Functor.{v₄, v₂, u₄, u₂} C B
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.Full
⊢ (preRight L F R).Full

Tactic:
Functor.Full.of_iso (preRightIso L F R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preRightIso, CategoryTheory.Functor.Full.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
F : Functor.{v₄, v₂, u₄, u₂} C B
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_7 : F.EssSurj
⊢ (preRight L F R).EssSurj

Tactic:
Functor.essSurj_of_iso (preRightIso L F R).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Comma.preRightIso, CategoryTheory.Functor.essSurj_of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : Functor.{v₃, v₄, u₃, u₄} T C
X Y : Comma L R
f : X ⟶ Y
⊢ (L ⋙ F).map f.left ≫ hom { left := Y.left, right := Y.right, hom := F.map Y.hom } =
    hom { left := X.left, right := X.right, hom := F.map X.hom : Comma (L ⋙ F) (R ⋙ F) } ≫ (R ⋙ F).map f.right

Tactic:
simp only [Functor.comp_map, ← F.map_comp, f.w]

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : Functor.{v₃, v₄, u₃, u₄} T C
⊢ (post L R F).Faithful

Tactic:
Functor.Faithful.of_iso (postIso L R F).symm

Premises used: CategoryTheory.Comma.postIso, CategoryTheory.Iso.symm, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : Functor.{v₃, v₄, u₃, u₄} T C
inst_7 : F.Faithful
⊢ (post L R F).Full

Tactic:
Functor.Full.of_iso (postIso L R F).symm

Premises used: CategoryTheory.Comma.postIso, CategoryTheory.Iso.symm, CategoryTheory.Functor.Full.of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L_1 : Functor.{v₁, v₃, u₁, u₃} A T
R_1 : Functor.{v₂, v₃, u₂, u₃} B T
C : Type u₄
inst_6 : Category.{v₄, u₄} C
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : Functor.{v₃, v₄, u₃, u₄} T C
inst_7 : F.Full
⊢ (post L R F).EssSurj

Tactic:
Functor.essSurj_of_iso (postIso L R F).symm

Premises used: CategoryTheory.Comma.postIso, CategoryTheory.Iso.symm, CategoryTheory.Functor.essSurj_of_iso
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
L : Functor.{v₁, u_1, u₁, u_1} A (Discrete PUnit.{u_1 + 1})
R : Functor.{u_2, u_1, u_2, u_1} (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})
⊢ (toPUnitIdEquiv L R).functor = fst L R

Tactic:
rfl

Premises used: CategoryTheory.Comma.fst, CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
B : Type u₂
inst : Category.{v₂, u₂} B
L : Functor.{u_1, u_2, u_1, u_2} (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})
R : Functor.{v₂, u_2, u₂, u_2} B (Discrete PUnit.{u_2 + 1})
⊢ (toIdPUnitEquiv L R).functor = snd L R

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comma.snd, rfl
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
f : X ⟶ Y
⊢ (R.op.map (op f.right) ≫
        hom (unop (op { left := op X.right, right := op X.left, hom := op X.hom : Comma R.op L.op }))).unop =
    (hom (unop (op { left := op Y.right, right := op Y.left, hom := op Y.hom })) ≫ L.op.map (op f.left)).unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L.op R.op
f : X ⟶ Y
⊢ (R.map f.right.unop ≫
        (unop (op { left := unop X.right, right := unop X.left, hom := X.hom.unop : Comma R L })).hom).op =
    ((unop (op { left := unop Y.right, right := unop Y.left, hom := Y.hom.unop : Comma R L })).hom ≫
        L.map f.left.unop).op

Tactic:
simpa using f.w.symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
mp : Finite.{u + 1} (Arrow C) → Nonempty.{u + 1} (FinCategory C)
mpr : Nonempty.{u + 1} (FinCategory C) → Finite.{u + 1} (Arrow C)
⊢ Finite.{u + 1} (Arrow C) ↔ Nonempty.{u + 1} (FinCategory C)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
⊢ Nonempty.{u + 1} (FinCategory C)

Tactic:
⟨?_, fun a b ↦ ?_⟩

Premises used: Nonempty.intro, CategoryTheory.FinCategory.mk
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
mp : Fintype C
mp₁ : (a b : C) → Fintype (a ⟶ b)
⊢ Nonempty.{u + 1} (FinCategory C)

Tactic:
refine ⟨?_, fun a b ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
⊢ Finite C

Tactic:
have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
        (fun _ _ ↦ congr_arg Comma.left)
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
this : Finite C
⊢ Fintype C

Tactic:
apply Fintype.ofFinite

Premises used: Fintype.ofFinite
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h_1 : Finite.{u + 1} (Arrow C)
a b : C
f g : a ⟶ b
h : Eq.{u + 1} (α := Arrow C) ((fun (f : a ⟶ b) ↦ mk f) f) ((fun (f : a ⟶ b) ↦ mk f) g)
change : (mk f).hom = (mk g).hom
⊢ f = g

Tactic:
change (Arrow.mk f).hom = (Arrow.mk g).hom

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h_1 : Finite.{u + 1} (Arrow C)
a b : C
f g : a ⟶ b
h : Eq.{u + 1} (α := Arrow C) ((fun (f : a ⟶ b) ↦ mk f) f) ((fun (f : a ⟶ b) ↦ mk f) g)
⊢ (mk f).hom = (mk g).hom

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
a b : C
⊢ Finite.{u + 1} (a ⟶ b)

Tactic:
have := Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
        (fun f g h ↦ by
          change (Arrow.mk f).hom = (Arrow.mk g).hom
          congr)
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
a b : C
this : Finite.{u + 1} (a ⟶ b)
⊢ Fintype (a ⟶ b)

Tactic:
apply Fintype.ofFinite

Premises used: Fintype.ofFinite
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
val : FinCategory C
mpr : ∀ (this : Fintype (Arrow C)), Finite.{u + 1} (Arrow C)
⊢ Finite.{u + 1} (Arrow C)

Tactic:
have := Fintype.ofEquiv _ (Arrow.equivSigma C).symm
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
val : FinCategory C
this : Fintype (Arrow C)
⊢ Finite.{u + 1} (Arrow C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
inst_1 : FinCategory C
rw : Nonempty.{u + 1} (FinCategory C)
⊢ Finite.{u + 1} (Arrow C)

Tactic:
rw [Arrow.finite_iff]

Premises used: CategoryTheory.Arrow.finite_iff
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
inst_1 : FinCategory C
⊢ Nonempty.{u + 1} (FinCategory C)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : SmallCategory C
inst_1 : FinCategory C
⊢ Nonempty.{u + 1} (FinCategory C)

Tactic:
exact ⟨inferInstance⟩
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
⊢ HasCardinalLT (Arrow.{v, u} Cᵒᵖ) κ ↔ HasCardinalLT (Arrow.{v, u} C) κ

Tactic:
hasCardinalLT_iff_of_equiv (Arrow.opEquiv C) κ

Premises used: hasCardinalLT_iff_of_equiv, CategoryTheory.Arrow.opEquiv
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
X : Type u
κ : Cardinal.{w}
⊢ HasCardinalLT.{w, u} (Arrow (Discrete X)) κ ↔ HasCardinalLT X κ

Tactic:
hasCardinalLT_iff_of_equiv (Arrow.discreteEquiv X) κ

Premises used: hasCardinalLT_iff_of_equiv, CategoryTheory.Arrow.discreteEquiv
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
X : Type u
inst : Finite X
⊢ Finite.{u + 1} (Arrow (Discrete X))

Tactic:
Finite.of_equiv _ (Arrow.discreteEquiv X).symm

Premises used: Finite.of_equiv, CategoryTheory.Arrow.discreteEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, max u v} (Arrow.{v, u} C)
⊢ Small.{w, u} C

Tactic:
small_of_injective (f := fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)

Premises used: CategoryTheory.Comma.left, small_of_injective, congr_arg
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, max u v} (Arrow.{v, u} C)
X Y : C
f g : X ⟶ Y
h : Eq (α := Arrow.{v, u} C) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) f) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) g)
change : (Arrow.mk f).hom = (Arrow.mk g).hom
⊢ f = g

Tactic:
change (Arrow.mk f).hom = (Arrow.mk g).hom

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, max u v} (Arrow.{v, u} C)
X Y : C
f g : X ⟶ Y
h : Eq (α := Arrow.{v, u} C) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) f) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) g)
⊢ (Arrow.mk f).hom = (Arrow.mk g).hom

Tactic:
congr