awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (x : IsLimit c) (j : X ⟶ c.pt), Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan.{w, v₁, u₁} s
hc : IsLimit c
j : Y ⟶ c.pt
h_1 : Mono j
⊢ f = g
have rw : f ≫ j = g ≫ j
Tactic: rw [← cancel_mono j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
have obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : ColimitOfShape.{w', w, v₁, u₁} P J X), f = g
Tactic: obtain ⟨J, _, ⟨p⟩⟩ := hP X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), limitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
have obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : LimitOfShape.{w', w, v₁, u₁} P J Y), f = g
Tactic: obtain ⟨J, _, ⟨p⟩⟩ := hP Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
⊢ HasInitial.{v₁, u₁} C
have this : HasFiniteLimits.{v₁, u₁} C
Tactic: have := hasFiniteLimits_of_hasLimitsOfSize C
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this : HasFiniteLimits.{v₁, u₁} C
⊢ HasInitial.{v₁, u₁} C
have this₁ : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
Tactic: haveI := hasProductsOfShape_of_small C (Subtype P)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
⊢ HasInitial.{v₁, u₁} C
have this₁ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
Tactic: haveI := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
⊢ HasInitial.{v₁, u₁} C
have suffices : (A : C) →
  Unique
    (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      A)
Tactic: suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
⊢ (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
have this₁ : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
Tactic: have := hP.mono_productTo
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
⊢ (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
have refine_1 : (A : C) →
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
Tactic: refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
refine_1 :
  (A : C) →
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      A
⊢ (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
have refine_2 : ∀ (A : C)
  (f :
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      A),
  f = default
Tactic: refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
⊢ f = default
have refine_2 : ∀
  (g :
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      A),
  f = g
Tactic: suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
      apply this
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
⊢ f = g
have refine_2 : IsSplitEpi (X := equalizer f g) (equalizer.ι f g)
Tactic: suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
⊢ CategoryStruct.comp (Y := equalizer f g) (Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥) ⋯)
      (equalizer.ι f g) =
    𝟙
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥)
have h : ∀ (b : Subtype P),
  Eq (α :=
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      (↑b : C))
    ((CategoryStruct.comp (Y := equalizer f g) (Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥) sorry)
          (equalizer.ι f g) ≫
        Subobject.arrow ⊥) ≫
      Pi.π (Subtype.val (p := P)) b)
    ((𝟙
          (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
            Subobject.underlying ⊥) ≫
        Subobject.arrow ⊥) ≫
      Pi.π (Subtype.val (p := P)) b)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst_2 : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst_3 : HasColimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsSeparating
⊢ HasTerminal.{v₁, u₁} C
have this : HasInitial.{v₁, u₁} Cᵒᵖ
Tactic: haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating (P.isCoseparating_op_iff.2 hP)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ P = Q
have suffices : IsIso (P.ofLE Q h₁)
Tactic: suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ IsIso (P.ofLE Q h₁)
have refine : ∀ (G : C) (hG : 𝒢 G) (f : G ⟶ Functor.obj underlying Q), ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f
Tactic: refine h𝒢 _ fun G hG f => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
⊢ ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f
have this : P.Factors (f ≫ Q.arrow)
Tactic: have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f
have refine_1 : (fun (h' : G ⟶ Functor.obj underlying P) ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)
Tactic: refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
refine_1 : (fun (h' : G ⟶ Functor.obj underlying P) ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)
⊢ ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f
have refine_2 : ∀ (g : G ⟶ Functor.obj underlying P) (hg : g ≫ P.ofLE Q h₁ = f), g = P.factorThru (f ≫ Q.arrow) this
Tactic: refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
⊢ (P.inverseImage (proj S T)).IsCoseparating
have refine : ∀ (X Y : StructuredArrow S T) (f g : X ⟶ Y)
  (hfg : ∀ (G : StructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) (G : C) (hG : P G)
  (h : Y.right ⟶ G), Hom.right f ≫ h = Hom.right g ≫ h
Tactic: refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
⊢ (P.inverseImage (proj S T)).IsSeparating
have refine : ∀ (X Y : CostructuredArrow S T) (f g : X ⟶ Y)
  (hfg : ∀ (G : CostructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) (G : C) (hG : P G)
  (h : G ⟶ X.left), h ≫ f.left = h ≫ g.left
Tactic: refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsSeparator.{v₁, u₁} (op G) ↔ IsCoseparator.{v₁, u₁} G
have rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparator.{v₁, u₁} G
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparator.{v₁, u₁} G
⊢ IsSeparator.{v₁, u₁} (op G) ↔ IsCoseparator.{v₁, u₁} G
have rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparator.{v₁, u₁} G
rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsSeparator.{v₁, u₁} (op G) ↔ IsCoseparator.{v₁, u₁} G
have rw₂ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
  IsSeparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparator.{v₁, u₁} G
rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsSeparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
⊢ IsSeparator.{v₁, u₁} (op G) ↔ IsCoseparator.{v₁, u₁} G
have rw₃ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G))
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparator.{v₁, u₁} G
have rw : IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparator.{v₁, u₁} G
have rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparator.{v₁, u₁} G
have rw₂ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
  IsCoseparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsCoseparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
⊢ IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparator.{v₁, u₁} G
have rw₃ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G))
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparator.{v₁, u₁} G
have rw : IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparator.{v₁, u₁} G
have rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparator.{v₁, u₁} G
have rw₂ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
  IsCoseparating.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCoseparating.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
⊢ IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparator.{v₁, u₁} G
have rw₃ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G))
Tactic: rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsSeparator.{v₁, u₁} (unop G) ↔ IsCoseparator.{v₁, u₁} G
have rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCoseparator.{v₁, u₁} G
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCoseparator.{v₁, u₁} G
⊢ IsSeparator.{v₁, u₁} (unop G) ↔ IsCoseparator.{v₁, u₁} G
have rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]