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₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
⊢ (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)

Tactic:
have ha₁ : (α.app (Opposite.op Y₁)) a₁ = (R.map f₁.op) r := (hr₀ f₁ h₁).symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
⊢ (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N₁ N₂ : M.Submodule
h : ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X
⊢ N₁ = N₂

Tactic:
by
  cases N₁; cases N₂; congr 1; ext X : 1; exact h X

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := ⋯
⊢ Ext.homEquiv₀.symm (𝟙 X) = Ext.homEquiv₀.symm 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ Ext.mk₀ (𝟙 X) = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)
E✝ X✝ : C
f : X ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
φ : X ⟶ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.X₂
hφ :
  (Ext.homEquiv₀.symm φ).comp (Ext.mk₀ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.g) ⋯ =
    Ext.mk₀ f
⊢ Ext.homEquiv₀.symm (φ ≫ g) = Ext.homEquiv₀.symm f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)
E✝ X✝ : C
f : X ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
φ : X ⟶ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.X₂
hφ :
  (Ext.homEquiv₀.symm φ).comp (Ext.mk₀ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.g) ⋯ =
    Ext.mk₀ f
⊢ Ext.mk₀ (φ ≫ g) = Ext.mk₀ f
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
e : Ext X Y d
hd : d = n + 0
⊢ d = n

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
e : Ext X Y d
hd : d = n + 0
⊢ d = n
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n + 1 ≤ i

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n < i
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ projectiveDimension X = ⊥ ↔ Limits.IsZero X

Tactic:
by
  rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
⊢ projectiveDimension M ≤ ⊥ ↔ projectiveDimension N ≤ ⊥

Tactic:
simpa using

Goal state after:
case bot
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
⊢ Subsingleton ↑M ↔ Subsingleton ↑N
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n ↔ projectiveDimension N ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
n : ℕ∞
⊢ projectiveDimension M ≤ ↑n ↔ projectiveDimension N ≤ ↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : Ring R
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : CategoryTheory.Projective M
⊢ projectiveDimension M = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : Ring R
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : CategoryTheory.Projective M
⊢ CategoryTheory.Projective M ∧ Nontrivial ↑M
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' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
⊢ (ConcreteCategory.hom (A.obj.map f)) a = (ConcreteCategory.hom (φ.app Y)) (a₀ • b₀)

Tactic:
apply A.isSeparated _ _ (J.pullback_stable f.unop hS)
    rintro Z g hg
    dsimp at hg
    rw [← ConcreteCategory.comp_apply, ← A.obj.map_comp, ← NatTrans.naturality_apply (D := Ab)]
    erw [M₀.map_smul] -- Mismatch between `M₀.map` and `M₀.presheaf.map`
    refine (ha _ hg).trans (app_eq_of_isLocallyInjective α φ A.isSeparated _ _ _ _ ?_ ?_)
    · rw [← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply, ha₀]
      apply (hr₀ _ hg).symm.trans
      simp
    · erw [NatTrans.naturality_apply φ, hb₀]
      apply (hm₀ _ hg).symm.trans
      dsimp
      rw [Functor.map_comp]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
a : α
⊢ (Sigma.ι (fun x ↦ R) (f a) ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) (f a) ≫ s.π

Tactic:
simpa using

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
a : α
⊢ 0 = Sigma.ι (fun x ↦ R) (f a) ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∉ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π

Tactic:
· simp [ι_sigmaConstCokernelCofork_π_assoc _ _ _ hb]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_unop
    exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
c₂ :
  Cone
    { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom))).map f ≫
      StructuredArrow.homMk (StructuredArrow.Hom.right (c₂.π.app j')) ⋯ =
    StructuredArrow.homMk (StructuredArrow.Hom.right (c₂.π.app j)) ⋯ ≫ H.map f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
c₂ :
  Cone
    { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
j j' : J
f : j ⟶ j'
⊢ StructuredArrow.Hom.right (c₂.π.app j') = StructuredArrow.Hom.right (c₂.π.app j) ≫ StructuredArrow.Hom.right (H.map f)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case h
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : val✝¹ ⟶ val✝
⊢ f ∈ Fintype.elems ∧ BiconeHom.diagram f = BiconeHom.diagram f

Tactic:
simpa using

Goal state after:
case h
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : val✝¹ ⟶ val✝
⊢ f ∈ Fintype.elems
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (𝟙 F).s₀
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (𝟙 F).h₀ i ≫ eqToHom ⋯
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (𝟙 F).s₀
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (𝟙 F).h₀ i ≫ eqToHom ⋯
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: 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
hS : S ∈ J.toGrothendieck X
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
simpa using

Goal state after:
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
hS : S ∈ J.toGrothendieck X
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows
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:
intro Y 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:
intro Y 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: 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 }
i✝ : ↑R.uncurry ⊕ ↑T.uncurry
i : ↑R.uncurry
⊢ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) (Sum.inl i) ⟶ S

Tactic:
by exact (eR _ i.2).hom ≫ i.1.2

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

Goal state before:
pp: case mpr.transitive.refine_1.h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
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)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ (Sieve.pullback f S).arrows (gg ≫ g)

Tactic:
simpa using

Goal state after:
case mpr.transitive.refine_1.h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
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)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ S.arrows (gg ≫ g ≫ f)