mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{t, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
inst✝ : HasLimitsOfSize.{max t u v, max t u v, t, w} D
⊢ PreservesLimits (J.diagramFunctor D X)

Tactic:
by
  constructor
  intro _ _
  apply preservesLimitsOfShape_diagramFunctor.{max t u v}

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (ConcreteCategory.hom (G.obj.map g.op)) ((ConcreteCategory.hom (f.hom.app X)) (H.amalgamate t ht)) =
    (ConcreteCategory.hom (G.obj.map g.op)) s

Tactic:
rw [← NatTrans.naturality_apply, H.valid_glue ht]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op Y))) (t g ?mp.Hf) = (ConcreteCategory.hom (G.obj.map g.op)) s

case mp.Hf
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (Presheaf.imageSieve f.hom s).arrows g
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ (Ext.mk₀ (h.i ≫ h.r)).comp x ⋯ = 0

Tactic:
← Ext.mk₀_comp_mk₀,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ ((Ext.mk₀ h.i).comp (Ext.mk₀ h.r) ⋯).comp x ⋯ = 0
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 : Cᵒᵖ
r : ↑(R.obj.obj X)
⊢ smul α φ r 0 = 0

Tactic:
apply A.isSeparated _ _ (Presheaf.imageSieve_mem J α r)
  rintro Y f ⟨r₀, hr₀⟩
  rw [(A.obj.map f.op).hom.map_zero, map_smul_eq α φ r 0 f.op r₀ hr₀ 0 (by simp),
    smul_zero, map_zero]

Goal state after:
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 : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.obj.map f.op)) m'
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ + (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' =
    (ConcreteCategory.hom (A.obj.map f.op)) m + (ConcreteCategory.hom (A.obj.map f.op)) m'

Tactic:
hm₀,

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 : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.obj.map f.op)) m'
⊢ (ConcreteCategory.hom (A.obj.map f.op)) m + (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' =
    (ConcreteCategory.hom (A.obj.map f.op)) m + (ConcreteCategory.hom (A.obj.map f.op)) 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.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.obj.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.obj.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.obj.map f.op)) ((RingCat.Hom.hom (R.obj.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map (π ≫ f.op))) m

Tactic:
hm₀,

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.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.obj.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.obj.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.obj.map f.op)) ((RingCat.Hom.hom (R.obj.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m)
⊢ (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m) =
    (ConcreteCategory.hom (A.obj.map (π ≫ f.op))) m
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f : E.Hom F
⊢ E.sieve₀ ≤ F.sieve₀

Tactic:
Sieve.generate_le_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f : E.Hom F
⊢ Presieve.ofArrows E.X E.f ≤ F.sieve₀.arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation y₁
h₂ : x.IsAmalgamation y₂
⊢ y₁ = y₂

Tactic:
refine hS.1.ext (fun Y g hg => ?_)

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation y₁
h₂ : x.IsAmalgamation y₂
Y : C
g : Y ⟶ X
hg : S g
⊢ (ConcreteCategory.hom (P.map g.op)) y₁ = (ConcreteCategory.hom (P.map g.op)) y₂
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g

Tactic:
obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1

Goal state after:
case of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
X : C
R : Presieve X
hR : R ∈ J.coverings X
⊢ ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hR : Presieve.ofArrows Y f ∈ J.coverings X
⊢ ∃ 𝒰, Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)

Goal state after:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve (E.X i)
hR' : R' ∈ J.coverings (E.X i)
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
R : Presieve X
inst✝¹ : R.HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks R
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)

Tactic:
have : (R.map F).HasPairwisePullbacks := .map_of_preservesPairwisePullbacks _ _

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
R : Presieve X
inst✝¹ : R.HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks R
this : (map F R).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
R : Presieve X
inst✝¹ : R.HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks R
this : (map F R).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (map F (ofArrows Y f)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y 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
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
⊢ K.W (H.map f)

Tactic:
by
  intro U hU
  rw [adj.map_comp_bijective_iff]
  exact hf _ (F.op_comp_isSheaf_of_isSheaf _ _ _ hU)

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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
⊢ ∀ (G : Sheaf K (Type (max u₁ v₁ u₂ v₂))), Presieve.IsSheaf J (F.op ⋙ G.obj)

Tactic:
rintro ⟨P, hP⟩
    rw [← isSheaf_iff_isSheaf_of_type]
    exact F.op_comp_isSheaf_of_preservesOneHypercovers J K P hP

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
U V : C
f : G.obj U ⟶ G.obj V
Y₁ Y₂ : C
i₁ : Y₁ ⟶ U
l : Y₁ ⟶ V
hl : G.map l = G.map i₁ ≫ f
i₂ : Y₂ ⟶ Y₁
⊢ G.map (i₂ ≫ l) = G.map (i₂ ≫ i₁) ≫ f

Tactic:
simp [hl]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_5)
X : D
s t : ℱ.obj.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄,
    (Sieve.coverByImage G X).arrows f →
      (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t

Tactic:
rintro Y _ ⟨Z, f₁, f₂, ⟨rfl⟩⟩

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_5)
X : D
s t : ℱ.obj.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ (ConcreteCategory.hom (ℱ.obj.map (f₁ ≫ f₂).op)) s = (ConcreteCategory.hom (ℱ.obj.map (f₁ ≫ f₂).op)) t
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
⊢ G.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯) = G.map (I.f ≫ i) ≫ g₁

Tactic:
simp [hl]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.obj).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (𝟙 (G.obj U)), ⋯⟩
⊢ G.map (l I.Y U U I.f (𝟙 (G.obj U)) ⋯) = G.map I.f

Tactic:
simp [hl]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
J : GrothendieckTopology E
⊢ F.inducedTopology (G.inducedTopology J) ≤ (F ⋙ G).inducedTopology J

Tactic:
le_inducedTopology_iff

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
J : GrothendieckTopology E
⊢ (F ⋙ G).IsContinuous (F.inducedTopology (G.inducedTopology J)) J
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ F.inducedTopology K ≤ G.inducedTopology K

Tactic:
le_inducedTopology_iff

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ G.IsContinuous (F.inducedTopology K) K
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ G.inducedTopology K ≤ F.inducedTopology K

Tactic:
le_inducedTopology_iff

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ F.IsContinuous (G.inducedTopology K) K
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.restrictedTopology K ≤ F.inducedTopology K

Tactic:
le_inducedTopology_iff

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.IsContinuous (F.restrictedTopology K) K
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
Z : C
f : Z ⟶ Y.left
⊢ ((overEquiv Y) S).arrows f ↔ S.arrows (Over.homMk f ⋯)

Tactic:
obtain ⟨S, rfl⟩ := (overEquiv Y).symm.surjective S
  simp

Goal state after:
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
e : M ≅ N
σ : N.GeneratingSections
⊢ (fun σ ↦ σ.ofEpi e.hom) ((fun σ ↦ σ.ofEpi e.inv) σ) = σ

Tactic:
dsimp
    simp only [← opEpi_comp, e.inv_hom_id, opEpi_id]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
this :
  (F.asEquivalence.inverse ⋙ F.asEquivalence.functor).obj (F.asEquivalence.functor.obj X) ≅
    (𝟭 D).obj (F.asEquivalence.functor.obj X)
⊢ Simple (F.asEquivalence.functor.obj X)

Tactic:
Functor.comp_obj,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
this :
  F.asEquivalence.functor.obj (F.asEquivalence.inverse.obj (F.asEquivalence.functor.obj X)) ≅
    (𝟭 D).obj (F.asEquivalence.functor.obj X)
⊢ Simple (F.asEquivalence.functor.obj X)