mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: case refine_2
J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesColimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι := { app := fun k ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
⊢ (P j₁).desc s = (G.map (c₁.ι.app j₁)).app c₂.pt

Tactic:
symm

Goal state after:
case refine_2
J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesColimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) := ⋯
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := ⋯
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := ⋯
j₁ : J₁
s : Cocone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) := ⋯
⊢ (G.map (c₁.ι.app j₁)).app c₂.pt = (P j₁).desc s
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: case refine_2
J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesLimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesLimit K₂ (G.obj x)
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
Q₀ : DiagramOfCones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsLimit (Q₀.obj j₁) := fun x ↦ isLimitOfPreserves (G.obj (K₁.obj x)) hc₂
E₀ : Q₀.conePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.conePoints.obj x)) ⋯
j₁ : J₁
s : Cone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    π := { app := fun k ↦ (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app k), naturality := ⋯ } }
⊢ (P j₁).lift s = (G.map (c₁.π.app j₁)).app c₂.pt

Tactic:
symm

Goal state after:
case refine_2
J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesLimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesLimit K₂ (G.obj x)
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
Q₀ : DiagramOfCones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) := ⋯
P : (j₁ : J₁) → IsLimit (Q₀.obj j₁) := ⋯
E₀ : Q₀.conePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := ⋯
j₁ : J₁
s : Cone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) := ⋯
⊢ (G.map (c₁.π.app j₁)).app c₂.pt = (P j₁).lift s
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₂⟩

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'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  (ConcreteCategory.hom
        ((((forget RingCat).mapCocone cR).tensor
                (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
          U))
      (a, x₁, x₂) =
    (r, m₁, m₂)
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂
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
ι : 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

Tactic:
have (i : ι) : Limits.HasPullback (g i) f := Presieve.hasPullback f (Presieve.ofArrows.mk i)

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
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X
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✝¹ x✝ : J.Cover X
h1 : x✝¹ ≤ x✝
h2 : x✝ ≤ x✝¹
Y : C
f : Y ⟶ X
⊢ (↑x✝¹).arrows f → (↑x✝).arrows f

Tactic:
apply h1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
intro m hm

Goal state after:
case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
m : s.pt ⟶ (Fork.ofι f w).pt
hm : m ≫ (Fork.ofι f w).ι = s.ι
⊢ m = ↾fun i ↦ Classical.choose ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h

Tactic:
rintro ⟨W, k, ⟨_⟩⟩
    apply ofArrows.mk

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
i : ι
⊢ pushforward f (ofArrows U g) (g i ≫ f)

Tactic:
use g i, rfl

Goal state after:
case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
i : ι
⊢ ofArrows U g (g i)
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₂
⊢ x₁ = x₂

Tactic:
by
  rw [← extend_restrict t₁, ← extend_restrict t₂]
  congr

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✝
I : Type u_1
Y : I → C
X : C
⊢ ∀ {Y_1 Z : C} {f : Y_1 ⟶ X}, (∃ i, Nonempty (Y_1 ⟶ Y i)) → ∀ (g : Z ⟶ Y_1), ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
rintro Z₁ Z₂ p ⟨i, ⟨f⟩⟩ g

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✝
I : Type u_1
Y : I → C
X Z₁ Z₂ : C
p : Z₁ ⟶ X
i : I
f : Z₁ ⟶ Y i
g : Z₂ ⟶ Z₁
⊢ ∃ i, Nonempty (Z₂ ⟶ Y 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 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:
intro _ _ f h g

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
h : Presieve.functorPushforward F R.arrows f
g : Z✝ ⟶ Y✝
⊢ Presieve.functorPushforward F R.arrows (g ≫ f)
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 S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)

Goal state after:
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
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

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:
· rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩
    simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)

Goal state after:
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
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
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
hx : x.SieveCompatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
specialize hu hx.cone

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
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : x.SieveCompatible
hu : Nonempty (Unique (hx.cone ⟶ P.mapCone S.arrows.cocone.op))
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
refine ⟨fun t ↦ ?_, fun t i j ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((equivShrink ((i : I) → P.obj (op (X i)))).symm
      ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x))
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

case refine_2
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) j)
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
⊢ E.π.app (WalkingMulticospan.left I) = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op

Tactic:
symm

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
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op = E.π.app (WalkingMulticospan.left I)
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 : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ (fun i ↦ g i ≫ inv f) i₁ = g₂ ≫ (fun i ↦ g i ≫ inv f) i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
simp only [← cancel_mono f, assoc, IsIso.inv_hom_id, comp_id] at h
        exact s.property _ _ _ _ _ h

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
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)

Tactic:
rw [isSheaf_iff_multifork]

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
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
a : WalkingMulticospan S.shape
⊢ (limit.cone (S.index P).multicospan).π.app a = (asIso (S.toMultiequalizer P)).symm.hom ≫ (S.multifork P).π.app a

Tactic:
symm

Goal state after:
case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
a : WalkingMulticospan S.shape
⊢ (asIso (S.toMultiequalizer P)).symm.hom ≫ (S.multifork P).π.app a = (limit.cone (S.index P).multicospan).π.app a
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
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J (P ⋙ s)
⊢ IsSheaf J P

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
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
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J P
⊢ IsSheaf J (P ⋙ s)

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
        colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj Y)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) Y ≫ colimit.ι ((curry.obj F).obj Y) k,
                naturality := ⋯ } } =
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj X)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) X ≫ colimit.ι ((curry.obj F).obj X) k,
                naturality := ⋯ } } ≫
        (curry.obj F ⋙ colim).map f

Tactic:
by
            intro j j' f
            dsimp
            ext k
            simp only [Functor.comp_obj, lim_obj, Category.id_comp, colimit.ι_desc,
              colimit.ι_desc_assoc, Category.assoc, ι_colimMap,
              curry_obj_obj_obj, curry_obj_map_app]
            rw [map_id_right_eq_curry_swap_map, limit.w_assoc]

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

Goal state before:
pp: case right
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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
rintro (x : ToType (multiequalizer (S.index _)))

Goal state after:
case right
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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
⊢ ∃ a, (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) a = x
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: 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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ J.sheafifyLift (η ≫ γ) ⋯ = ((plusPlusSheaf J D).map η).hom ≫ J.sheafifyLift γ ⋯

Tactic:
symm

Goal state after:
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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ ((plusPlusSheaf J D).map η).hom ≫ J.sheafifyLift γ ⋯ = J.sheafifyLift (η ≫ γ) ⋯