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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (M₂.map φ)) ((ConcreteCategory.hom (f.app X)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ConcreteCategory.hom (g.app X)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
i : IsIso f
⊢ Sieve.generate (Presieve.singleton f) = ⊤

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
⊢ S.arrows f → Sieve.pullback f R ∈ J Y

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
⊢ R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J Y

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (S.bind Ti))

Tactic:
rintro Y g ⟨W, h, g, hg, rfl⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ (Sieve.pullback f (Sieve.generate (S.bind Ti))).arrows (h ≫ g)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ (X : C), ⊤ ∈ Set.univ

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S R : Sieve X✝
J : GrothendieckTopology C
X Y : C
f : Sieve X
⊢ ∀ (f_1 : Y ⟶ X), f ∈ Set.univ → Sieve.pullback f_1 f ∈ Set.univ

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ Set.univ → ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ Set.univ) → R ∈ Set.univ

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
J : GrothendieckTopology C
hJ : J ∈ T
⊢ ⊤ ∈ (fun f ↦ ↑f X) ⟨J.sieves, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ sInf (sieves '' s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : J = ⊤
⊢ ∀ (X : C), ⊥ ∈ ⊤ X

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (f ≫ inv g) ≫ g = 𝟙 Y ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ ≫ pullback.snd g f = 𝟙 Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ¬⊥ < ⊤ ↔ IsEmpty C

Tactic:
simp

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

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.fst g f ≫ g ≫ inv g = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
x✝¹ : C
x✝ : Presieve x✝¹
⊢ x✝ ∈ (comap (𝟭 C) K).coverings x✝¹ ↔ x✝ ∈ K.coverings x✝¹

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
J : Precoverage E
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ (comap (F ⋙ G) J).coverings X ↔ Presieve.ofArrows Y f ∈ (comap F (comap G J)).coverings X

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑(S.pullback (𝟙 X))).arrows f ↔ (↑S).arrows f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝¹ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y✝ Z : C
S : J.Cover X
f✝ : Z ⟶ Y✝
g : Y✝ ⟶ X
Y : C
f : Y ⟶ Z
⊢ (↑(S.pullback (f✝ ≫ g))).arrows f ↔ (↑((S.pullback g).pullback f✝)).arrows f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ sInf ((fun J ↦ J.coverings) '' T) X ↔ ∀ t ∈ T, S ∈ t.coverings X

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows f

Tactic:
rw [← h3]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows (e1 ≫ e2)
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ F.hom.1 ≫ g₂.obj.hom = 𝟙 (unop (op g₁.obj.left)) ≫ g₁.obj.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ singleton (f default) (f default)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : IsEmpty ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ∀ (i : ι), ⊥ (f i)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve Y
T : Presieve X
⊢ R ≤ pullback f T → pushforward f R ≤ T

Tactic:
rintro hle Z - ⟨g, rfl, hg⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve Y
T : Presieve X
hle : R ≤ pullback f T
Z : C
g : Z ⟶ Y
hg : R g
⊢ T (g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
x✝¹ : C
x✝ : x✝¹ ⟶ X
⊢ pullback (𝟙 X) R x✝ = R x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
R : Presieve Z
g : X ⟶ Z
x✝¹ : C
x✝ : x✝¹ ⟶ Y
⊢ pullback (f ≫ g) R x✝ = pullback f (pullback g R) x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ F.map f₁ = 𝟙 (F.obj X) ≫ F.map f₁

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) = (g₁ ≫ G.map g₂) ≫ (F ⋙ G).map f₂

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
R : Presieve X
f : Y ⟶ X
h : R f
⊢ F.map f = 𝟙 (F.obj Y) ≫ F.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
x✝ : map F R f
Y✝ : C
u : Y✝ ⟶ X
hu : R u
⊢ F.map u = eqToHom ⋯ ≫ F.map u

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ singleton f f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝¹ : C
S : Sieve X✝
R : Presieve X✝
X Y✝ : C
f : X ⟶ Y✝
x : FamilyOfElements P (singleton f)
Y : C
⊢ (fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) ((fun x ↦ x f ⋯) x) X f ⋯ = x f ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S.arrows f ∧ R.arrows f → ∀ (g : Z ⟶ Y), S.arrows (g ≫ f) ∧ R.arrows (g ≫ f)

Tactic:
rintro _ _ _ ⟨h₁, h₂⟩ g
    simp [h₁, h₂]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ (fun x ↦ x f ⋯) ((fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) x) = x

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Presieve X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ (h ≫ g) ≫ f = h ≫ g ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x f hf) = x f hf

Tactic:
simp

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ∀ (hf : S.arrows f), x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)

Tactic:
hf

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ section_ f ≫ f = 𝟙 X

Tactic:
simp

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
⊢ ∀ (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (secondMap P S)) x)

Tactic:
hf

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
      ((ConcreteCategory.hom (firstMap P S)) x) =
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
      ((ConcreteCategory.hom (secondMap P S)) x)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ f = inv i ≫ i ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
i : I
⊢ 𝟙 (Y i) ≫ f i = f i

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
Y : C
f : Over S
hf : R f.hom
⊢ 𝟙 { obj := f, property := hf }.obj.left ≫ f.hom = { obj := f, property := hf }.obj.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
⊢ ∀ (hf : (Sieve.pullback f S).arrows f₁),
    FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ =
      (ConcreteCategory.hom (P.map f₂.op)) (FamilyOfElements.pullback f x f₁ hf)

Tactic:
hf

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ = (ConcreteCategory.hom (P.map f₂.op)) (FamilyOfElements.pullback f x f₁ hf)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ∀ (hf : S.arrows f),
    (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
      (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ a ≫ f i = (a ≫ f i ≫ e.inv) ≫ e.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows g

Tactic:
by exact Sieve.le_generate R W _ hg

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
⊢ Presieve.functorPullback F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)

Tactic:
hf

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
⊢ ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
S : Sieve (F.obj Y)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback F (pullback (F.map f) S)).arrows f✝ ↔ (pullback f (functorPullback F S)).arrows f✝

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
⊢ ∀ (h : S.arrows f), (ConcreteCategory.hom (P.map f.op)) t = x f h

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (g₂ ≫ f₂).op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map f''

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
⊢ ∀ (h : (generate R).arrows f), (ConcreteCategory.hom (P.map f.op)) t = x.sieveExtend f h

Tactic:
hf

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x.sieveExtend f hf
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ g ≫ β ≫ F.map α = (g ≫ β) ≫ F.map α

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ f = 𝟙 X ≫ (𝟭 C).map f

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
⊢ ∀ (h₁ : R f) (h₂ : R g),
    (ConcreteCategory.hom (P.map (pullback.fst f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x g h₂)

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
⊢ ∀ (h₂ : R g),
    (ConcreteCategory.hom (P.map (pullback.fst f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f hf) =
      (ConcreteCategory.hom (P.map (pullback.snd f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x g h₂)