mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

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
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (M.freeHomEquiv.symm σ.s ≫ p)

Tactic:
]

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
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (M.freeHomEquiv.symm σ.s ≫ p)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

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
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso ((mapFreeIso F G.I η).hom ≫ F.map G.π)

Tactic:
]

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
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso ((mapFreeIso F G.I η).hom ≫ F.map G.π)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
this : IsIso u
⊢ (functorPullback (Over.map f) S).arrows (Over.homMk g ⋯) ↔ S.arrows (Over.homMk g ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
this : IsIso u
⊢ (functorPullback (Over.map f) S).arrows (Over.homMk g ⋯) ↔ S.arrows (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (Sieve.ofArrows (E.refineOneHypercover F).Y fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).sieve₀

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (Sieve.ofArrows (E.refineOneHypercover F).Y fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).sieve₀
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ (overEquiv U) (functorPullback (Over.post F) S) ≤ functorPullback F ((overEquiv ((Over.post F).obj U)) S)

Tactic:
dsimp [Sieve.overEquiv]

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPushforward (Over.forget X) (functorPullback (Over.post F) S) ≤
    functorPullback F (functorPushforward (Over.forget (F.obj X)) S)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ ((isomorphisms (Sheaf J Ab)).inverseImage (presheafToSheaf J Ab)).inverseImage (toPresheaf R₀) =
    (isomorphisms (SheafOfModules R)).inverseImage (sheafification α)

Tactic:
]

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ ((isomorphisms (Sheaf J Ab)).inverseImage (presheafToSheaf J Ab)).inverseImage (toPresheaf R₀) =
    (isomorphisms (SheafOfModules R)).inverseImage (sheafification α)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization ((MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (sheafification α))

Tactic:
]

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization ((MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (sheafification α))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ (functorPullback (Over.post F) S).arrows (Over.homMk g ⋯)

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ (functorPullback (Over.post F) S).arrows (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁) S₁) ∈ J Y₂.left

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁) S₁) ∈ J Y₂.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : Sieve.pullback (Over.Hom.left (Over.homMk f ⋯)) ((Sieve.overEquiv Y) R) ∈ J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : Sieve.pullback (Over.Hom.left (Over.homMk f ⋯)) ((Sieve.overEquiv Y) R) ∈ J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₁ hg₁)

Tactic:
]

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₁ hg₁)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₁.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op

Tactic:
]

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₁.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₂ hg₂)

Tactic:
]

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op

Tactic:
]

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J ((Over.map f).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.map f) S) ∈ J U.left

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J ((Over.map f).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.map f) S) ∈ J U.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J ((Over.map f).obj U).left
⊢ (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J U.left

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J ((Over.map f).obj U).left
⊢ (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J U.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.post F) S) ∈ J U.left

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.post F) S) ∈ J U.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ Sieve.functorPullback F ((Sieve.overEquiv ((Over.post F).obj U)) S) ∈ J U.left

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ Sieve.functorPullback F ((Sieve.overEquiv ((Over.post F).obj U)) S) ∈ J U.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ (Sieve.overEquiv ((Over.post F).obj U)) (Sieve.functorPushforward (Over.post F) S) ∈ K ((Over.post F).obj U).left

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ (Sieve.overEquiv ((Over.post F).obj U)) (Sieve.functorPushforward (Over.post F) S) ∈ K ((Over.post F).obj U).left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ Sieve.functorPushforward F ((Sieve.overEquiv U) S) ∈ K ((Over.post F).obj U).left

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ Sieve.functorPushforward F ((Sieve.overEquiv U) S) ∈ K ((Over.post F).obj U).left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ Sieve.functorPushforward (Over.forget X) E.sieve₀ ∈ J Y.left

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ Sieve.functorPushforward (Over.forget X) E.sieve₀ ∈ J Y.left
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree

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 : Type u
⊢ IsIso (𝟙 (free I))

Tactic:
]

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 : Type u
⊢ IsIso (𝟙 (free I))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this✝ : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
this :
  (E.map (Over.forget X)).sieve₁ (Over.Hom.left (Over.homMk p₁ ⋯)) (Over.Hom.left (Over.homMk p₂ ⋯)) ∈
    J (Over.mk (p₁ ≫ (E.X i₁).hom)).left
⊢ (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this✝ : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
this :
  (E.map (Over.forget X)).sieve₁ (Over.Hom.left (Over.homMk p₁ ⋯)) (Over.Hom.left (Over.homMk p₂ ⋯)) ∈
    J (Over.mk (p₁ ≫ (E.X i₁).hom)).left
⊢ (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (Sieve.ofArrows (fun i ↦ ((Over.post F).obj (E.X i)).left) fun i ↦ Over.Hom.left ((Over.post F).map (E.f i))) ∈
    K ((Over.post F).obj Y).left

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (Sieve.ofArrows (fun i ↦ ((Over.post F).obj (E.X i)).left) fun i ↦ Over.Hom.left ((Over.post F).map (E.f i))) ∈
    K ((Over.post F).obj Y).left