mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
⊢ ∀ (f : Y ⟶ Opposite.unop X),
    S.arrows f → (ConcreteCategory.hom (A.obj.map f.op)) x₁ = (ConcreteCategory.hom (A.obj.map f.op)) x₂

Tactic:
f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
⊢ S.arrows f → (ConcreteCategory.hom (A.obj.map f.op)) x₁ = (ConcreteCategory.hom (A.obj.map f.op)) x₂
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: I : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : Bicategory B
inst✝ : Strict B
F : I ⥤ B
b₀✝ b₁✝ b₂✝ : LocallyDiscrete I
f : b₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
⊢ (match f ≫ g with
    | { as := f } => F.map f) =
    (match f with
      | { as := f } => F.map f) ≫
      match g with
      | { as := f } => F.map f

Tactic:
by obtain ⟨f⟩ := f; obtain ⟨g⟩ := g; simp [CategoryStruct.comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
i : I
⊢ (free J).unitHomEquiv.symm ((free J).freeHomEquiv (freeMap f) i) = ιFree (f i)

Tactic:
freeHomEquiv_freeMap

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
i : I
⊢ (free J).unitHomEquiv.symm ((freeSection ∘ f) i) = ιFree (f i)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ HasFiniteLimits (StructuredArrow X F)

Tactic:
by
      apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
      exact fun _ _ _ => HasLimitsOfShape.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
Y : C
⊢ ∀ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ J₁ Y

Tactic:
f

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
Y : C
f : Y ⟶ X
⊢ ⊤.arrows f → Sieve.pullback f S ∈ J₁ Y
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
Y : C
⊢ ∀ (f : Y ⟶ X), ⊤.arrows f → (J₁.close S).arrows f

Tactic:
f

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
Y : C
f : Y ⟶ X
⊢ ⊤.arrows f → (J₁.close S).arrows f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
⊢ ∀ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
⊢ ∀ (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
⊢ ∀ (f : Y ⟶ X) (h : S.arrows f),
    (ConcreteCategory.hom ((Functor.closedSieves J₁).toFunctor.map f.op)) ⟨J₁.close M, ⋯⟩ = x f h

Tactic:
f

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
⊢ ∀ (h : S.arrows f), (ConcreteCategory.hom ((Functor.closedSieves J₁).toFunctor.map f.op)) ⟨J₁.close M, ⋯⟩ = x f h
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
Y : C
⊢ ∀ (f : Y ⟶ X), J.Covers ⊤ f → ⊤.arrows f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
Y : C
f : Y ⟶ X
⊢ J.Covers ⊤ f → ⊤.arrows f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
⊢ ∀ (f : Y ⟶ X), S.arrows f → ((c X) R).arrows f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
f : Y ⟶ X
⊢ S.arrows f → ((c X) R).arrows f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.pullback
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y✝ : C
f : Y✝ ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
⊢ ∀ (f_1 : Y ⟶ Y✝), Presieve.IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows

Tactic:
f

Goal state after:
case mpr.pullback
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y✝ : C
f✝ : Y✝ ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y✝
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback f✝ S)).arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.transitive
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
Y : C
⊢ ∀ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
f

Goal state after:
case mpr.transitive
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
Y : C
⊢ R ≤ R.preZeroHypercover.presieve₀

Tactic:
f

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
Y : C
f : Y ⟶ S
⊢ R f ≤ R.preZeroHypercover.presieve₀ f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
⊢ E ≅ F

Tactic:
refine PreZeroHypercover.isoMk (Equiv.refl _) (fun i ↦ ?_) (fun i ↦ ?_)
    · match i with
      | .inl i => dsimp [E, F]; symm; exact eR _ _
      | .inr i => dsimp [E, F]; apply eT
    · cases i <;> simp [E, F]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
⊢ ∀ (f : Y ⟶ X), ∀ S ∈ {S | Sieve.generate S ∈ J X}, ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f

Tactic:
f

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
⊢ ∀ S ∈ {S | Sieve.generate S ∈ J X}, ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝³ : Category.{v_1, ?u.2} C
inst✝² : Category.{v_2, ?u.4} D
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ J.coverings X
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f

Tactic:
by
    have : S.HasPullbacks f := J.hasPullbacks_of_mem _ hS
    exact ⟨S.pullbackArrows f, J.pullbackArrows_mem _ hS,
      Presieve.FactorsThruAlong.pullbackArrows f S⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : Coverage C
⊢ J.toGrothendieck = J.toGrothendieck

Tactic:
by
  rw [Coverage.toGrothendieck, GrothendieckTopology.copy_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
⊢ ∀ {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
f

Goal state after:
case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
⊢ ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
⊢ ∀ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows

Tactic:
f

Goal state after:
case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
Y : C
⊢ ∀ (f : Y ⟶ X), S.arrows f → m ≫ P.map f.op = lift hP hE le F ≫ P.map f.op

Tactic:
f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
Y : C
f : Y ⟶ X
⊢ S.arrows f → m ≫ P.map f.op = lift hP hE le F ≫ P.map f.op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesRightKanExtension F L
inst✝ : L.HasRightKanExtension F
a : A
⊢ (G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫ G.map ((L.rightKanExtensionCounit F).app a) =
    (L.rightKanExtensionCounit (F ⋙ G)).app a

Tactic:
by
  simpa [-rightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (rightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
⊢ ∀ (f : Y ⟶ W), (E.sieve₁ p₁ p₂).arrows f → (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f

Tactic:
f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
⊢ (E.sieve₁ p₁ p₂).arrows f → (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve X
hR : R ∈ J.toCoverage.coverings X
this✝ : F.PreservesPairwisePullbacks R
this : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor (F.op ⋙ { obj := G, property := H✝ }.obj) R

Tactic:
rw [Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve X
hR : R ∈ J.toCoverage.coverings X
this✝ : F.PreservesPairwisePullbacks R
this : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor { obj := G, property := H✝ }.obj (Presieve.map F R)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
Y : C
⊢ ∀ (f : Y ⟶ U),
    (Sieve.functorPullback F (Sieve.pullback (e.hom.app U) S)).arrows f → (Sieve.functorPullback G S).arrows f

Tactic:
f

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
Y : C
f : Y ⟶ U
⊢ (Sieve.functorPullback F (Sieve.pullback (e.hom.app U) S)).arrows f → (Sieve.functorPullback G S).arrows f
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve U
hS : S ∈ K U
X : C
⊢ ∀ (f : X ⟶ G.obj U),
    (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f → (Sieve.functorPushforward G S).arrows f

Tactic:
f

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve U
hS : S ∈ K U
X : C
f : X ⟶ G.obj U
⊢ (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f → (Sieve.functorPushforward G S).arrows f
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
hS : S ∈ K (F.obj U)
X : C
⊢ ∀ (f : X ⟶ U),
    (Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S)).arrows f → (Sieve.functorPullback F S).arrows f

Tactic:
f

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
hS : S ∈ K (F.obj U)
X : C
f : X ⟶ U
⊢ (Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S)).arrows f → (Sieve.functorPullback F S).arrows f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (E.sieve₁ p₁ p₂).arrows g → (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g

Tactic:
rintro ⟨j, h, fac₁, fac₂⟩

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
⊢ (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
Y : C
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac : h ≫ E.toPullback j = g ≫ pullback.lift p₁ p₂ w
⊢ g ≫ p₁ = h ≫ E.p₁ j

Tactic:
by simpa using fac.symm =≫ pullback.fst _ _

Goal state after: