mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
⊢ x✝ ∈ F.obj U✝ ⊔ G.obj U✝ → x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)

Tactic:
by
        rintro (h | h)
        · exact Or.inl (F.map _ h)
        · exact Or.inr (G.map _ h)

Goal state after:
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)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m₁ : ↑(M₁.obj X✝)
m₂ : ↑(M₂.obj X✝)
⊢ (ConcreteCategory.hom (M₁.map (f ≫ g))) m₁ ⊗ₜ[↑(R.obj Z✝)] (ConcreteCategory.hom (M₂.map (f ≫ g))) m₂ =
    (ConcreteCategory.hom (M₁.map g)) ((ConcreteCategory.hom (M₁.map f)) m₁) ⊗ₜ[↑(R.obj Z✝)]
      (ConcreteCategory.hom (M₂.map g)) ((ConcreteCategory.hom (M₂.map f)) m₂)

Tactic:
simp +instances

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
R : Presieve X
hR : R ∈ {R | Sieve.generate R ∈ J X}
⊢ pullbackArrows f R ∈ {R | Sieve.generate R ∈ J Y}

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ {R | Sieve.generate R ∈ J X}
⊢ Sieve.pullback f (Sieve.generate R) ∈ 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 : C⦄ ⦃f : Y ⟶ X⦄, (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ J Y

Tactic:
intro Y f

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 : C
f : Y ⟶ X
⊢ (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : J.Covers S f
hR : J.Covers R f
⊢ J.Covers (S ⊓ R) f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : J.Covers S f
hR : J.Covers R f
⊢ Sieve.pullback f S ∈ J Y ∧ Sieve.pullback f R ∈ J Y
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
hS : S.arrows (𝟙 X)
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R ∈ {⊤}

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S.arrows (𝟙 X)
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R = ⊤
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
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ R.arrows ((h ≫ g) ≫ f)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ R.arrows (h ≫ g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
R : Presieve Y
hR : R ∈ J.coverings Y
inst✝ : R.HasPullbacks f
⊢ Presieve.pullbackArrows f R ∈ J.coverings X

Tactic:
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
⊢ Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X
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
F : C ⥤ D
J K : Precoverage D
inst✝ : J.HasIsos
S T : C
f : S ⟶ T
hf : IsIso f
⊢ Presieve.singleton f ∈ (comap F J).coverings T

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝ : J.HasIsos
S T : C
f : S ⟶ T
hf : IsIso f
⊢ Presieve.singleton (F.map f) ∈ J.coverings (F.obj T)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
R : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → R f → Presieve Y
hR : R ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : R f), Ti f H ∈ J.coverings Y
⊢ R.bind Ti ∈ J.coverings X

Tactic:
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (generate R)).arrows

Tactic:
intro Y f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows
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
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : D
i : ι
hu : ofArrows Y✝ f (eqToHom ⋯ ≫ f i)
⊢ ofArrows (fun i ↦ F.obj (Y✝ i)) (fun i ↦ F.map (f i)) (F.map (eqToHom ⋯ ≫ f i))

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : D
i : ι
hu : ofArrows Y✝ f (eqToHom ⋯ ≫ f i)
⊢ ofArrows (fun i ↦ F.obj (Y✝ i)) (fun i ↦ F.map (f i)) (F.map (f i))
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
s : Presieve X
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s

Tactic:
by
  refine funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩
  · rintro ⟨_, _, _, ⟨hu⟩, rfl⟩; exact ⟨_, _, _, hu, rfl⟩
  · rintro ⟨_, _, _, hu, rfl⟩; exact ⟨_, _, _, ⟨hu⟩, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
f₁ : Y ⟶ X
f₂ : Z ⟶ X
hf₁ : R f₁
hf₂ : R f₂
heq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map g₁.op)) (x f₁ hf₁)) =
    (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂))

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
f₁ : Y ⟶ X
f₂ : Z ⟶ X
hf₁ : R f₁
hf₂ : R f₂
heq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (Q.map g₁.op)) ((ConcreteCategory.hom (f.app (op Y))) (x f₁ hf₁)) =
    (ConcreteCategory.hom (Q.map g₂.op)) ((ConcreteCategory.hom (f.app (op Z))) (x f₂ hf₂))
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:
simpa using

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 : C
S : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f
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
x : FamilyOfElements P S.arrows
t : x.Compatible
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
x : FamilyOfElements P S.arrows
t : x.Compatible
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)
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:
simpa using

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.fst)) ⟨Z, ⟨g ≫ f, ⋯⟩⟩)) x =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) x)
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 :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((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:
simpa using

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 :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (secondMap P S)) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Z, ⟨g ≫ f, ⋯⟩⟩)) x =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) x)
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 : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) f hf = x f hf

Tactic:
simpa using

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 : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ (ConcreteCategory.hom
        (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
          { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
      ((ConcreteCategory.hom (firstMap P R)) x) =
    (ConcreteCategory.hom
        (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
          { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
      ((ConcreteCategory.hom (secondMap P R)) x)

Tactic:
simpa using

Goal state after:
case mp
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 : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (P.map (pullback.fst f g).op))
      ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) x) =
    (ConcreteCategory.hom (P.map (pullback.snd f g).op))
      ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Z, ⟨g, hg⟩⟩)) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

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

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
Y : C
u : Y ⟶ X
hu : R u
⊢ (ConcreteCategory.hom (Q.map u.op)) ((ConcreteCategory.hom (f.app (op X))) t) =
    (ConcreteCategory.hom (f.app (op Y))) (x u hu)
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 :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (firstMap P R)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (secondMap P R)) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : 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 hg)

Tactic:
simpa using

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 :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (firstMap P R)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (secondMap P R)) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ (ConcreteCategory.hom (P.map (pullback.fst f g).op))
      ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) x) =
    (ConcreteCategory.hom (P.map (pullback.snd f g).op))
      ((ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Z, ⟨g, hg⟩⟩)) x)
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
x : FirstObj P R
⊢ Presieve.FamilyOfElements.Compatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x) ↔
    (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

Tactic:
rw [Presieve.pullbackCompatible_iff]
  constructor
  · intro t
    apply Limits.Types.limit_ext
    rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
    simpa [firstMap, secondMap] using t hf hg
  · intro t Y Z f g hf hg
    rw [Types.limit_ext_iff'] at t
    simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, 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
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPullback F S).arrows (F.preimage ((F.objObjPreimageIso Y).hom ≫ f)) ∧
    f = (F.objObjPreimageIso Y).inv ≫ F.map (F.preimage ((F.objObjPreimageIso Y).hom ≫ f))

Tactic:
simpa using

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
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ S.arrows f
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : R f
⊢ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) f hf = x f hf

Tactic:
simpa using

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
Z : C
iZX : Z ⟶ X
iYZ : Y ⟶ e.functor.obj Z
hiZX : S.arrows iZX
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows (iYZ ≫ e.functor.map iZX)

Tactic:
simpa using

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
Z : C
iZX : Z ⟶ X
iYZ : Y ⟶ e.functor.obj Z
hiZX : S.arrows iZX
⊢ S.arrows (e.inverse.map iYZ ≫ e.unitInv.app Z ≫ iZX)
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
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t

Tactic:
intro hu

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hu : ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
⊢ ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
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
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ (hom (f.app Y)).toFun y = (hom (g.app Y)).toFun y

Tactic:
simpa using

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
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ ↑((hom (f.app Y)) y) = ↑((hom (g.app Y)) y)