awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf :
  Mono.{v_2, u_2} (C := D) (X := F.obj X) (Y := Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ F'.obj Y) → F.obj X ⟶ Y)
        ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f) :
      F.obj X ⟶ Y)
inst_2 : F.ReflectsMonomorphisms
⊢ Mono (X := F.obj X) (Y := F.obj (F'.obj Y)) (F.map ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f))

Tactic:
mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

Premises used: CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.mono_of_mono_fac, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf :
  Mono.{v_2, u_2} (C := D) (X := F.obj X) (Y := Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ F'.obj Y) → F.obj X ⟶ Y)
        ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f) :
      F.obj X ⟶ Y)
inst_2 : F.ReflectsMonomorphisms
⊢ Mono (X := F.obj X) (Y := F.obj (F'.obj Y)) (F.map ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f))

Tactic:
exact mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

Premises used: CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.mono_of_mono_fac, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A B : C
f : A ⟶ B
inst_2 : F.IsEquivalence
mp : StrongEpi (F.map f) → StrongEpi f
mpr : StrongEpi f → StrongEpi (F.map f)
⊢ StrongEpi (F.map f) ↔ StrongEpi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A B : C
f : A ⟶ B
inst_2 : F.IsEquivalence
h : StrongEpi (F.map f)
mp : ∀ (e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))), StrongEpi f
⊢ StrongEpi f

Tactic:
have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A B : C
f : A ⟶ B
inst_2 : F.IsEquivalence
h : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
mp : StrongEpi (F.inv.map (F.map f))
⊢ StrongEpi f

Tactic:
rw [StrongEpi.iff_of_arrow_iso e]

Premises used: CategoryTheory.StrongEpi.iff_of_arrow_iso
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A B : C
f : A ⟶ B
inst_2 : F.IsEquivalence
h : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A B : C
f : A ⟶ B
inst_2 : F.IsEquivalence
h : StrongEpi f
⊢ StrongEpi (F.map f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ RepresentablyFlat.{v₁, v₁, u₁, u₁} (𝟭 C)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ RepresentablyCoflat.{v₁, v₁, u₁, u₁} (𝟭 C)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
⊢ RepresentablyFlat (F ⋙ G)

Tactic:
⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.IsCofiltered.of_cone_nonempty, CategoryTheory.RepresentablyFlat.mk, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
refine :
  ∀ (X : E) {J : Type} (x : SmallCategory J) (x_1 : FinCategory J) (H : J ⥤ StructuredArrow X (F ⋙ G)),
    Nonempty (Cone H)
⊢ RepresentablyFlat (F ⋙ G)

Tactic:
refine ⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
X : E
J : Type
x : SmallCategory J
x_1 : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
obtain : ∀ (c₁ : Cone (H ⋙ StructuredArrow.pre X F G)), Nonempty (Cone H)
⊢ Nonempty (Cone H)

Tactic:
obtain ⟨c₁⟩ := IsCofiltered.cone_nonempty (H ⋙ StructuredArrow.pre X F G)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.IsCofiltered.cone_nonempty, CategoryTheory.StructuredArrow.pre
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
X : E
J : Type
x : SmallCategory J
x_1 : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
    map_comp := ⋯ }
obtain : ∀ (c₂ : Cone H₂), Nonempty (Cone H)
⊢ Nonempty (Cone H)

Tactic:
obtain ⟨c₂⟩ := IsCofiltered.cone_nonempty H₂

Premises used: CategoryTheory.IsCofiltered.cone_nonempty
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
X : E
J : Type
x : SmallCategory J
x_1 : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
    map_comp := ⋯ }
c₂ :
  Cone (J := J) (C := StructuredArrow c₁.pt.right F)
    { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
      map_comp := ⋯ }
j : J
⊢ (Functor.obj (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) j).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (c₂.π.app j)) =
    (H.obj j).hom

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
X : E
J : Type
x : SmallCategory J
x_1 : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
    map_comp := ⋯ }
c₂ :
  Cone (J := J) (C := StructuredArrow c₁.pt.right F)
    { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
      map_comp := ⋯ }
j j' : J
f : j ⟶ j'
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) j ⟶ H.obj j')
    (CategoryStruct.comp (Y :=
        Functor.obj (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) j')
        (Functor.map (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) f)
        ((fun (j : J) ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (c₂.π.app j)) ⋯) j') :
      Functor.obj (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) j ⟶ H.obj j')
    ((fun (j : J) ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (c₂.π.app j)) ⋯) j ≫ H.map f :
      Functor.obj (Functor.obj (Functor.const J) (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))) j ⟶ H.obj j')

Tactic:
simpa using (c₂.w f).symm

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
X : E
J : Type
x : SmallCategory J
x_1 : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
    map_comp := ⋯ }
c₂ :
  Cone (J := J) (C := StructuredArrow c₁.pt.right F)
    { obj := fun (j : J) ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j' : J} (f : j ⟶ j') ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯,
      map_comp := ⋯ }
⊢ Nonempty (Cone H)

Tactic:
exact ⟨⟨StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom),
    ⟨fun j => StructuredArrow.homMk (c₂.π.app j).right (by simp [← G.map_comp]),
     fun j j' f => by simpa using (c₂.w f).symm⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F

