awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
h₁ : f.left = g.left
⊢ f = g
have h₂ : f.right = g.right
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))
have rw : α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right
Tactic: rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right
have erw : (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right)
Tactic: erw [← α.naturality_assoc, β.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right)
have dsimp : L'.map (F₁.map (F₁.preimage φ.left)) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map (F₂.map (F₂.preimage φ.right))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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.Faithful
inst_7 : F₁.Full
inst_8 : F₂.Full
inst_9 : IsIso α
inst_10 : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ L'.map (F₁.map (F₁.preimage φ.left)) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map (F₂.map (F₂.preimage φ.right))
have rw : L'.map φ.left ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right = α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map φ.right
Tactic: rw [F₁.map_preimage, F₂.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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'
⊢ L'.map (Iso.hom (F₁.objObjPreimageIso X.left)) ≫ X.hom =
    ((map α β).obj
          { left := F₁.objPreimage X.left, right := F₂.objPreimage X.right,
            hom :=
              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)) :
            Comma L R }).hom ≫
      R'.map (Iso.hom (F₂.objObjPreimageIso X.right))
have dsimp : 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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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'
⊢ 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))))
have 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))))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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'
⊢ 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))))
have 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))))
Tactic: rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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))))
⊢ 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))))
have 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))
Tactic: rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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))
⊢ 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))))
have 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))
Tactic: rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
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))
⊢ 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))))
have 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)
Tactic: rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
⊢ Finite.{u + 1} (Arrow C) ↔ Nonempty.{u + 1} (FinCategory C)
have mp : Finite.{u + 1} (Arrow C) → Nonempty.{u + 1} (FinCategory C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
mp : Finite.{u + 1} (Arrow C) → Nonempty.{u + 1} (FinCategory C)
⊢ Finite.{u + 1} (Arrow C) ↔ Nonempty.{u + 1} (FinCategory C)
have mpr : Nonempty.{u + 1} (FinCategory C) → Finite.{u + 1} (Arrow C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
⊢ Nonempty.{u + 1} (FinCategory C)
have mp : Fintype C
Tactic: refine ⟨?_, fun a b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
mp : Fintype C
⊢ Nonempty.{u + 1} (FinCategory C)
have mp₁ : (a b : C) → Fintype (a ⟶ b)
Tactic: refine ⟨?_, fun a b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
⊢ Fintype C
have this : Finite C
Tactic: have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
        (fun _ _ ↦ congr_arg Comma.left)
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
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)
⊢ f = g
have change : (mk f).hom = (mk g).hom
Tactic: change (Arrow.mk f).hom = (Arrow.mk g).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
h : Finite.{u + 1} (Arrow C)
a b : C
⊢ Fintype (a ⟶ b)
have this : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
val : FinCategory C
⊢ Finite.{u + 1} (Arrow C)
have mpr : ∀ (this : Fintype (Arrow C)), Finite.{u + 1} (Arrow C)
Tactic: have := Fintype.ofEquiv _ (Arrow.equivSigma C).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : FinCategory C
⊢ Finite.{u + 1} (Arrow C)
have rw : Nonempty.{u + 1} (FinCategory C)
Tactic: rw [Arrow.finite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
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)
⊢ f = g
have change : (Arrow.mk f).hom = (Arrow.mk g).hom
Tactic: change (Arrow.mk f).hom = (Arrow.mk g).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.CardinalArrow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, w} (Shrink.{w, u} C)
⊢ Eq (α :=
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (left
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
          (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x)))
      (right
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
          (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x))))
    (hom
      (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
        (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x)))
    (eqToHom ⋯ ≫ x.hom ≫ eqToHom ⋯)
have simp : Eq (α :=
  Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
    (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
      (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
    (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
      (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
  (CategoryStruct.comp (Y := x.left) (NatTrans.app (Equivalence.counit (Shrink.equivalence C)) x.left)
      (x.hom ≫ NatTrans.app (Equivalence.counitInv (Shrink.equivalence C)) x.right) :
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
  (eqToHom sorry ≫ x.hom ≫ eqToHom sorry :
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
⊢ (fst L R).Final
have rw : ∀ (G : A ⥤ Type v₁), IsIso (X := colimit (fst L R ⋙ G)) (Y := colimit G) (colimit.pre G (fst L R))
Tactic: rw [Functor.final_iff_isIso_colimit_pre]