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

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
rw [Functor.final_iff_of_isFiltered]
  constructor
  · rintro ⟨h, _⟩ j₂
    obtain ⟨j₁, ⟨φ⟩⟩ := h j₂
    exact ⟨j₁, leOfHom φ⟩
  · intro h
    constructor
    · intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩
    · intro _ c _ _
      exact ⟨c, 𝟙 _, rfl⟩

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
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
by
  rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]
  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
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k = limit.π G (j, k)

Tactic:
simp [limitIsoLimitCurryCompLim, Trans.simple]

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'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂

Tactic:
obtain ⟨U, ⟨a, x₁, x₂⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM'))) ⟨r, m₁, m₂⟩
  rw [Prod.ext_iff, Prod.ext_iff] at h
  obtain ⟨rfl, rfl, rfl⟩ := h
  exact ⟨U, a, x₁, x₂, rfl, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤

Tactic:
refine ⟨fun h ↦ ?_, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : F.IsLeftAdjoint
⊢ F.rightAdjointObjIsDefined = ⊤
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'
N : ModuleCat ↑cR.pt
φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ (ModuleCat.Hom.hom (((homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ')).app U)) m =
    (ModuleCat.Hom.hom ((f ≫ (homEquiv hcR hcM') φ').app U)) m

Tactic:
simp only [homEquiv_app_apply, ModuleCat.hom_comp, ModuleCat.hom_ofHom, LinearMap.coe_comp,
    Function.comp_apply, comp_app]

Goal state after:
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'
N : ModuleCat ↑cR.pt
φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ (ModuleCat.Hom.hom φ') ((map hcR hcM hcM' f) ((ConcreteCategory.hom (cM.ι.app U)) m)) =
    (ConcreteCategory.hom φ') ((ConcreteCategory.hom (cM'.ι.app U)) ((ModuleCat.Hom.hom (f.app U)) m))
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
Y✝ Y : C
⊢ singleton (pullback.snd g f) (pullback.snd g f)

Tactic:
exact singleton.mk

Goal state after:
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
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.Compatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) ↔
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) ↔
    (ConcreteCategory.hom (firstMap P S)) x = (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
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible ↔ x.SieveCompatible

Tactic:
by
  constructor
  · intro h Y Z f g hf
    simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)
  · intro h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k
    simp_rw [← h f₁ g₁ h₁, ← h f₂ g₂ h₂]
    congr

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
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ x.Compatible ↔
    ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)

Tactic:
by
  refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩
  rintro ⟨rfl⟩ ⟨rfl⟩ h
  exact H _ _ h

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
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g

Tactic:
rwa [← hf]

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
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
⊢ x.IsAmalgamation t

Tactic:
by
  intro Y u hu
  refine injective_of_mono (f.app _) ?_
  simpa using ht _ hu

Goal state after:
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
| Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
enter [2, a, 1, 1]; rw [← Iso.toEquiv_apply]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
a : Presieve.FamilyOfElements P R
| (firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)
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
⊢ FamilyOfElements.Compatible fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

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
⊢ FamilyOfElements.SieveCompatible fun Y f hf ↦
    (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
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
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX

Tactic:
intro H
    exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩

Goal state after:
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
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ coyoneda.obj E) S.arrows

Tactic:
dsimp [IsSheafFor]; simp_rw [compatible_iff_sieveCompatible]
  rw [((Cone.isLimitEquivIsTerminal _).trans (isTerminalEquivUnique _ _)).nonempty_congr]
  rw [Classical.nonempty_pi]; constructor
  · intro hu E x hx
    specialize hu hx.cone
    rw [(homEquivAmalgamation hx).uniqueCongr.nonempty_congr] at hu
    exact (unique_subtype_iff_existsUnique _).1 hu
  · rintro h ⟨E, π⟩
    let eqv := conesEquivSieveCompatibleFamily P S (op E)
    rw [← eqv.left_inv π]
    erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]
    rw [unique_subtype_iff_existsUnique]
    exact h _ _ (eqv π).2

Goal state after:
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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ ∀ (I_1 : GrothendieckTopology.Cover.Arrow ⟨ofArrows X f, hf⟩), x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op

Tactic:
rintro ⟨Z, _, _, g, _, ⟨i⟩, rfl⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op = y ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op
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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      colimit.ι (J.diagram P (unop X)) (op ((unop S).pullback (𝟙 (unop X)))) =
    colimit.ι (J.diagram P (unop X)) S

Tactic:
rw [← colimit.w _ e.inv.op, ← Category.assoc]

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ (Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop X)).map e.inv.op) ≫
      colimit.ι (J.diagram P (unop X)) (op (unop S)) =
    colimit.ι (J.diagram P (unop X)) S
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
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ m ≫ P.map I.f.op = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op

Tactic:
hm (WalkingMulticospan.left I)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ E.π.app (WalkingMulticospan.left I) = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : x.refine h1 = y.refine h2
i : (unop (op S)).shape.L
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y))

Tactic:
apply_fun fun ee => ee i at e

Goal state after:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.Compatible

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.SieveCompatible
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
⊢ (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X

Tactic:
refine ?_ ≪≫ HasColimit.isoOfNatIso (J.diagramCompIso F P X.unop)

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
⊢ (J.plusObj P ⋙ F).obj X ≅ colimit (J.diagram P (unop X) ⋙ F)
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv) ≫ (J.plusCompIso F (J.plusObj P)).inv =
    J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv

Tactic:
simp only [sheafify, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom

Tactic:
by
  dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]
  simp only [sheafify, Category.id_comp, Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv

Tactic:
by
  dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]
  simp only [sheafify, Category.id_comp, Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toPlus P) F ≫
      (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight (J.toPlus P) F ≫ (J.plusCompIso F P).hom) =
    J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))

Tactic:
whiskerRight_toPlus_comp_plusCompIso_hom,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toPlus P) F ≫ (J.plusCompIso F P).hom ≫ J.plusMap (J.toPlus (P ⋙ F)) =
    J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ (piFan α).π.app j = S.π.app j
x : ↑S.pt
i : ι
⊢ (ConcreteCategory.hom m) x i =
    (ConcreteCategory.hom
        (ofHom { toFun := fun s i ↦ (ConcreteCategory.hom (S.π.app { as := i })) s, continuous_toFun := ⋯ }))
      x i

Tactic:
simp [ContinuousMap.coe_mk, ← h ⟨i⟩]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (Sigma.ι α i ≫ (sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv)) x =
    (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
Iso.hom_inv_id,

Goal state after:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (Sigma.ι α i ≫ 𝟙 (∐ α))) x = (ConcreteCategory.hom (Sigma.ι α i)) x