awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
have refine_1 : ∀ (A B : StructuredArrow X (F ⋙ G)), ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True
Tactic: refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
refine_1 : ∀ (A B : StructuredArrow X (F ⋙ G)), ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
have refine_2 : ∀ (A B : StructuredArrow X (F ⋙ G)) (f g : A ⟶ B), ∃ (W : StructuredArrow X (F ⋙ G)) (h : W ⟶ A), h ≫ f = h ≫ g
Tactic: refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
have 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
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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True
have 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
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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
have 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
Tactic: refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ ∃ (W : StructuredArrow X (F ⋙ G)) (h : W ⟶ A), h ≫ f = h ≫ g
have refine_2₁ : Eq (α := StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
  (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) sorry ≫ f :
    StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
  (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) sorry ≫ g :
    StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom) ⟶ B)
Tactic: refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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) ⟶ 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)
have 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')) sorry ≫ 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')) sorry ≫ g) :
    (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.eq f' g').hom)).right ⟶ B.right)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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)
⊢ IsFiltered (CostructuredArrow (F ⋙ G) X)
have rw : ∀ (h : IsCofiltered (StructuredArrow (op X) G.op)), IsCofiltered (StructuredArrow (op X) (F ⋙ G).op)
Tactic: rw [← isCofiltered_op_iff_isFiltered, IsCofiltered.iff_of_equivalence
    (costructuredArrowOpEquivalence _ _)] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 (F ⋙ G).Elements
have suffices : IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))
Tactic: suffices h : IsCofiltered (StructuredArrow PUnit (F ⋙ G)) from
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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} (F ⋙ G))
have this : IsCofiltered (StructuredArrow PUnit.{u_4 + 1} G)
Tactic: have : IsCofiltered (StructuredArrow PUnit G) :=
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g
have rw : F.map g = F.map g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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
inst_2 : F.Full
inst_3 : F.Faithful
f : X ≅ Y
⊢ F.preimageIso (F.mapIso f) = f
have w : (F.preimageIso (F.mapIso f)).hom = f.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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
hF h₁ h₂ : F.FullyFaithful
⊢ h₁ = h₂
have this : F.Faithful
Tactic: have := h₁.faithful
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } =
    { preimage := @f₂, map_preimage := @hf₂, preimage_map := @preimage_map_1 }
have mk : @f₁ = @f₂
Tactic: simp only [Functor.FullyFaithful.mk.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ @f₁ = @f₂
have mk : ∀ (x x_1 : C) (x_2 : F.obj x ⟶ F.obj x_1), f₁ x_2 = f₂ x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x x_1 : C
x_2 : F.obj x ⟶ F.obj x_1
⊢ f₁ x_2 = f₂ x_2
have mk : F.map (f₁ x_2) = F.map (f₂ x_2)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x x_1 : C
x_2 : F.obj x ⟶ F.obj x_1
⊢ F.map (f₁ x_2) = F.map (f₂ x_2)
have mk : x_2 = F.map (f₂ x_2)
Tactic: rw [hf₁, hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x x_1 : C
x_2 : F.obj x ⟶ F.obj x_1
mk : x_2 = F.map (f₂ x_2)
⊢ F.map (f₁ x_2) = F.map (f₂ x_2)
have mk₁ : x_2 = x_2
Tactic: rw [hf₁, hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF h₂ : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
⊢ { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } = h₂
have mk : ∀ (f₂ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y) (hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f)
  (preimage_map_1 : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f),
  { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } =
    { preimage := @f₂, map_preimage := @hf₂, preimage_map := @preimage_map_1 }
Tactic: cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
hF h₁ h₂ : F.FullyFaithful
this : F.Faithful
⊢ h₁ = h₂
have mk : ∀ (f₁ : {X Y : C} → (f : F.obj X ⟶ F.obj Y) → X ⟶ Y) (hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f)
  (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f),
  { preimage := @f₁, map_preimage := @hf₁, preimage_map := @preimage_map : F.FullyFaithful } = h₂
Tactic: cases h₁ with | mk f₁ hf₁ _ => cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
⊢ Nonempty F.FullyFaithful
have this : F.Faithful
Tactic: have : F.Faithful := ⟨fun h ↦ (hF _ _).injective h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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
hF : ∀ (X Y : C), Function.Bijective (α := X ⟶ Y) F.map
this : F.Faithful
⊢ Nonempty F.FullyFaithful
have this₁ : F.Full
Tactic: have : F.Full := ⟨(hF _ _).surjective⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
α : F ≅ F'
X Y : C
a₁ a₂ : X ⟶ Y
h : F'.map a₁ = F'.map a₂
⊢ F.map a₁ = F.map a₂
have rw : α.symm.inv.app X ≫ F'.map a₁ ≫ α.symm.hom.app Y = F.map a₂
Tactic: rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
α : F ≅ F'
X Y : C
a₁ a₂ : X ⟶ Y
h : F'.map a₁ = F'.map a₂
rw : α.symm.inv.app X ≫ F'.map a₁ ≫ α.symm.hom.app Y = F.map a₂
⊢ F.map a₁ = F.map a₂
have rw₁ : α.symm.inv.app X ≫ F'.map a₂ ≫ α.symm.hom.app Y = F.map a₂
Tactic: rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Faithful
α : F ≅ F'
X Y : C
a₁ a₂ : X ⟶ Y
h : F'.map a₁ = F'.map a₂
rw : α.symm.inv.app X ≫ F'.map a₁ ≫ α.symm.hom.app Y = F.map a₂
rw₁ : α.symm.inv.app X ≫ F'.map a₂ ≫ α.symm.hom.app Y = F.map a₂
⊢ F.map a₁ = F.map a₂
have rw₂ : F.map a₂ = F.map a₂
Tactic: rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
⊢ map (𝟙 X) = 𝟙 (obj X)
have a : G.map (map (𝟙 X)) = G.map (𝟙 (obj X))
Tactic: apply G.map_injective