mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
⊢ ∀ (s_1 s' : d ⟶ (Pi.eval I s).obj c), ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
f

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
f : d ⟶ (Pi.eval I s).obj c
⊢ ∀ (s' : d ⟶ (Pi.eval I s).obj c), ∃ c' t, f ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
d : I s
c : (i : α) → I i
⊢ ∀ (s_1 s' : (Pi.eval I s).obj c ⟶ d), ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
f

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
d : I s
c : (i : α) → I i
f : (Pi.eval I s).obj c ⟶ d
⊢ ∀ (s' : (Pi.eval I s).obj c ⟶ d), ∃ c' t, (Pi.eval I s).map t ≫ f = (Pi.eval I s).map t ≫ s'
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
⊢ P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } } ≫
      (coneOfConeUncurry Q c).π.app j =
    s.π.app j

Tactic:
apply (Q j).hom_ext
    intro k
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
⊢ (coconeOfCoconeUncurry Q c).ι.app j ≫
      P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
apply (Q j).hom_ext
    intro k
    simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
r : ↑(R.obj U)
m₁ m₂ : ↑(M.obj U)
⊢ (ιR cR) r • (ιM m₁ + ιM m₂) = (ιR cR) r • ιM m₁ + (ιR cR) r • ιM m₂

Tactic:
simp only [smul_eq, smul_add, ← map_add]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
⊢ Sieve.pullback i S ∈ J X ↔ S ∈ J Y

Tactic:
refine ⟨fun H ↦ ?_, J.pullback_stable i⟩

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

Tactic:
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 : 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:
f

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
⊢ 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:
f

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
⊢ R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

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

Tactic:
refine ⟨fun h ↦ ⟨fun X ↦ ?_⟩, fun h ↦ eq_top_of_isEmpty _⟩
  apply bot_ne_top (α := Sieve X)
  simp only [← GrothendieckTopology.bot_covering, h, top_covering]

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
S : Sieve X
h : Y ⟶ X
H : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Z : C
⊢ ∀ (f : Z ⟶ Y), ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Z : C
f : Z ⟶ Y
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
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 g, R.arrows (g ≫ f)

Tactic:
f

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 g, R.arrows (g ≫ f)
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:
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
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ ((ofArrows Z g).bind fun x f H ↦ ofArrows (W f H) (k f H)) =
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
funext Y

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
⊢ ((ofArrows Z g).bind fun x f H ↦ ofArrows (W f H) (k f H)) =
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
⊢ ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Exists.choose ⋯ = s.ι.app j

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f
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:
f

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.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:
f

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.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = x₂

Tactic:
← extend_restrict t₂

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend
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:
f

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
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:
f

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
⊢ Presieve.functorPullback F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)
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:
f

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
⊢ ∀ (h : S.arrows f), (ConcreteCategory.hom (P.map f.op)) t = x f h
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
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R

Tactic:
funext Y

Goal state after:
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
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
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:
f

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
⊢ ∀ (h : (generate R).arrows f), (ConcreteCategory.hom (P.map f.op)) t = x.sieveExtend f h
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
⊢ ∀ {f : Y✝ ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPushforward F R.arrows (g ≫ f)

Tactic:
f

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 X
Y✝ Z✝ : D
f : Y✝ ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPushforward F R.arrows (g ≫ f)
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⦄ ⦃f₂ : Z ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂),
    (ConcreteCategory.hom (P.map (pullback.fst f₁ f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₁ h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f₁ f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₂ h₂)

Tactic:
f

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
⊢ ∀ ⦃f₂ : Z ⟶ X⦄ (h₁ : R f) (h₂ : R f₂),
    (ConcreteCategory.hom (P.map (pullback.fst f f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₂ h₂)
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
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
⊢ ∀ (f : X ⟶ X✝), R.arrows f → (functorPullback F S).arrows f

Tactic:
f

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
⊢ R.arrows f → (functorPullback F S).arrows 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✝ 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), S.arrows f → (functorPushforward F (functorPullback F S)).arrows f

Tactic:
f

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
⊢ S.arrows f → (functorPushforward F (functorPullback F S)).arrows f
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X✝ : C
S : Sieve X✝
R : Presieve X✝
E : Aᵒᵖ
π : (S.arrows.diagram.op ⋙ P).cones.obj E
X Y : C
f : X ⟶ X✝
g : Y ⟶ X
hf : S.arrows f
⊢ (fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) Y (g ≫ f) ⋯ =
    (ConcreteCategory.hom ((P ⋙ coyoneda.obj E).map g.op))
      ((fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) X f hf)

Tactic:
by
      let φ : S.arrows.categoryMk (g ≫ f) (S.downward_closed hf g) ⟶
        S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ rfl)
      simpa using! π.naturality φ.op

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
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y Z : C
⊢ ∀ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f),
    (fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Z (g ≫ f) ⋯ =
      (ConcreteCategory.hom (F.map g.op))
        ((fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Y f hf)

Tactic:
f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y Z : C
f : Y ⟶ X
⊢ ∀ (g : Z ⟶ Y) (hf : S.arrows f),
    (fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Z (g ≫ f) ⋯ =
      (ConcreteCategory.hom (F.map g.op))
        ((fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Y 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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
⊢ ∀ (f : Y ⟶ X) (h : R f), (ConcreteCategory.hom (P.map f.op)) t = x f h

Tactic:
f

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 : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
⊢ ∀ (h : R f), (ConcreteCategory.hom (P.map f.op)) t = x f h
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y) (g : Y ⟶ Z),
    colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (g : Y ⟶ Z),
    colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ e ((ConcreteCategory.hom (P₁.map g₁.op)) (x₁ f₁ h₁)) = e ((ConcreteCategory.hom (P₁.map g₂.op)) (x₁ f₂ h₂))

Tactic:
simp only [he, Equiv.apply_symm_apply, hx₂ g₁ g₂ h₁ h₂ fac, x₁]

Goal state after: