awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True

Tactic:
⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom,
      StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_,
      StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_, trivial⟩

Premises used: CategoryTheory.StructuredArrow.homMk, trivial, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, CategoryTheory.IsCofiltered.minToRight, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, CategoryTheory.IsCofiltered.min, CategoryTheory.IsCofiltered.minToLeft, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
refine_1 :
  CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToLeft A' B')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right ⟶ (F ⋙ G).obj A.right) =
    A.hom
refine_1₁ :
  CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right ⟶ (F ⋙ G).obj B.right) =
    B.hom
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True

Tactic:
refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom,
      StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_,
      StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_, trivial⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToLeft A' B')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right ⟶ (F ⋙ G).obj A.right) =
    A.hom

Tactic:
simp [← Functor.map_comp, A', T]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).right ⟶ (F ⋙ G).obj B.right) =
    B.hom

Tactic:
simp [← Functor.map_comp, B', T]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (h : W ⟶ A), h ≫ f = h ≫ g

Tactic:
⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, CategoryTheory.IsCofiltered.eqHom, CategoryTheory.IsCofiltered.eq, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
refine_2 :
  CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ (F ⋙ G).obj A.right) =
    A.hom
refine_2₁ :
  Eq (α := StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
    (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f :
      StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
    (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g :
      StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (h : W ⟶ A), h ≫ f = h ≫ g

Tactic:
refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ CategoryStruct.comp (Y := (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right)
      ((StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).hom :
        X ⟶ (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right)
      ((F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) :
        (F ⋙ G).obj (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ (F ⋙ G).obj A.right) =
    A.hom

Tactic:
simp [← Functor.map_comp, A', T]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
refine_2 :
  Eq (α := (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
⊢ Eq (α := StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
    (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f :
      StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
    (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g :
      StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ Eq (α := (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)

Tactic:
congr($(IsCofiltered.eq_condition f' g').right)

Premises used: congrArg, id, CategoryTheory.IsCofiltered.eq_condition, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A_1 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ Eq (α := (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
    (StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g) :
      (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)

Tactic:
exact congr($(IsCofiltered.eq_condition f' g').right)
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyCoflat F
h : IsFiltered (CostructuredArrow G X)
rw : ∀ (h : IsCofiltered (StructuredArrow (op X) G.op)), IsCofiltered (StructuredArrow (op X) (F ⋙ G).op)
⊢ IsFiltered (CostructuredArrow (F ⋙ G) X)

Tactic:
rw [← isCofiltered_op_iff_isFiltered, IsCofiltered.iff_of_equivalence
    (costructuredArrowOpEquivalence _ _)] at h ⊢

Premises used: CategoryTheory.costructuredArrowOpEquivalence, CategoryTheory.IsCofiltered.iff_of_equivalence, CategoryTheory.isCofiltered_op_iff_isFiltered
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyCoflat F
h : IsCofiltered (StructuredArrow (op X) G.op)
⊢ IsCofiltered (StructuredArrow (op X) (F ⋙ G).op)

Tactic:
inferInstanceAs <| IsCofiltered (StructuredArrow (op X) (F.op ⋙ G.op))

Premises used: _private.0.CategoryTheory.instIsFilteredCostructuredArrowCompOfRepresentablyCoflat._proof_1
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyCoflat F
h : IsCofiltered (StructuredArrow (op X) G.op)
⊢ IsCofiltered (StructuredArrow (op X) (F ⋙ G).op)

Tactic:
exact inferInstanceAs <| IsCofiltered (StructuredArrow (op X) (F.op ⋙ G.op))
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G_1 : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_2, u_4, u_2, u_4 + 1} D (Type u_4)
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered G.Elements
suffices : IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))
⊢ IsCofiltered (F ⋙ G).Elements

Tactic:
suffices h : IsCofiltered (StructuredArrow PUnit (F ⋙ G)) from
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _).symm
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G_1 : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_2, u_4, u_2, u_4 + 1} D (Type u_4)
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered G.Elements
⊢ IsCofiltered (StructuredArrow PUnit.{u_4 + 1} G)

Tactic:
have : IsCofiltered (StructuredArrow PUnit G) :=
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _)
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G_1 : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_2, u_4, u_2, u_4 + 1} D (Type u_4)
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered G.Elements
this : IsCofiltered (StructuredArrow PUnit.{u_4 + 1} G)
⊢ IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
⊢ Function.Injective (α := X ⟶ Y) F.map

Tactic:
Faithful.map_injective

Premises used: CategoryTheory.Functor.Faithful.map_injective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
inst_2 : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
rw rw₁ : F.map g = F.map g
⊢ F.map f = F.map g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
⊢ Function.Injective (α := X ≅ Y) F.mapIso

Tactic:
fun _ _ h =>
  Iso.ext (map_injective F (congr_arg Iso.hom h :))

Premises used: congr_arg, CategoryTheory.Functor.map_injective, Function.Injective, CategoryTheory.Iso.ext, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
⊢ Function.Surjective (α := X ⟶ Y) F.map

Tactic:
Full.map_surjective

Premises used: CategoryTheory.Functor.Full.map_surjective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
inst_2 : F.Full
X Y : C
f : F.obj X ⟶ F.obj Y
⊢ F.map (F.preimage f) = f

Tactic:
(F.map_surjective f).choose_spec

Premises used: CategoryTheory.Functor.preimage, Exists.choose_spec, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
X : C
inst_2 : F.Full
inst_3 : F.Faithful
⊢ F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
X Y Z : C
inst_2 : F.Full
inst_3 : F.Faithful
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
X Y : C
inst_2 : F.Full
inst_3 : F.Faithful
f : X ⟶ Y
⊢ F.map (F.preimage (F.map f)) = F.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X_1 Y_1 : C
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
inst_3 : F.Full
inst_4 : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)

Tactic:
simp