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
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ ObjectProperty.IsSeparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.pair G H)
have h : Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
  (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
have h : ∀ (X : C),
  ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
X : C
⊢ ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
have h : G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
Tactic: simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
X : C
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
have h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
have h₁ : (∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X) → G = X ∨ H = X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
have h : ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left →
  H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
have h : ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right →
  H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
⊢ IsCoseparator.{v₁, u₁} c.pt
have rw : ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g
Tactic: rw [isCoseparator_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g
have refine : ∀ (x x_1 : C) (x_2 x_3 : x ⟶ x_1) (huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h) (x_4 : C)
  (h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4) (g : x_1 ⟶ x_4), x_2 ≫ g = x_3 ≫ g
Tactic: refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h
x_4 : C
h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4
g : x_1 ⟶ x_4
⊢ x_2 ≫ g = x_3 ≫ g
have obtain : ∀ (b : β) (g : x_1 ⟶ f b), x_2 ≫ g = x_3 ≫ g
Tactic: obtain ⟨b⟩ := h
Cleared hypotheses: x_4, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
⊢ IsCoseparator.{v₁, u₁} c.pt ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
have refine : ∀ (h : IsCoseparator.{v₁, u₁} c.pt) (X Y : C) (u v : X ⟶ Y)
  (huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h), u = v
Tactic: refine ⟨fun h X Y u v huv => ?_, fun h => isCoseparator_of_isLimit_fan h hc⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
h : IsCoseparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v
have refine : ∀ (g : Y ⟶ c.pt) (b : Discrete β), (u ≫ g) ≫ c.π.app b = (v ≫ g) ≫ c.π.app b
Tactic: refine h.def _ _ fun g => hc.hom_ext fun b => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ IsCoseparator.{v₁, u₁} (Limits.prod.{v₁, u₁} G H) ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)
have refine : ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
  ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)
Tactic: refine (isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)
have h : Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
  (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
have h : ∀ (X : C),
  ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
X : C
⊢ ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
have h : G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
Tactic: simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
X : C
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
have h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
have h₁ : (∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X) → G = X ∨ H = X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
have h : ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left →
  H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
have h : ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right →
  H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsDetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
have refine_1 : ∀ (hG : IsDetector.{v₁, u₁} G) {A B : C} (f : A ⟶ B)
  (hf : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) A) (Functor.map (Functor.obj coyoneda (op G)) f))
  (h : G ⟶ B), ∃! h' : G ⟶ A, h' ≫ f = h
Tactic: refine
    ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
      (isDetector_def _).2 fun X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
refine_1 :
  ∀ (hG : IsDetector.{v₁, u₁} G) {A B : C} (f : A ⟶ B)
    (hf : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) A) (Functor.map (Functor.obj coyoneda (op G)) f))
    (h : G ⟶ B), ∃! h' : G ⟶ A, h' ≫ f = h
⊢ IsDetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
have refine_2 : ∀ (h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))) (X Y : C) (f : X ⟶ Y)
  (hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h), IsIso f
Tactic: refine
    ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
      (isDetector_def _).2 fun X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
A B : C
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) A) (Functor.map (Functor.obj coyoneda (op G)) f)
h : G ⟶ B
⊢ ∃! h' : G ⟶ A, h' ≫ f = h
have refine_1 : ∀
  (hf :
    ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) B)),
      ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) A),
        (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f) :
              (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj A)) →
                (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj B))
            a =
          b)
  (h : G ⟶ B), ∃! h' : G ⟶ A, h' ≫ f = h
Tactic: rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f
have refine_2 : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
Tactic: suffices IsIso ((coyoneda.obj (op G)).map f) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
have refine_2 : Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
  (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
  (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
    (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) → (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_2 :
  Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
      (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
        (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
⊢ IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
have refine_2₁ : ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y)),
  ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X),
    (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
        a =
      b
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCodetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
have refine_1 : ∀ (hG : IsCodetector.{v₁, u₁} G) {A B : Cᵒᵖ} (f : A ⟶ B)
  (hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)), IsIso f
Tactic: refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
refine_1 :
  ∀ (hG : IsCodetector.{v₁, u₁} G) {A B : Cᵒᵖ} (f : A ⟶ B)
    (hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)), IsIso f
⊢ IsCodetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
have refine_2 : ∀ (h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)) (X Y : C) (f : X ⟶ Y)
  (hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h), IsIso f
Tactic: refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
⊢ IsIso f
have refine_1 : ∀ (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
Tactic: refine (isIso_unop_iff _).1 (hG.def _ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
⊢ ∀ (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
have refine_1 : ∀
  (hf :
    Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) A)) (β :=
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) B))
      (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f)) :
        (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj A)) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj B)))
  (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
refine_1 :
  ∀
    (hf :
      Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) A)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) B))
        (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj A)) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj B)))
    (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
⊢ ∀ (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
have refine_1₁ : ∀
  (hf :
    ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) B)),
      ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) A),
        (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f) :
              (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj A)) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj B))
            a =
          b)
  (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso f
have refine_2 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op
Tactic: rw [← isIso_op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op
have refine_2 : IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
Tactic: suffices IsIso ((yoneda.obj G).map f.op) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
have refine_2 : Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
  (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
  (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
    (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_2 :
  Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
⊢ IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
have refine_2₁ : ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X))),
  ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y)),
    (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
        a =
      b
Tactic: rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.HomologicalComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
⊢ f = g
have h₁ : ∀ (j : ι), f.f j = g.f j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.HomologicalComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
⊢ f.f j = g.f j
have h₁ : ∀ (G : C), ObjectProperty.ofObj.{v, u, t} X G → ∀ (h : G ⟶ K.X j), h ≫ f.f j = h ≫ g.f j
Tactic: apply hX