awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
rw₁ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
rw₃ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
have rw₄ : IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (toSheafify J P ≫ InducedCategory.Hom.hom (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
Tactic: rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
have rw : IsLocallySurjective J (FA := FA) (CA := CA) (F :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
    (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallySurjective J (FA := FA) (CA := CA) φ
Tactic: rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
have rw₁ : IsLocallySurjective J (FA := FA) (CA := CA) (F :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
    (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
Tactic: rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
rw₁ :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
have rw₂ : IsLocallySurjective J (FA := FA) (CA := CA) (G :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
  IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
Tactic: rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
rw₁ :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
have rw₃ : IsLocallySurjective J (FA := FA) (CA := CA) (G :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
  IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
Tactic: rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
rw₁ :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
rw₃ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
have rw₄ : IsLocallySurjective J (FA := FA) (CA := CA) (G :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (toSheafify J P ≫ InducedCategory.Hom.hom (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
Tactic: rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
U V : C
f : U ⟶ V
⊢ G.imageSieve (G.map f) = ⊤
have h : ∀ ⦃W : C⦄ (g : W ⟶ U), (G.imageSieve (G.map f)).arrows g ↔ Sieve.arrows ⊤ g
Tactic: ext W g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
U V : C
f : U ⟶ V
⊢ equalizer f f = ⊤
have h : ∀ ⦃Y : C⦄ (f_1 : Y ⟶ U), (equalizer f f).arrows f_1 ↔ arrows ⊤ f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
⊢ s = t
have apply : ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
  (Sieve.functorPushforward G (G.imageSieve i)).arrows f →
    Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
          s :
        (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
          t :
        (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property) _
    (G.functorPushforward_imageSieve_mem K i)).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X),
    j ≫ i₁ = j ≫ i₂ →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
⊢ s = t
have apply : ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
  (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f →
    Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
          s :
        (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
          t :
        (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property) _
    (G.functorPushforward_equalizer_mem K i₁ i₂ e)).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Full
U V : C
f : G.obj U ⟶ G.obj V
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (G.imageSieve f))
have rw : Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
  (Sieve.functorPushforward G (G.imageSieve (G.map (G.preimage f))))
Tactic: rw [← G.map_preimage f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyFullyFaithful (goal)
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Faithful
U V : C
f₁ f₂ : U ⟶ V
e : G.map f₁ = G.map f₂
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (Sieve.equalizer f₁ f₂))
have obtain : ∀ (e : G.map f₁ = G.map f₁),
  Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (Sieve.equalizer f₁ f₁))
Tactic: obtain rfl := G.map_injective e
Cleared hypotheses: f₂, e
-- 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 : Functor.{v, v', u, u'} Cᵒᵖ D
X_1 : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X_1)
X Y : C
f : X ⟶ unop X_1
hf :
  Eq (α := CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op X)))
        x :
      CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op X)))
        y :
      CD (F.obj (op X)))
g : Y ⟶ X
⊢ Eq (α := CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (g ≫ f).op) :
          (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op Y)))
        x :
      CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (g ≫ f).op) :
          (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op Y)))
        y :
      CD (F.obj (op Y)))
have dsimp : Eq (α := CD (F.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) x :
    CD (F.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) y :
    CD (F.obj (op Y)))
Tactic: dsimp at hf ⊢
-- 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
⊢ equalizerSieve (FD := FD) (CD := CD) x y = ⊤ ↔ x = y
have mp : equalizerSieve (FD := FD) (CD := CD) x y = ⊤ → 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
mp : equalizerSieve (FD := FD) (CD := CD) x y = ⊤ → x = y
⊢ equalizerSieve (FD := FD) (CD := CD) x y = ⊤ ↔ x = y
have mpr : x = y → 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₂
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))
⊢ 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₁ : equalizerSieve (FD := FD) (CD := CD) x y = ⊤
Tactic: convert! J.top_mem X.unop
-- 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))
⊢ equalizerSieve (FD := FD) (CD := CD) x y = ⊤
have h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ unop X), (equalizerSieve (FD := FD) (CD := CD) x y).arrows f ↔ Sieve.arrows ⊤ f
Tactic: ext Y f