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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ Hom.right f = Hom.right g
have rw : Hom.right g = Hom.right g
Tactic: rw [h]
-- 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
S S' S'' : D
Y_1 Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
h : X = Y
⊢ X.right = Y.right
have rw : Y.right = Y.right
Tactic: rw [h]
-- 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯
have subst : Hom.right (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
x y : StructuredArrow S T
hr : x.right = y.right
hh : x.hom ≫ T.map (eqToHom hr) = y.hom
⊢ x = y
have mk : ∀ (left : Discrete PUnit.{1}) (right : C) (hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right)
  (hr : StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y.right)
  (hh :
    StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
        T.map (eqToHom hr) =
      y.hom),
  { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y
Tactic: cases x
Cleared hypotheses: x, hr, hh
-- 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
y : StructuredArrow S T
left : Discrete PUnit.{1}
right : C
hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right
hr : StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y.right
hh :
  StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
      T.map (eqToHom hr) =
    y.hom
⊢ { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } = y
have mk : ∀ (left_1 : Discrete PUnit.{1}) (right_1 : C)
  (hom_1 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right_1)
  (hr :
    StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
      StructuredArrow.right { left := left_1, right := right_1, hom := hom_1 : Comma (Functor.fromPUnit S) T })
  (hh :
    StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
        T.map (eqToHom hr) =
      StructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 }),
  { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    { left := left_1, right := right_1, hom := hom_1 }
Tactic: cases y
Cleared hypotheses: y, hr, hh
-- 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
left : Discrete PUnit.{1}
right : C
hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left ⟶ T.obj right
left_1 : Discrete PUnit.{1}
right_1 : C
hom_1 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right_1
hr :
  StructuredArrow.right { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    StructuredArrow.right { left := left_1, right := right_1, hom := hom_1 : Comma (Functor.fromPUnit S) T }
hh :
  StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
      T.map (eqToHom hr) =
    StructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 }
⊢ { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    { left := left_1, right := right_1, hom := hom_1 }
have mk : ∀ (hom_2 : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit S) left_1 ⟶ T.obj right)
  (hh :
    StructuredArrow.hom { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } ≫
        T.map (eqToHom sorry) =
      StructuredArrow.hom { left := left_1, right := right, hom := hom_2 }),
  { left := left, right := right, hom := hom : Comma (Functor.fromPUnit S) T } =
    { left := left_1, right := right, hom := hom_2 }
Tactic: cases hr
Cleared hypotheses: right_1, hom_1, hr, hh
-- 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
⊢ Functor.obj (map (𝟙 S)) f = f
have rw : Functor.obj (map (𝟙 S)) (mk f.hom) = mk f.hom
Tactic: rw [eq_mk 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
S S' S'' : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ Functor.obj (map (f ≫ f')) h = Functor.obj (map f) (Functor.obj (map f') h)
have rw : Functor.obj (map (f ≫ f')) (mk h.hom) = Functor.obj (map f) (Functor.obj (map f') (mk h.hom))
Tactic: rw [eq_mk h]
-- 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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
⊢ m = homMk (T.preimage c.pt.hom) ⋯
have left : m.left = (homMk (T.preimage c.pt.hom) sorry).left
Tactic: apply CommaMorphism.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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
left : m.left = (homMk (T.preimage c.pt.hom) ⋯).left
⊢ m = homMk (T.preimage c.pt.hom) ⋯
have right : m.right = (homMk (T.preimage c.pt.hom) sorry).right
Tactic: apply CommaMorphism.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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : T.Full
inst_3 : T.Faithful
c : Cocone (C := StructuredArrow (T.obj Y) T) (Functor.empty (StructuredArrow (T.obj Y) T))
m : Cocone.pt (asEmptyCocone (mk (𝟙 (T.obj Y)))) ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{1}), NatTrans.app (Cocone.ι (asEmptyCocone (mk (𝟙 (T.obj Y))))) j ≫ m = c.ι.app j
⊢ m.right = (homMk (T.preimage c.pt.hom) ⋯).right
have right : T.map m.right = T.map (homMk (T.preimage c.pt.hom) sorry).right
Tactic: apply T.map_injective
-- 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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : G.Faithful
inst_5 : F.Full
inst_6 : IsIso α
inst_7 : IsIso β
⊢ (map₂ α β).Full
have inst : IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
  Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
Tactic: apply +allowSynthFailures Comma.full_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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst_4 : G.Faithful
inst_5 : F.Full
inst_6 : IsIso α
inst_7 : IsIso β
⊢ IsIso (C := Functor.{0, v₄, 0, u₄} (Discrete PUnit.{1}) B) (X := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
have inst : ∀ (X : Discrete PUnit.{1}),
  IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj 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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
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 := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
  Functor.fromPUnit L ⋙ G) (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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
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 := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
have inst : ∀ (X : Discrete PUnit.{1}),
  IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj 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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
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 := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
  Functor.fromPUnit L ⋙ G) (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
S S' S'' : D
Y Y' Y'' : C
T T' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
L : D
R : Functor.{v₁, v₂, u₁, u₂} C D
L' : B
R' : Functor.{v₃, v₄, u₃, u₄} A B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
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 := 𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') (Y :=
    Functor.fromPUnit L ⋙ G) (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ α)
have inst : ∀ (X : Discrete PUnit.{1}),
  IsIso.{v₄, u₄} (C := B) (X := Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit L') X) (Y :=
    (Functor.fromPUnit L ⋙ G).obj 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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ η = η'
have rw : h.desc (mk (f.hom ≫ T.map η)) = η'
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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
rw : h.desc (mk (f.hom ≫ T.map η)) = η'
⊢ η = η'
have rw₁ : Eq (α := f.right ⟶ c) (h.desc (mk (f.hom ≫ T.map η)) : f.right ⟶ (mk (f.hom ≫ T.map η)).right)
  (h.desc (mk (f.hom ≫ T.map η')))
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
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
rw : h.desc (mk (f.hom ≫ T.map η)) = η'
rw₁ :
  Eq (α := f.right ⟶ c) (h.desc (mk (f.hom ≫ T.map η)) : f.right ⟶ (mk (f.hom ≫ T.map η)).right)
    (h.desc (mk (f.hom ≫ T.map η')))
⊢ η = η'
have rw₂ : Eq (α := f.right ⟶ c) (h.desc (mk (f.hom ≫ T.map η')) : f.right ⟶ (mk (f.hom ≫ T.map η')).right)
  (h.desc (mk (f.hom ≫ T.map η')))
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
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ f.left = g.left
have rw : g.left = g.left
Tactic: rw [h]
-- 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_1 Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left
have rw : Y.left = Y.left
Tactic: rw [h]
-- 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
X Y : CostructuredArrow S T
h : X = Y
⊢ CommaMorphism.left (eqToHom h) = eqToHom ⋯
have subst : CommaMorphism.left (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- 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
x y : CostructuredArrow S T
hl : x.left = y.left
hh : S.map (eqToHom hl) ≫ y.hom = x.hom
⊢ x = y
have mk : ∀ (left : C) (right : Discrete PUnit.{1}) (hom : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right)
  (hl : CostructuredArrow.left { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y.left)
  (hh : S.map (eqToHom hl) ≫ y.hom = CostructuredArrow.hom { left := left, right := right, hom := hom }),
  { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y
Tactic: cases x
Cleared hypotheses: x, hl, hh
-- 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
y : CostructuredArrow S T
left : C
right : Discrete PUnit.{1}
hom : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right
hl : CostructuredArrow.left { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y.left
hh : S.map (eqToHom hl) ≫ y.hom = CostructuredArrow.hom { left := left, right := right, hom := hom }
⊢ { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y
have mk : ∀ (left_1 : C) (right_1 : Discrete PUnit.{1})
  (hom_1 : S.obj left_1 ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right_1)
  (hl :
    CostructuredArrow.left { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
      CostructuredArrow.left { left := left_1, right := right_1, hom := hom_1 : Comma S (Functor.fromPUnit T) })
  (hh :
    S.map (eqToHom hl) ≫
        CostructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 : Comma S (Functor.fromPUnit T) } =
      CostructuredArrow.hom { left := left, right := right, hom := hom }),
  { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
    { left := left_1, right := right_1, hom := hom_1 }
Tactic: cases y
Cleared hypotheses: y, hl, hh
-- 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
left : C
right : Discrete PUnit.{1}
hom : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right
left_1 : C
right_1 : Discrete PUnit.{1}
hom_1 : S.obj left_1 ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right_1
hl :
  CostructuredArrow.left { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
    CostructuredArrow.left { left := left_1, right := right_1, hom := hom_1 : Comma S (Functor.fromPUnit T) }
hh :
  S.map (eqToHom hl) ≫
      CostructuredArrow.hom { left := left_1, right := right_1, hom := hom_1 : Comma S (Functor.fromPUnit T) } =
    CostructuredArrow.hom { left := left, right := right, hom := hom }
⊢ { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
    { left := left_1, right := right_1, hom := hom_1 }
have mk : ∀ (hom_2 : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right_1)
  (hh :
    S.map (eqToHom sorry) ≫
        CostructuredArrow.hom { left := left, right := right_1, hom := hom_2 : Comma S (Functor.fromPUnit T) } =
      CostructuredArrow.hom { left := left, right := right, hom := hom }),
  { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
    { left := left, right := right_1, hom := hom_2 }
Tactic: cases hl
Cleared hypotheses: left_1, hom_1, hl, hh
-- 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
⊢ Functor.obj (map (𝟙 T)) f = f
have rw : Functor.obj (map (𝟙 T)) (mk f.hom) = mk f.hom
Tactic: rw [eq_mk 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
T T' T'' : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ Functor.obj (map (f ≫ f')) h = Functor.obj (map f') (Functor.obj (map f) h)
have rw : Functor.obj (map (f ≫ f')) (mk h.hom) = Functor.obj (map f') (Functor.obj (map f) (mk h.hom))
Tactic: rw [eq_mk h]
-- 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
inst_2 : S.Full
inst_3 : S.Faithful
c : Cone (C := CostructuredArrow S (S.obj Y)) (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ Cone.pt (asEmptyCone (mk (𝟙 (S.obj Y))))
⊢ m = homMk (S.preimage c.pt.hom) ⋯
have h : m.left = (homMk (S.preimage c.pt.hom) sorry).left
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
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : S.Full
inst_3 : S.Faithful
c : Cone (C := CostructuredArrow S (S.obj Y)) (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ Cone.pt (asEmptyCone (mk (𝟙 (S.obj Y))))
⊢ m.left = (homMk (S.preimage c.pt.hom) ⋯).left
have h : S.map m.left = S.map (homMk (S.preimage c.pt.hom) sorry).left
Tactic: apply S.map_injective
-- 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 : G.Faithful
inst_5 : F.Full
inst_6 : IsIso α
inst_7 : IsIso β
⊢ (map₂ α β).Full
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.full_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 : G.Faithful
inst_5 : F.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]