awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
⊢ Eq (α := Z ⟶ s.pt)
    (g₁ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (g₂ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
have hF : Eq (α :=
  S.arrows.diagram.obj
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
    Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
  (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F) ≫
    s.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
  (s.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
    Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F))
Tactic: have hF := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ (ObjectProperty.homMk F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F) ≫
      s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F))
⊢ Eq (α := Z ⟶ s.pt)
    (g₁ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (g₂ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
have hF₁ : Eq (α :=
  S.arrows.diagram.obj
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
    Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
  (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁) ≫
    s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
  (s.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
    Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁))
Tactic: have hF₁ := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ (ObjectProperty.homMk F₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) ↔ Nonempty (IsColimit S.arrows.cocone)
have mp : (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
mp : (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)
⊢ (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) ↔ Nonempty (IsColimit S.arrows.cocone)
have mpr : Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)
have mp : IsColimit S.arrows.cocone
Tactic: refine Nonempty.intro ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
⊢ S.arrows.cocone.ι.app f ≫
      Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
        (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
              (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
            x ∧
          ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) y → y = x)
        ⋯ =
    s.ι.app f
have H₁ : ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
  (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
Tactic: replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
⊢ S.arrows.cocone.ι.app f ≫
      Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
        (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
              (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
            x ∧
          ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) y → y = x)
        ⋯ =
    s.ι.app f
have ht : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj yoneda s.pt) f.obj (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom).hom.op) :
      (a : (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op X))) →
        (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op f.obj.left)))
    (Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
      (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
          x ∧
        ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
          (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
                (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
              y →
            y = x)
      H) =
  S.arrows.yonedaFamilyOfElements_fromCocone s f.obj (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom).hom sorry
Tactic: have ht := H.choose_spec.1 f.obj.hom f.property
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
⊢ Fs =
    Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
      (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
          x ∧
        ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
          (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) y → y = x)
      ⋯
have H₁ : ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
  (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
Tactic: replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
⊢ Fs =
    Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
      (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
          x ∧
        ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
          (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) y → y = x)
      ⋯
have apply : (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) Fs
Tactic: apply H.choose_spec.2 Fs
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t
have mpr : ∀ (H : IsColimit S.arrows.cocone), ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: replace H := Classical.choice H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t
have h : (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s) ∧
  ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
Tactic: use H.desc s
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s) ∧
    ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
      (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
have h : (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
h : (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s)
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s) ∧
    ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
      (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
have h₁ : ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
  (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
adj : F ⊣ sheafToPresheaf J A
inst_2 : PreservesFiniteLimits F
⊢ ∀ (J_1 : Type) [inst_3 : SmallCategory J_1] [FinCategory J_1],
    PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) J_1 (Functor.leftAdjoint (sheafToPresheaf J A))
have this : Functor.IsRightAdjoint (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (sheafToPresheaf J A)
Tactic: have : (sheafToPresheaf J A).IsRightAdjoint := ⟨_, ⟨adj⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (Y := sheafify J P) (toSheafify J P)
have refine_1 : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
    (InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
  𝟙 P
Tactic: refine ⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).hom, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_1 :
  CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    𝟙 P
⊢ IsIso (Y := sheafify J P) (toSheafify J P)
have refine_2 : InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
    toSheafify J P =
  𝟙 (sheafify J P)
Tactic: refine ⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).hom, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    𝟙 P
have refine_1 : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
    (InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
  NatTrans.app (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)))
    (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)
Tactic: change _ = (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D)) :).app ⟨P, hP⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    NatTrans.app (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)))
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)
have refine_1 : CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
    (InducedCategory.Hom.hom
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
  NatTrans.app
    (CategoryStruct.comp (Y := sheafToPresheaf J D ⋙ presheafToSheaf J D ⋙ sheafToPresheaf J D)
      (Functor.whiskerLeft (sheafToPresheaf J D) (Adjunction.unit (sheafificationAdjunction J D)))
      (Functor.whiskerRight (Adjunction.counit (sheafificationAdjunction J D)) (sheafToPresheaf J D)))
    (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)
Tactic: rw [← sheafificationAdjunction J D |>.right_triangle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P =
    𝟙 (sheafify J P)
have refine_2 : Eq (α :=
  Functor.obj (sheafToPresheaf J D)
      (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
    sheafify J P)
  (Functor.map (sheafToPresheaf J D)
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
    toSheafify J P)
  (𝟙 (sheafify J P))
Tactic: change (sheafToPresheaf _ _).map _ ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      sheafify J P)
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P)
    (𝟙 (sheafify J P))
have refine_2 : Eq (α :=
  Functor.obj (sheafToPresheaf J D)
      (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
    Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
      (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
  (Functor.map (sheafToPresheaf J D)
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
    NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
      (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
  (𝟙 (sheafify J P))
Tactic: change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨P, hP⟩) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (𝟙 (sheafify J P))
have refine_2 : Eq (α :=
  Functor.obj (sheafToPresheaf J D)
      (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
    Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
      (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
  (Functor.map (sheafToPresheaf J D)
      (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
    inv
      (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))))
  (𝟙 (sheafify J P))
Tactic: rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheafification (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ CategoryStruct.comp (Y := sheafify J P) (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
      (InducedCategory.Hom.hom
        (Functor.map (presheafToSheaf J D) η ≫
          NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
have change : CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
    (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
    (Functor.map (sheafToPresheaf J D) (Functor.map (presheafToSheaf J D) η) ≫
      InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
  η
Tactic: change _ ≫ (sheafToPresheaf J D).map _ ≫ _ = _