awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
⊢ IsZero F ↔ ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
have refine : (∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)) → IsZero F
Tactic: refine ⟨fun h _ => Functor.map_isZero _ h, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
⊢ IsIso f
have rw : ∀ (x : (↑X : Type u)),
  IsIso (X :=
    Functor.obj (stalkFunctor C x)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))))
    (CategoryTheory.Functor.map (stalkFunctor C x) f.hom)
Tactic: rw [Presheaf.isIso_iff_stalkFunctor_map_iso]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
⊢ IsZero F
have this : IsIso f
Tactic: have : IsIso f := by
    rw [Presheaf.isIso_iff_stalkFunctor_map_iso]
    exact fun x => isIso_of_source_target_iso_zero _ (h x).isoZero
      ((forget C X ⋙ stalkFunctor C x).map_isZero (isZero_zero _)).isoZero
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact ↔ ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
have mp : S.Exact → ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
mp : S.Exact → ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
⊢ S.Exact ↔ ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
have mpr : (∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))) → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : S.Exact
x : (↑X : Type u)
⊢ ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
have this : Functor.PreservesHomology (C := Sheaf C X) (forget C X ⋙ stalkFunctor C x) ↔
  ∀ (S : ShortComplex (Sheaf C X)), S.Exact → ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
Tactic: have := (forget C X ⋙ stalkFunctor C x).exact_tfae.out 2 1
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
⊢ S.Exact
have h₁ : ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))
Tactic: simp_rw [ShortComplex.exact_iff_isZero_homology] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))
⊢ S.Exact
have mpr : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) S.homology)
Tactic: rw [ShortComplex.exact_iff_isZero_homology, isZero_iff_stalkFunctor_obj_isZero S.homology]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.AddCommGrpCat (goal)
Goal:
X : TopCat
U V : Opens (↑X : Type u)
F : Presheaf AddCommGrpCat X
h : V ≤ U
s t : (↑(F.obj (op U)) : Type u_1)
⊢ restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
      AddCommGrpCat.carrier) (s + t) V h =
    HAdd.hAdd (α :=
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) (F.obj (op V)))
      (restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) s V h)
      (restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) t V h)
have delta : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
      (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
    (s + t) =
  HAdd.hAdd (α :=
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
      AddCommGrpCat.carrier) (F.obj (op V)))
    (β :=
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
      AddCommGrpCat.carrier) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
            AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
          (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
        s :
      (↑(F.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
            AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
          (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
        t :
      (↑(F.obj (op V)) : Type u_1))
Tactic: delta Presheaf.restrictOpen Presheaf.restrict
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
x : X
⊢ IsOpen[inst] {y : X | x ≤ y}
have rw : IsUpperSet.{v} (α := X) {y : X | x ≤ y}
Tactic: rw [IsUpperSet.isOpen_iff_isUpperSet]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
⊢ principalOpen x ≤ U ↔ x ∈ U
have refine : ∀ (hx : x ∈ U) (y : X) (hy : Membership.mem (γ := Opens X) (principalOpen x) y), y ∈ U
Tactic: refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (hypothesis)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
⊢ y ∈ U
have this : IsOpen[inst] (↑U : Set X)
Tactic: have := U.isOpen
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (hypothesis)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
this : IsOpen[inst] (↑U : Set X)
⊢ y ∈ U
have this₁ : IsUpperSet (↑U : Set X)
Tactic: rw [IsUpperSet.isOpen_iff_isUpperSet] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
⊢ m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)
have symm : limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S) = m
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
⊢ limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S) = m
have w : ∀ (left : Discrete PUnit.{1}) (x : (↑X : Type v))
  (f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x),
  CategoryStruct.comp (Y :=
      limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v))) (generator (iSup Us) ⋙ F))
      (limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S))
      (limit.π (generator (iSup Us) ⋙ F)
        { left := left, right := x, hom := f : Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }) =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left, right := x, hom := f }
Tactic: ext ⟨_, x, f⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x
⊢ ∃ (i : α), principalOpen x ≤ Us i
have w : principalOpen x ≤ iSup Us
Tactic: apply exists_le_of_le_sup
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
X : TopCat
inst_2 : Preorder (↑X : Type v)
inst_3 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)
have rw : IsSheafOpensLeCover (principalsKanExtension F)
Tactic: rw [isSheaf_iff_isSheafOpensLeCover]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
X : TopCat
inst_2 : Preorder (↑X : Type v)
inst_3 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
ι : Type v
Us : ι → Opens (↑X : Type v)
⊢ Nonempty
    (IsLimit (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : ι), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op))
have val : IsLimit (F :=
  Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : ι), V ≤ Us i) ⋙ principalsKanExtension F)
  (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P
have have : ∀ (this : P ≅ principalsKanExtension F), CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P
Tactic: have : P ≅ principalsKanExtension F :=
    @rightKanExtensionUnique _ _ _ _ _ _ _ _ _ _ (by assumption) _ _ (by assumption)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P
have change : TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) P
Tactic: change TopCat.Presheaf.IsSheaf (X := TopCat.of X) P
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
⊢ TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) P
have rw : TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) (principalsKanExtension F)
Tactic: rw [isSheaf_iso_iff this]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (hypothesis)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
x : Preorder (↑(of X) : Type v) := inst_1
⊢ TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) (principalsKanExtension F)
have x : Topology.IsUpperSet.{v} (↑(of X) : Type v)
Tactic: have _ : Topology.IsUpperSet (TopCat.of X) := inferInstanceAs <| Topology.IsUpperSet X
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))
have simp_rw : CommRingCat.ofHom (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) sorry) =
  𝟙 (CommRingCat.of (Localization (G.obj U)))
Tactic: simp_rw [F.map_id]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))
have hf : ∀ (x : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)),
  Eq (α := (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) sorry)) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom (𝟙 (CommRingCat.of (Localization (G.obj U)))) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ Eq (α := CommRingCat.of (Localization (G.obj U)) ⟶ CommRingCat.of (Localization (G.obj W)))
    (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
      CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯))
    (CategoryStruct.comp (Y := CommRingCat.of (Localization (G.obj V)))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)))
have simp_rw : Eq (α := CommRingCat.of (Localization (G.obj U)) ⟶ CommRingCat.of (Localization (G.obj W)))
  (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
    CommRingCat.carrier)
    (IsLocalization.map (T := G.obj W) (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) sorry))
  (CategoryStruct.comp (Y := CommRingCat.of (Localization (G.obj V)))
    (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
      CommRingCat.carrier) (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) sorry))
    (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
      CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) sorry)))
Tactic: simp_rw [F.map_comp]