awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
rw : F.map (g ≫ f) = F.map h ≫ F.map f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f
have rw₁ : F.map (h ≫ f) = F.map h ≫ F.map f
Tactic: rw [← F.map_comp, hgh, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
rw : F.map (g ≫ f) = F.map h ≫ F.map f
rw₁ : F.map (h ≫ f) = F.map h ≫ F.map f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f
have rw₂ : F.map h ≫ F.map f = F.map h ≫ F.map f
Tactic: rw [← F.map_comp, hgh, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Epi (F.map f)
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
⊢ F.map f ≫ F.map g = F.map f ≫ F.map h
have rw : F.map (f ≫ g) = F.map f ≫ F.map h
Tactic: rw [← F.map_comp, hgh, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Epi (F.map f)
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
rw : F.map (f ≫ g) = F.map f ≫ F.map h
⊢ F.map f ≫ F.map g = F.map f ≫ F.map h
have rw₁ : F.map (f ≫ h) = F.map f ≫ F.map h
Tactic: rw [← F.map_comp, hgh, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Epi (F.map f)
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
rw : F.map (f ≫ g) = F.map f ≫ F.map h
rw₁ : F.map (f ≫ h) = F.map f ≫ F.map h
⊢ F.map f ≫ F.map g = F.map f ≫ F.map h
have rw₂ : F.map f ≫ F.map h = F.map f ≫ F.map h
Tactic: rw [← F.map_comp, hgh, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitEpi (F.map f)
⊢ F.preimage s.section_ ≫ f = 𝟙 Y
have a : F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitEpi (F.map f)
⊢ F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)
have a : s.section_ ≫ F.map f = 𝟙 (F.obj Y)
Tactic: simp only [map_comp, map_preimage, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f
have mp : IsSplitEpi (F.map f) → IsSplitEpi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
mp : IsSplitEpi (F.map f) → IsSplitEpi f
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f
have mpr : IsSplitEpi f → IsSplitEpi (F.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitMono (F.map f)
⊢ f ≫ F.preimage s.retraction = 𝟙 X
have a : F.map (f ≫ F.preimage s.retraction) = F.map (𝟙 X)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitMono (F.map f)
⊢ F.map (f ≫ F.preimage s.retraction) = F.map (𝟙 X)
have a : F.map f ≫ s.retraction = 𝟙 (F.obj X)
Tactic: simp only [map_comp, map_preimage, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
⊢ IsSplitMono (F.map f) ↔ IsSplitMono f
have mp : IsSplitMono (F.map f) → IsSplitMono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
mp : IsSplitMono (F.map f) → IsSplitMono f
⊢ IsSplitMono (F.map f) ↔ IsSplitMono f
have mpr : IsSplitMono f → IsSplitMono (F.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) ↔ Epi f
have mp : Epi (F.map f) → Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
mp : Epi (F.map f) → Epi f
⊢ Epi (F.map f) ↔ Epi f
have mpr : Epi f → Epi (F.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) ↔ Mono f
have mp : Mono (F.map f) → Mono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
mp : Mono (F.map f) → Mono f
⊢ Mono (F.map f) ↔ Mono f
have mpr : Mono f → Mono (F.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
inst_3 : SplitEpiCategory.{v₁, u₁} C
X Y : D
f : X ⟶ Y
inst_4 : Epi f
⊢ IsSplitEpi f
have rw : IsSplitEpi (F.inv.map f)
Tactic: rw [← F.inv.isSplitEpi_iff f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
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'
f : A ⟶ B
inst_2 : F'.PreservesMonomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : StrongEpi f
X Y : D
Z : X ⟶ Y
inst_5 : Mono Z
⊢ HasLiftingProperty (F.map f) Z
have rw : HasLiftingProperty f (F'.map Z)
Tactic: rw [adj.hasLiftingProperty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (hypothesis)
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 f
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))
have 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)
Tactic: rw [← (homEquiv adj X Y).symm_apply_apply f] at hf
Cleared hypotheses: hf, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
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
⊢ StrongEpi (F.map f) ↔ StrongEpi f
have mp : StrongEpi (F.map f) → StrongEpi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
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
⊢ StrongEpi (F.map f) ↔ StrongEpi f
have mpr : StrongEpi f → StrongEpi (F.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
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)
⊢ StrongEpi f
have mp : ∀ (e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
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
have mp : StrongEpi (F.inv.map (F.map f))
Tactic: rw [StrongEpi.iff_of_arrow_iso e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : RepresentablyFlat F
inst_4 : RepresentablyFlat G
⊢ RepresentablyFlat (F ⋙ G)
have refine : ∀ (X : E) {J : Type} (x : SmallCategory J) (x_1 : FinCategory J) (H : J ⥤ StructuredArrow X (F ⋙ G)), Nonempty (Cone H)
Tactic: refine ⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
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)
⊢ Nonempty (Cone H)
have obtain : ∀ (c₁ : Cone (H ⋙ StructuredArrow.pre X F G)), Nonempty (Cone H)
Tactic: obtain ⟨c₁⟩ := IsCofiltered.cone_nonempty (H ⋙ StructuredArrow.pre X F G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
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 := ⋯ }
⊢ Nonempty (Cone H)
have obtain : ∀ (c₂ : Cone H₂), Nonempty (Cone H)
Tactic: obtain ⟨c₂⟩ := IsCofiltered.cone_nonempty H₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F
have refine_1 : RepresentablyCoflat F.op → ∀ (X : D), IsCofiltered (StructuredArrow X F)
Tactic: refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 : RepresentablyCoflat F.op → ∀ (X : D), IsCofiltered (StructuredArrow X F)
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F
have refine_2 : RepresentablyFlat F → ∀ (x : Dᵒᵖ) (X : D), IsFiltered (CostructuredArrow F.op (op X))
Tactic: refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)
have refine_1 : IsFiltered (StructuredArrow X F)ᵒᵖ
Tactic: suffices IsFiltered (StructuredArrow X F)ᵒᵖ from isCofiltered_of_isFiltered_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyFlat F
x : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))
have refine_2 : IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ
Tactic: suffices IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ from isFiltered_of_isCofiltered_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyFlat F
x : Dᵒᵖ
X : D
⊢ IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ
have refine_2 : IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ
Tactic: suffices IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ from
      IsCofiltered.of_equivalence (structuredArrowOpEquivalence _ _).op
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F
have refine_1 : RepresentablyFlat F.op → ∀ (X : D), IsFiltered (CostructuredArrow F X)
Tactic: refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 : RepresentablyFlat F.op → ∀ (X : D), IsFiltered (CostructuredArrow F X)
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F
have refine_2 : RepresentablyCoflat F → ∀ (x : Dᵒᵖ) (X : D), IsCofiltered (StructuredArrow (op X) F.op)
Tactic: refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)
have refine_1 : IsCofiltered (CostructuredArrow F X)ᵒᵖ
Tactic: suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyCoflat F
x : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)
have refine_2 : IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ
Tactic: suffices IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ from isCofiltered_of_isFiltered_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : RepresentablyCoflat F
x : Dᵒᵖ
X : D
⊢ IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ
have refine_2 : IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ
Tactic: suffices IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ from
      IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).op
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ HasFiniteLimits (StructuredArrow X F)
have apply : ∀ (J : Type v₁) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J (StructuredArrow X F)
Tactic: apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have left_eq : 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₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
left_eq :
  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
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have e₁ : CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
    CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
  CommaMorphism.right (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
Tactic: injection c₀.π.naturality (BiconeHom.left j) with _ e₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
left_eq :
  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
e₁ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have left_eq : CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
    CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
  CommaMorphism.left (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
Tactic: injection c₀.π.naturality (BiconeHom.right j) with _ e₂