awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 }
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 }
⊢ { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } = y

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 }
mk :
  ∀ (hom_2 : S.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit T) right_1)
    (hh :
      S.map (eqToHom ⋯) ≫
          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 }
⊢ { left := left, right := right, hom := hom : Comma S (Functor.fromPUnit T) } =
    { left := left_1, right := right_1, hom := hom_1 }

Tactic:
cases hl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
A B : CostructuredArrow S T
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
CommaMorphism.ext h (Subsingleton.elim _ _)

Premises used: CategoryTheory.CommaMorphism.ext, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
A B : CostructuredArrow S T
f g : A ⟶ B
⊢ f = g ↔ f.left = g.left

Tactic:
⟨fun h => h ▸ rfl, ext f g⟩

Premises used: CategoryTheory.CostructuredArrow.ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
A B : CostructuredArrow S T
f : A ⟶ B
h : Mono f.left
⊢ Mono f

Tactic:
(proj S T).mono_of_mono_map h

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
A B : CostructuredArrow S T
f : A ⟶ B
h : Epi f.left
⊢ Epi f

Tactic:
(proj S T).epi_of_epi_map h

Premises used: CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 B : CostructuredArrow S T
f : A.left ⟶ B.left
w : S.map f ≫ B.hom = A.hom
h : Mono f
⊢ Mono (homMk f w)

Tactic:
(proj S T).mono_of_mono_map h

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 B : CostructuredArrow S T
f : A.left ⟶ B.left
w : S.map f ≫ B.hom = A.hom
h : Epi f
⊢ Epi (homMk f w)

Tactic:
(proj S T).epi_of_epi_map h

Premises used: CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
⊢ f = mk f.hom

Tactic:
rfl

Premises used: CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
⊢ ∃ (Y : C) (g : S.obj Y ⟶ T), f = mk g

Tactic:
⟨_, _, eq_mk f⟩

Premises used: CategoryTheory.CostructuredArrow.eq_mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' : D
Y : C
S : Functor.{v₁, v₂, u₁, u₂} C D
f : S.obj Y ⟶ T
g : T ⟶ T'
⊢ Functor.obj (map g) (mk f) = mk (f ≫ g)

Tactic:
rfl

Premises used: CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
rw : Functor.obj (map (𝟙 T)) (mk f.hom) = mk f.hom
⊢ Functor.obj (map (𝟙 T)) f = f

Tactic:
rw [eq_mk f]

Premises used: CategoryTheory.CostructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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)) (mk f.hom) = mk f.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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
rw : Functor.obj (map (f ≫ f')) (mk h.hom) = Functor.obj (map f') (Functor.obj (map f) (mk h.hom))
⊢ Functor.obj (map (f ≫ f')) h = Functor.obj (map f') (Functor.obj (map f) h)

Tactic:
rw [eq_mk h]

Premises used: CategoryTheory.CostructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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')) (mk h.hom) = Functor.obj (map f') (Functor.obj (map f) (mk h.hom))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 B : CostructuredArrow S T
f : A ⟶ B
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) ⋯ = 𝟙 A ∧ homMk (inv ((proj S T).map f)) ⋯ ≫ f = 𝟙 B

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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))))
h : m.left = (homMk (S.preimage c.pt.hom) ⋯).left
⊢ m = homMk (S.preimage c.pt.hom) ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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))))
h : S.map m.left = S.map (homMk (S.preimage c.pt.hom) ⋯).left
⊢ m.left = (homMk (S.preimage c.pt.hom) ⋯).left

Tactic:
apply S.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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))))
⊢ S.map m.left = S.map (homMk (S.preimage c.pt.hom) ⋯).left

Tactic:
simpa only [homMk_left, S.map_preimage, ← w m] using (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.w, CategoryTheory.CostructuredArrow.homMk_left, Eq.symm, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : D
inst_4 : F.Faithful
⊢ (pre F G S).Faithful

Tactic:
show (Comma.preLeft _ _ _).Faithful from inferInstance

Premises used: inferInstance, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.pre
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : D
inst_4 : F.Full
⊢ (pre F G S).Full

Tactic:
show (Comma.preLeft _ _ _).Full from inferInstance

Premises used: inferInstance, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.pre
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : D
inst_4 : F.EssSurj
⊢ (pre F G S).EssSurj

Tactic:
show (Comma.preLeft _ _ _).EssSurj from inferInstance

Premises used: inferInstance, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.pre
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : D
inst_4 : F.IsEquivalence
⊢ (pre F G S).IsEquivalence

Tactic:
Comma.isEquivalence_preLeft _ _ _

Premises used: CategoryTheory.CostructuredArrow, CategoryTheory.Comma.isEquivalence_preLeft, CategoryTheory.CostructuredArrow.pre
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : C
X Y_1 : CostructuredArrow F S
f : X ⟶ Y_1
⊢ Eq (α := (F ⋙ G).obj (mk (G.map X.hom)).left ⟶ G.obj S) ((F ⋙ G).map f.left ≫ (mk (G.map Y_1.hom)).hom)
    (mk (G.map X.hom)).hom

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : C
x x_1 : CostructuredArrow F S
x_2 x_3 : x ⟶ x_1
h : (post F G S).map x_2 = (post F G S).map x_3
⊢ x_2 = x_3

Tactic:
simpa [ext_iff] using h

Premises used: CategoryTheory.CostructuredArrow.ext_iff
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : C
inst_4 : G.Faithful
X Y_1 : CostructuredArrow F S
f : (post F G S).obj X ⟶ (post F G S).obj Y_1
⊢ G.map (F.map f.left ≫ Y_1.hom) = G.map X.hom

Tactic:
simpa using f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : C
inst_4 : G.Faithful
X Y_1 : CostructuredArrow F S
f : (post F G S).obj X ⟶ (post F G S).obj Y_1
⊢ (post F G S).map (homMk f.left ⋯) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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_1 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
F : Functor.{v₄, v₁, u₄, u₁} B C
G : Functor.{v₁, v₂, u₁, u₂} C D
S : C
inst_4 : G.Full
h : CostructuredArrow (F ⋙ G) (G.obj S)
⊢ (F ⋙ G).map (Iso.hom (Iso.refl ((post F G S).obj (mk (G.preimage h.hom))).left)) ≫ h.hom =
    ((post F G S).obj (mk (G.preimage h.hom))).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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.Faithful
⊢ (map₂ α β).Faithful

Tactic:
apply Comma.faithful_map

Premises used: CategoryTheory.Comma.faithful_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
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}) ↦ β)
⊢ (map₂ α β).Full

Tactic:
apply +allowSynthFailures Comma.full_map

Premises used: CategoryTheory.Comma.full_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
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)
⊢ 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:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : G.Faithful
inst_6 : F.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso β
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 β
X : Discrete PUnit.{1}
⊢ IsIso β

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
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}) ↦ β)
⊢ (map₂ α β).EssSurj

Tactic:
apply +allowSynthFailures Comma.essSurj_map

Premises used: CategoryTheory.Comma.essSurj_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
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)
⊢ 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:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : F.EssSurj
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso β
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
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 β
X : Discrete PUnit.{1}
⊢ IsIso β

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
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}) ↦ β)
⊢ (map₂ α β).IsEquivalence

Tactic:
apply +allowSynthFailures Comma.isEquivalenceMap

Premises used: CategoryTheory.Comma.isEquivalenceMap
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : 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_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : 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_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
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)
⊢ 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:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app