awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
⊢ Eq (α := (pullback f f).obj (P := Presheaf.IsSheaf J) ⟶ I) (InducedCategory.Hom.hom (pullback.fst f f) ≫ p)
    (InducedCategory.Hom.hom (pullback.snd f f) ≫ p)
have e_a : Eq (α := (pullback f f).obj (P := Presheaf.IsSheaf J) ⟶ G.obj (P := Presheaf.IsSheaf J))
  ((InducedCategory.Hom.hom (pullback.fst f f) ≫ p) ≫ i) ((InducedCategory.Hom.hom (pullback.snd f f) ≫ p) ≫ i)
Tactic: rw [← cancel_mono i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
⊢ IsColimit (F :=
    parallelPair (X := Functor.obj (presheafToSheaf J D) ((pullback f f).obj (P := Presheaf.IsSheaf J)))
      (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.fst f f)))
      (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.snd f f))))
    (Cofork.ofπ (Functor.map (presheafToSheaf J D) p) ⋯)
have this₁ : IsRegularEpi p
Tactic: have := IsRegularEpiCategory.regularEpiOfEpi p
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
⊢ Functor.map (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E)) g ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      (S.arrows.diagram.op ⋙ P).map g
have this : (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
    (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) sorry =
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda E).map (Over.Hom.left g.unop.hom).op) :
      (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f).obj.left))) →
        (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f').obj.left)))
    ((↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom sorry)
Tactic: have := x.2 f.unop.1.hom g.unop.hom.left f.unop.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda E).map (Over.Hom.left g.unop.hom).op) :
        (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f).obj.left))) →
          (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f').obj.left)))
      ((↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯)
⊢ Functor.map (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E)) g ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      (S.arrows.diagram.op ⋙ P).map g
have dsimp : 𝟙 (unop E) ≫
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom sorry =
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom sorry ≫
    P.map (Over.Hom.left g.unop.hom).op
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
⊢ 𝟙 (unop E) ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
have rw : (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
    (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom sorry =
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
    (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) sorry
Tactic: rw [id_comp, ← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
⊢ (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯
have h : Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom =
  (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ Functor.obj coyoneda E) S.arrows
have dsimp : Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.Compatible (R := S.arrows) → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: dsimp [IsSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.Compatible (R := S.arrows) → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have simp_rw : Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: simp_rw [compatible_iff_sieveCompatible]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have rw : Nonempty ((X_1 : Cone (S.arrows.diagram.op ⋙ P)) → Unique (X_1 ⟶ P.mapCone S.arrows.cocone.op)) ↔
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: rw [((Cone.isLimitEquivIsTerminal _).trans (isTerminalEquivUnique _ _)).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ Nonempty ((X_1 : Cone (S.arrows.diagram.op ⋙ P)) → Unique (X_1 ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have rw : (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: rw [Classical.nonempty_pi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have mp : (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) →
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
mp :
  (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have mpr : (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t) →
  ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hu : ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
⊢ ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have hu₁ : Nonempty.{v₂ + 1} (Unique (hx.cone ⟶ P.mapCone S.arrows.cocone.op))
Tactic: specialize hu hx.cone
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
hu : Nonempty.{v₂ + 1} (Unique (hx.cone ⟶ P.mapCone S.arrows.cocone.op))
⊢ ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
have hu₁ : Nonempty.{v₂ + 1} (Unique { t : (P ⋙ Functor.obj coyoneda E).obj (op X) // x.IsAmalgamation (R := S.arrows) t })
Tactic: rw [(homEquivAmalgamation hx).uniqueCongr.nonempty_congr] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Nonempty.{v₂ + 1} (Unique ({ pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))
have mpr : Nonempty.{v₂ + 1}
  (Unique ({ pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))
Tactic: rw [← eqv.left_inv π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Nonempty.{v₂ + 1}
    (Unique
      ({ pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))
have mpr : Nonempty.{v₂ + 1}
  (Unique
    { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
      IsAmalgamation (R := S.arrows)
        (↑((eqv :
                (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                  { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
              π) :
          FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
        t })
Tactic: erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Nonempty.{v₂ + 1}
    (Unique
      { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
        IsAmalgamation (R := S.arrows)
          (↑((eqv :
                  (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                    { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                π) :
            FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
          t })
have mpr : ∃! a : (P ⋙ Functor.obj coyoneda (op E)).obj (op X),
  IsAmalgamation (R := S.arrows)
    (↑((eqv :
            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
          π) :
      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
    a
Tactic: rw [unique_subtype_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
have mp : (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) →
  ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
mp :
  (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) →
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
have mpr : (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows) →
  ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
⊢ t₁ = t₂
have hx : x.Compatible (R := S.arrows)
Tactic: have hx := is_compatible_of_exists_amalgamation x ⟨t₁, h₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.Compatible (R := S.arrows)
⊢ t₁ = t₂
have hx₁ : x.SieveCompatible
Tactic: rw [compatible_iff_sieveCompatible] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.SieveCompatible
⊢ t₁ = t₂
have hs₁ : Subsingleton.{v₂ + 1} (hx.cone ⟶ P.mapCone S.arrows.cocone.op)
Tactic: specialize hs hx.cone
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.SieveCompatible
hs : Subsingleton.{v₂ + 1} (hx.cone ⟶ P.mapCone S.arrows.cocone.op)
⊢ t₁ = t₂
have hs₁ : ∀ (a b : hx.cone ⟶ P.mapCone S.arrows.cocone.op), a = b
Tactic: rcases hs with ⟨hs⟩
Cleared hypotheses: hs