awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : 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
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_4 : F.EssSurj
inst_5 : G.Full
inst_6 : IsIso α
inst_7 : IsIso β
⊢ (map₂ α β).EssSurj
have inst : IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := Functor.fromPUnit T ⋙ G) (Y :=
  𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β)
Tactic: apply +allowSynthFailures Comma.essSurj_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : 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
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_4 : F.EssSurj
inst_5 : G.Full
inst_6 : IsIso α
inst_7 : IsIso β
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := Functor.fromPUnit T ⋙ G) (Y :=
    𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β)
have inst : ∀ (X : Discrete PUnit.{1}),
  IsIso.{v₄, u₄} (C := B) (X := (Functor.fromPUnit T ⋙ G).obj X) (Y :=
    Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) X)
    (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β) X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : 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
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_4 : F.IsEquivalence
inst_5 : G.Faithful
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
⊢ (map₂ α β).IsEquivalence
have inst : IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := Functor.fromPUnit T ⋙ G) (Y :=
  𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β)
Tactic: apply +allowSynthFailures Comma.isEquivalenceMap
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : 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
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_4 : F.IsEquivalence
inst_5 : G.Faithful
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := Functor.fromPUnit T ⋙ G) (Y :=
    𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β)
have inst : ∀ (X : Discrete PUnit.{1}),
  IsIso.{v₄, u₄} (C := B) (X := (Functor.fromPUnit T ⋙ G).obj X) (Y :=
    Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) X)
    (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β) X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ η = η'
have rw : h.lift (mk (S.map η ≫ f.hom)) = η'
Tactic: rw [h.hom_desc η, h.hom_desc η', w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
rw : h.lift (mk (S.map η ≫ f.hom)) = η'
⊢ η = η'
have rw₁ : Eq (α := c ⟶ f.left) (h.lift (mk (S.map η ≫ f.hom)) : (mk (S.map η ≫ f.hom)).left ⟶ f.left)
  (h.lift (mk (S.map η' ≫ f.hom)))
Tactic: rw [h.hom_desc η, h.hom_desc η', w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
rw : h.lift (mk (S.map η ≫ f.hom)) = η'
rw₁ :
  Eq (α := c ⟶ f.left) (h.lift (mk (S.map η ≫ f.hom)) : (mk (S.map η ≫ f.hom)).left ⟶ f.left)
    (h.lift (mk (S.map η' ≫ f.hom)))
⊢ η = η'
have rw₂ : Eq (α := c ⟶ f.left) (h.lift (mk (S.map η' ≫ f.hom)) : (mk (S.map η' ≫ f.hom)).left ⟶ f.left)
  (h.lift (mk (S.map η' ≫ f.hom)))
Tactic: rw [h.hom_desc η, h.hom_desc η', w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : StructuredArrow d F
f : op X ⟶ op Y
⊢ Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op X) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op Y)))
    (Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op X)) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
have obtain : ∀ (X : C) (x : d ⟶ F.obj X) (f : op (StructuredArrow.mk x) ⟶ op Y),
  Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op) (op Y)))
    (Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op)
          (op (StructuredArrow.mk x))) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
Tactic: obtain ⟨X, x, rfl⟩ := X.mk_surjective
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
Y : StructuredArrow d F
X : C
x : d ⟶ F.obj X
f : op (StructuredArrow.mk x) ⟶ op Y
⊢ Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op Y)))
    (Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
          (op (StructuredArrow.mk x))) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
have obtain : ∀ (Y : C) (y : d ⟶ F.obj Y) (f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)),
  Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
        (op (StructuredArrow.mk y)))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op)
          (op (StructuredArrow.mk y))))
    (Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op)
          (op (StructuredArrow.mk x))) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
Tactic: obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ Eq (α :=
    unop
        ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
          (op (StructuredArrow.mk y))) ⟶
      unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x))))
    (Quiver.Hom.unop
      (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk x))) ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f))
