awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
X : A'ᵒᵖ
q :
  Nonempty
    (IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda X) R)
        (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda X) R)
        (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda X) R))
      (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda X) R) ⋯))
mp :
  (q :
      IsLimit (F :=
        parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda X) R)
          (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda X) R)
          (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda X) R))
        (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda X) R) ⋯)) →
    IsLimit (F :=
      parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P') ⋙ Functor.obj coyoneda X)
      (Functor.mapCone (Functor.obj coyoneda X) (Fork.ofι (forkMap R P') ⋯))
⊢ IsLimit (F :=
    parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P') ⋙ Functor.obj coyoneda X)
    (Functor.mapCone (Functor.obj coyoneda X) (Fork.ofι (forkMap R P') ⋯))

Tactic:
replace q := Classical.choice q
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
X : A'ᵒᵖ
q :
  IsLimit (F :=
    parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda X) R)
      (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda X) R)
      (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda X) R))
    (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda X) R) ⋯)
⊢ IsLimit (F :=
    parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P') ⋙ Functor.obj coyoneda X)
    (Functor.mapCone (Functor.obj coyoneda X) (Fork.ofι (forkMap R P') ⋯))

Tactic:
apply (isSheafForIsSheafFor' _ _ _ _).symm q

Premises used: CategoryTheory.Presheaf.isSheafForIsSheafFor', Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
mpr :
  Nonempty
    (IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows))
      (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows) ⋯))
⊢ Presieve.IsSheafFor (P' ⋙ Functor.obj coyoneda (op U)) S.arrows

Tactic:
rw [Equalizer.Presieve.sheaf_condition]

Premises used: CategoryTheory.Equalizer.Presieve.sheaf_condition
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Nonempty
    (IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows))
      (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows) ⋯))

Tactic:
⟨?_⟩

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
mpr :
  IsLimit (F :=
    parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
      (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
      (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows))
    (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows) ⋯)
⊢ Nonempty
    (IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
        (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows))
      (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows) ⋯))

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
mpr :
  IsLimit (F :=
    parallelPair (X := firstObj S.arrows P') (Y := secondObj S.arrows P') (firstMap S.arrows P')
        (secondMap S.arrows P') ⋙
      Functor.obj coyoneda (op U))
    (Functor.mapCone (Functor.obj coyoneda (op U)) (Fork.ofι (forkMap S.arrows P') ⋯))
⊢ IsLimit (F :=
    parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
      (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows)
      (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows))
    (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda (op U)) S.arrows) ⋯)

Tactic:
refine isSheafForIsSheafFor' _ _ _ _ ?_

Premises used: CategoryTheory.Presheaf.isSheafForIsSheafFor', DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
this : PreservesLimitsOfSize.{0, 0, max u₁ v₁, max u₁ v₁, u₂, (max u₁ v₁) + 1} (Functor.obj coyoneda (op U)) := ⋯
mpr :
  IsLimit (F :=
    parallelPair (X := firstObj S.arrows P') (Y := secondObj S.arrows P') (firstMap S.arrows P')
      (secondMap S.arrows P'))
    (Fork.ofι (forkMap S.arrows P') ⋯)
⊢ IsLimit (F :=
    parallelPair (X := firstObj S.arrows P') (Y := secondObj S.arrows P') (firstMap S.arrows P')
        (secondMap S.arrows P') ⋙
      Functor.obj coyoneda (op U))
    (Functor.mapCone (Functor.obj coyoneda (op U)) (Fork.ofι (forkMap S.arrows P') ⋯))

Tactic:
apply isLimitOfPreserves

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
this : PreservesLimitsOfSize.{0, 0, max u₁ v₁, max u₁ v₁, u₂, (max u₁ v₁) + 1} (Functor.obj coyoneda (op U)) := ⋯
apply : generate S.arrows ∈ (J : (a : C) → Set (Sieve a)) X
⊢ IsLimit (F :=
    parallelPair (X := firstObj S.arrows P') (Y := secondObj S.arrows P') (firstMap S.arrows P')
      (secondMap S.arrows P'))
    (Fork.ofι (forkMap S.arrows P') ⋯)

Tactic:
apply Classical.choice (h _ S.arrows _)

Premises used: Classical.choice, CategoryTheory.Sieve.arrows
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
this : PreservesLimitsOfSize.{0, 0, max u₁ v₁, max u₁ v₁, u₂, (max u₁ v₁) + 1} (Functor.obj coyoneda (op U)) := ⋯
⊢ generate S.arrows ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J (P ⋙ s)
rw :
  ∀ (h : ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op)))
    ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ IsSheaf J P

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isLimit
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Tactic:
fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t

Premises used: CategoryTheory.Limits.isLimitOfReflects, Nonempty.map
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Tactic:
exact fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J P
rw :
  ∀ (h : ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))) ⦃X : C⦄,
    ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ IsSheaf J (P ⋙ s)

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isLimit
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))

Tactic:
apply fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfPreserves s t

Premises used: Nonempty.map, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst_4 : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst_5 : s.ReflectsIsomorphisms
this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := ⋯
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩

Premises used: CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp, CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst_4 : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst_5 : s.ReflectsIsomorphisms
this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := ⋯
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
exact ⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst_2 : HasLimits A'
inst_3 : PreservesLimits s
inst_4 : s.ReflectsIsomorphisms
⊢ HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'

Tactic:
have : HasLimitsOfSize.{v₁, max v₁ u₁} A' := hasLimitsOfSizeShrink.{_, _, u₁, 0} A'
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst_2 : HasLimits A'
inst_3 : PreservesLimits s
inst_4 : s.ReflectsIsomorphisms
this : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
⊢ PreservesLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, max u₁ v₁, u₂, max (u₁ + 1) (v₁ + 1)} s

Tactic:
have : PreservesLimitsOfSize.{v₁, max v₁ u₁} s := preservesLimitsOfSize_shrink.{_, 0, _, u₁} s
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst_2 : HasLimits A'
inst_3 : PreservesLimits s
inst_4 : s.ReflectsIsomorphisms
this_1 : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
this : PreservesLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, max u₁ v₁, u₂, max (u₁ + 1) (v₁ + 1)} s
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Tactic:
apply isSheaf_iff_isSheaf_comp

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
n : ℕ
inst_3 : Injective F
⊢ Subsingleton.{w' + 1} (F.H (n + 1))

Tactic:
subsingleton_of_forall_eq 0 fun x ↦ (Ext.eq_zero_of_injective x)

Premises used: subsingleton_of_forall_eq, OfNat.ofNat, CategoryTheory.Abelian.Ext.eq_zero_of_injective
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
a :
  Eq.{w' + 1} (α := Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := ⋯ } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
          ((map f 0 : (a : F.H 0) → G.H 0) x)) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
                Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                  (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
                Ext.homEquiv₀;
              { toEquiv := __Equiv, map_add' := ⋯ } :
              (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
                (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
            x ≫
          f) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
⊢ Eq (α := Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)
    ((let __Equiv :
            Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
              (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
            Ext.homEquiv₀;
          { toEquiv := __Equiv, map_add' := ⋯ } :
          (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
            (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
        ((map f 0 : (a : F.H 0) → G.H 0) x) :
      Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)
    ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := ⋯ } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
          x ≫
        f :
      Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G)

Tactic:
apply (Ext.mk₀_bijective _ G).injective

Premises used: Function.Bijective.injective, CategoryTheory.Abelian.Ext.mk₀_bijective
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
a : (map f 0 : (a : F.H 0) → G.H 0) x = Ext.comp x (Ext.mk₀ f) ⋯
⊢ Eq.{w' + 1} (α := Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
              Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0 ≃
                (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ G) :=
              Ext.homEquiv₀;
            { toEquiv := __Equiv, map_add' := ⋯ } :
            (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) G 0) →
              (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ G)
          ((map f 0 : (a : F.H 0) → G.H 0) x)) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)
    (Ext.mk₀
        ((let __Equiv :
                Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) F 0 ≃
                  (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ)) ⟶ F) :=
                Ext.homEquiv₀;
              { toEquiv := __Equiv, map_add' := ⋯ } :
              (a : Ext ((constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ))) F 0) →
                (constantSheaf J AddCommGrpCat).obj (of (ULift.{w, 0} ℤ)) ⟶ F)
            x ≫
          f) :
      Ext (Functor.obj (constantSheaf J AddCommGrpCat) (of (ULift.{w, 0} ℤ))) G 0)

Tactic:
simp only [AddEquiv.coe_mk, Ext.mk₀_homEquiv₀_apply, Ext.mk₀_homEquiv₀_apply, ← Ext.mk₀_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, AddEquiv.coe_mk, CategoryTheory.Abelian.Ext.mk₀_homEquiv₀_apply
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (map f 0 : (a : F.H 0) → G.H 0) x = Ext.comp x (Ext.mk₀ f) ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
            (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
          (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
        ((equiv₀ F hT : (a : F.H 0) → (↑(F.obj.obj (op T)) : Type w)) x :
          (↑(F.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w)) ((map f 0 : (a : F.H 0) → G.H 0) x) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))

Tactic:
simp only [equiv₀, AddEquiv.trans_apply, addEquiv₀_map f x]

Premises used: CategoryTheory.Sheaf.H.addEquiv₀_map, AddEquiv.trans_apply, CategoryTheory.Sheaf.H.equiv₀
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : (↑(F.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w)
a :
  Eq.{w + 1} (α := (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
        ((map f 0 : (a : F.H 0) → G.H 0)
          ((AddEquiv.symm (equiv₀ F hT) : (a : (↑(F.obj.obj (op T)) : Type w)) → F.H 0) x : F.H 0)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
        ((AddEquiv.symm (equiv₀ G hT) : (a : (↑(G.obj.obj (op T)) : Type w)) → G.H 0)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
              (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
            x)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
⊢ Eq (α := G.H 0)
    ((map f 0 : (a : F.H 0) → G.H 0)
        ((AddEquiv.symm (equiv₀ F hT) : (a : (↑(F.obj.obj (op T)) : Type w)) → F.H 0) x : F.H 0) :
      G.H 0)
    ((AddEquiv.symm (equiv₀ G hT) : (a : (↑(G.obj.obj (op T)) : Type w)) → G.H 0)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
            (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
          x) :
      G.H 0)

Tactic:
apply (H.equiv₀ G hT).injective

Premises used: AddEquiv.injective, CategoryTheory.Sheaf.H.equiv₀