Tactic:
⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.RepresentablyCoflat.mk, CategoryTheory.CostructuredArrow, _private.0.CategoryTheory.representablyCoflat_op_iff.match_1, Iff.intro, CategoryTheory.IsFiltered, CategoryTheory.RepresentablyFlat.mk
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
refine_1 : RepresentablyCoflat F.op → ∀ (X : D), IsCofiltered (StructuredArrow X F)
refine_2 : RepresentablyFlat F → ∀ (x : Dᵒᵖ) (X : D), IsFiltered (CostructuredArrow F.op (op X))
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyCoflat F.op
X : D
refine_1 : IsFiltered (StructuredArrow X F)ᵒᵖ
⊢ IsCofiltered (StructuredArrow X F)

Tactic:
suffices IsFiltered (StructuredArrow X F)ᵒᵖ from isCofiltered_of_isFiltered_op _
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyCoflat F.op
X : D
⊢ IsFiltered (StructuredArrow X F)ᵒᵖ

Tactic:
apply IsFiltered.of_equivalence (structuredArrowOpEquivalence _ _).symm

Premises used: CategoryTheory.structuredArrowOpEquivalence, CategoryTheory.IsFiltered.of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyFlat F
x : Dᵒᵖ
X : D
refine_2 : IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ
⊢ IsFiltered (CostructuredArrow F.op (op X))

Tactic:
suffices IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ from isFiltered_of_isCofiltered_op _
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyFlat F
x : Dᵒᵖ
X : D
refine_2 : IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ
⊢ IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ

Tactic:
suffices IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ from
      IsCofiltered.of_equivalence (structuredArrowOpEquivalence _ _).op
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyFlat F
x : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ

Tactic:
apply IsCofiltered.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F

Tactic:
⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.RepresentablyCoflat.mk, CategoryTheory.IsCofiltered, _private.0.CategoryTheory.representablyCoflat_op_iff.match_1, Iff.intro, CategoryTheory.RepresentablyFlat.mk, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
refine_1 : RepresentablyFlat F.op → ∀ (X : D), IsFiltered (CostructuredArrow F X)
refine_2 : RepresentablyCoflat F → ∀ (x : Dᵒᵖ) (X : D), IsCofiltered (StructuredArrow (op X) F.op)
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyFlat F.op
X : D
refine_1 : IsCofiltered (CostructuredArrow F X)ᵒᵖ
⊢ IsFiltered (CostructuredArrow F X)

Tactic:
suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyFlat F.op
X : D
⊢ IsCofiltered (CostructuredArrow F X)ᵒᵖ

Tactic:
apply IsCofiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm

Premises used: CategoryTheory.costructuredArrowOpEquivalence, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyCoflat F
x : Dᵒᵖ
X : D
refine_2 : IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ
⊢ IsCofiltered (StructuredArrow (op X) F.op)

Tactic:
suffices IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ from isCofiltered_of_isFiltered_op _
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyCoflat F
x : Dᵒᵖ
X : D
refine_2 : IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ
⊢ IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ

Tactic:
suffices IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ from
      IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).op
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
h : RepresentablyCoflat F
x : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ

Tactic:
apply IsFiltered.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.IsFiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyFlat F
⊢ RepresentablyCoflat F.op

Tactic:
(representablyCoflat_op_iff F).2 inferInstance

Premises used: Iff.mpr, inferInstance, CategoryTheory.representablyCoflat_op_iff
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyCoflat F
⊢ RepresentablyFlat F.op

Tactic:
(representablyFlat_op_iff F).2 inferInstance

Premises used: Iff.mpr, CategoryTheory.representablyFlat_op_iff, inferInstance
-- Module: Mathlib.CategoryTheory.Functor.Flat
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
inst_3 : RepresentablyCoflat F
inst_4 : RepresentablyCoflat G
⊢ RepresentablyCoflat (F ⋙ G)

Tactic:
(representablyFlat_op_iff _).1 <| inferInstanceAs <| RepresentablyFlat (F.op ⋙ G.op)

Premises used: CategoryTheory.representablyFlat_op_iff, _private.0.CategoryTheory.RepresentablyCoflat.comp._proof_1, Iff.mp
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasFiniteLimits.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteLimits F
X : D
apply : ∀ (J : Type v₁) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J (StructuredArrow X F)
⊢ HasFiniteLimits (StructuredArrow X F)

Tactic:
apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasFiniteLimits.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J (StructuredArrow X F)

Tactic:
fun _ _ _ => HasLimitsOfShape.mk

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasFiniteLimits.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J (StructuredArrow X F)

Tactic:
exact fun _ _ _ => HasLimitsOfShape.mk

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasFiniteColimits.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteColimits F
⊢ RepresentablyCoflat F

Tactic:
let _ := preservesFiniteLimits_op F
  (representablyFlat_op_iff _).1 (flat_of_preservesFiniteLimits _)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.preservesFiniteLimits_op, CategoryTheory.representablyFlat_op_iff, Iff.mp, CategoryTheory.flat_of_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
x : J
⊢ lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x

Tactic:
simp [lift, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.PreservesFiniteLimitsOfFlat.lift
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
X : J
⊢ ((F.mapCone c).toStructuredArrow ⋙ map f₁).obj X = s.toStructuredArrow.obj X

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
X : J
⊢ ((F.mapCone c).toStructuredArrow ⋙ map f₂).obj X = s.toStructuredArrow.obj X

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
j : J
⊢ CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left

Tactic:
injection c₀.π.naturality (BiconeHom.left j) with _ e₁

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, CategoryTheory.BiconeHom.left