awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
rw :
  Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
        ((uliftYoneda.{v', v, u} J).map g.unop ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
⊢ Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g) :
          (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) f) :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
have rw₁ : Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
        (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj (op (unop Y)))) →
          (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op (unop Y))))
      ((J.uliftYonedaEquiv :
          (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ (uliftYoneda.{v', v, u} J).obj (unop X)) →
            ((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj (op (unop Y)))
        ((uliftYoneda.{v', v, u} J).map g.unop)) :
    (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
        (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
          (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
      { down := g.unop } :
    (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
Tactic: rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
t : F.obj (P := Presheaf.IsSheaf J).obj X
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          t) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          t :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
have obtain : ∀ (u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F),
  Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
Tactic: obtain ⟨u, rfl⟩ := J.uliftYonedaEquiv.surjective t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
have rw : Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
  ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
      ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
        ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) :
    (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
  ((uliftYoneda.{v', v, u} J).map f.unop ≫
      (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
    (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
Tactic: rw [uliftYonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
rw :
  Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
          ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
have rw₁ : (uliftYoneda.{v', v, u} J).map f.unop ≫ u =
  (uliftYoneda.{v', v, u} J).map f.unop ≫
    (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
      ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)
Tactic: rw [uliftYonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
rw :
  Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
          ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
rw₁ :
  (uliftYoneda.{v', v, u} J).map f.unop ≫ u =
    (uliftYoneda.{v', v, u} J).map f.unop ≫
      (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
have rw₂ : (uliftYoneda.{v', v, u} J).map f.unop ≫ u = (uliftYoneda.{v', v, u} J).map f.unop ≫ u
Tactic: rw [uliftYonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g
have h₁ : ∀ (X : Cᵒᵖ) (x : P.obj (P := Presheaf.IsSheaf J).obj X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.hom.app X)).toFun x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda
have refine : ∀ {I : Type u_2} (x : Category.{u_1, u_2} I), PreservesLimitsOfShape I J.yoneda
Tactic: refine ⟨fun {I} _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
I : Type u_2
x : Category.{u_1, u_2} I
⊢ PreservesLimitsOfShape I J.yoneda
have this : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))
Tactic: have : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J _) :=
    inferInstanceAs <| PreservesLimitsOfShape I CategoryTheory.yoneda
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
⊢ Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have pos : ∀ (h : i = j),
  Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
pos :
  ∀ (h : i = j),
    Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          a :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          b :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have neg : ∀ (h : ¬i = j),
  Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : i = j
⊢ Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have pos : ∀ (b : Y ⟶ X i) (hab : a ≫ c.inj i = b ≫ c.inj i),
  Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: subst h
Cleared hypotheses: j, b, hab, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i : ι
a b : Y ⟶ X i
hab : a ≫ c.inj i = b ≫ c.inj i
⊢ Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have pos : Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
          (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
      b :
    (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
          (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
      b :
    (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: rw [(cancel_mono _).mp hab]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have neg : ∀ (h : IsInitial.{v, u} Y),
  Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        a :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
            (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
        b :
      (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: obtain ⟨h⟩ := hdisj h a b hab