awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hφ :
  ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Eq (α := CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x : CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y : CD (F₂.obj X))
Y : C
f : Y ⟶ unop X
⊢ (equalizerSieve (FD := FD) (CD := CD) x y).arrows f ↔ Sieve.arrows ⊤ f
have h₁ : Eq (α := CD (F₁.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
    CD (F₁.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
    CD (F₁.obj (op Y)))
Tactic: simp only [equalizerSieve_apply, op_unop, Sieve.top_apply, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hφ :
  ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Eq (α := CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x : CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y : CD (F₂.obj X))
Y : C
f : Y ⟶ unop X
⊢ Eq (α := CD (F₁.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
      CD (F₁.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
      CD (F₁.obj (op Y)))
have h₁ : Eq (α := CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
        CD (F₁.obj (op Y))) :
    CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
        CD (F₁.obj (op Y))) :
    CD (F₂.obj (op Y)))
Tactic: apply hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsIso φ
X : Cᵒᵖ
⊢ Function.Bijective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
    (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
have rw : IsIso.{w, w + 1} (X := CD (F₁.obj X)) (Y := CD (F₂.obj X))
  (↾(⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X)))
Tactic: rw [bijective_iff_isIso_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) ↔
    IsLocallyInjective (FD := FD) (CD := CD) J φ
have mp : IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) →
  IsLocallyInjective (FD := FD) (CD := CD) J φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
mp :
  IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) →
    IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) ↔
    IsLocallyInjective (FD := FD) (CD := CD) J φ
have mpr : IsLocallyInjective (FD := FD) (CD := CD) J φ →
  IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)
have mp : IsLocallyInjective (FD := FD) (CD := CD) J φ →
  ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
    Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
        (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
        (equalizerSieve (FD := FD) (CD := CD) x y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
mp :
  IsLocallyInjective (FD := FD) (CD := CD) J φ →
    ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)
have mpr : (∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
    Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
        (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
        (equalizerSieve (FD := FD) (CD := CD) x y)) →
  IsLocallyInjective (FD := FD) (CD := CD) J φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)
have mp : Sieve.bind S.arrows T ≤ equalizerSieve (FD := FD) (CD := CD) x y
Tactic: refine J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
mp : Sieve.bind S.arrows T ≤ equalizerSieve (FD := FD) (CD := CD) x y
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)
have mp₁ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
  Sieve.arrows
      (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
      f →
    Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: refine J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
Y : C
f : Y ⟶ unop X
hf :
  Sieve.arrows
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
    f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
have mp : Eq (α := CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
          x :
        CD (F₁.obj (op Y))) :
    CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
          y :
        CD (F₁.obj (op Y))) :
    CD (F₂.obj (op Y)))
Tactic: refine J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf)
        (equalizerSieve_mem J φ _ _ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J φ
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Eq (α := CD (F₃.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((φ ≫ ψ).app X) : (a : CD (F₁.obj X)) → CD (F₃.obj X)) x :
      CD (F₃.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((φ ≫ ψ).app X) : (a : CD (F₁.obj X)) → CD (F₃.obj X)) y :
      CD (F₃.obj X))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)
have h₁ : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
  (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
Tactic: apply equalizerSieve_mem_of_equalizerSieve_app_mem J φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J φψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ
have inst : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
Tactic: subst fac
Cleared hypotheses: φψ, fac, inst_4
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φψ ↔ IsLocallyInjective (FD := FD) (CD := CD) J φ
have mp : IsLocallyInjective (FD := FD) (CD := CD) J φψ → IsLocallyInjective (FD := FD) (CD := CD) J φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
mp : IsLocallyInjective (FD := FD) (CD := CD) J φψ → IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φψ ↔ IsLocallyInjective (FD := FD) (CD := CD) J φ
have mpr : IsLocallyInjective (FD := FD) (CD := CD) J φ → IsLocallyInjective (FD := FD) (CD := CD) J φψ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
h : IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φψ
have mpr : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
Tactic: rw [← fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ (X : Cᵒᵖ),
      Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
have mp : IsLocallyInjective (FD := FD) (CD := CD) J φ →
  ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
mp :
  IsLocallyInjective (FD := FD) (CD := CD) J φ →
    ∀ (X : Cᵒᵖ),
      Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ (X : Cᵒᵖ),
      Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))
have mpr : (∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))) →
  IsLocallyInjective (FD := FD) (CD := CD) J φ
Tactic: constructor