have h : Eq (α :=
  (unop
        ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
          (op (StructuredArrow.mk y)))).right ⟶
    (unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)))).right)
  (StructuredArrow.Hom.right
    (Quiver.Hom.unop
      (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op)
            (op (StructuredArrow.mk y))))))
  (StructuredArrow.Hom.right
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) sorry).op)
            (op (StructuredArrow.mk x))) ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : CostructuredArrow F d
f : op X ⟶ op Y
⊢ Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op X) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op Y)))
    (Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op X)) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
have obtain : ∀ (X : C) (x : F.obj X ⟶ d) (f : op (CostructuredArrow.mk x) ⟶ op Y),
  Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op) (op Y)))
    (Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op)
          (op (CostructuredArrow.mk x))) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
Tactic: obtain ⟨X, x, rfl⟩ := X.mk_surjective
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
Y : CostructuredArrow F d
X : C
x : F.obj X ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op Y
⊢ Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op Y)))
    (Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
          (op (CostructuredArrow.mk x))) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
have obtain : ∀ (Y : C) (y : F.obj Y ⟶ d) (f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)),
  Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
        (op (CostructuredArrow.mk y)))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op)
          (op (CostructuredArrow.mk y))))
    (Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op)
          (op (CostructuredArrow.mk x))) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
Tactic: obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ Eq (α :=
    unop
        ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
          (op (CostructuredArrow.mk y))) ⟶
      unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x))))
    (Quiver.Hom.unop
      (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk x))) ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f))
have h : Eq (α :=
  (unop
        ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
          (op (CostructuredArrow.mk y)))).left ⟶
    (unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)))).left)
  (CommaMorphism.left
    (Quiver.Hom.unop
      (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op)
            (op (CostructuredArrow.mk y))))))
  (CommaMorphism.left
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) sorry).op)
            (op (CostructuredArrow.mk x))) ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : StructuredArrow e G
X Y : StructuredArrow f (pre e F G)
φ : X ⟶ Y
⊢ (mk (Hom.right X.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) = (mk (Hom.right Y.hom)).hom
have rw : (mk (Hom.right X.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) =
  (mk (Hom.right X.hom ≫ Hom.right ((pre e F G).map (Hom.right φ)))).hom
Tactic: rw [← w φ, comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : CostructuredArrow G e
X Y : CostructuredArrow (pre F G e) f
φ : X ⟶ Y
⊢ F.map φ.left.left ≫ (mk Y.hom.left).hom = (mk X.hom.left).hom
have rw : F.map φ.left.left ≫ (mk Y.hom.left).hom = (mk (((pre F G e).map φ.left).left ≫ Y.hom.left)).hom
Tactic: rw [← w φ, comp_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow S T × StructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X ⟶
      Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y)
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
      Iso.hom
        ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          Y))
    (Iso.hom
        ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          X) ≫
      Functor.map (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f)
have h₁ : Eq (α :=
  ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.right ⟶
    (Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y).1.right)
  (Hom.right
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        Iso.hom
          ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            Y)).1)
  (Hom.right
    (Iso.hom
          ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            X) ≫
        Functor.map (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f).1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
X Y : CostructuredArrow S T × CostructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X ⟶
      Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y)
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
      Iso.hom
        ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          Y))
    (Iso.hom
        ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          X) ≫
      Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f)
have h₁ : Eq (α :=
  ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.left ⟶
    (Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y).1.left)
  (CommaMorphism.left
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        Iso.hom
          ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            Y)).1)
  (CommaMorphism.left
    (Iso.hom
          ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            X) ≫
        Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f).1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (goal)
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
inst_4 : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
⊢ L.Final
have rw : ∀ (G : T ⥤ Type u₁), IsIso (X := colimit (L ⋙ G)) (Y := colimit G) (colimit.pre G L)
Tactic: rw [final_iff_isIso_colimit_pre]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (hypothesis)
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
inst_4 : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
G : T ⥤ Type u₁
⊢ IsIso (X := colimit (L ⋙ G)) (Y := colimit G) (colimit.pre G L)
have this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
Tactic: have : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b).toFunctor := fun b =>
    inferInstanceAs (Final (CostructuredArrow.toOver L (R.obj b)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (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
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
⊢ Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
have dsimp : Final (C := CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
  (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
Tactic: dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