mathlib-initiative/mathlib-tactics huggingface dataset:
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
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2

Tactic:
simp only [Category.id_comp, Category.assoc]

Goal state after:
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
p p' : J × K
f : p ⟶ p'
⊢ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    s.π.app p.1 ≫ (D.obj p.1).π.app p.2 ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
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 (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
s : Cocone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ (D.obj j).ι.app k ≫
      D.coconePoints.map f ≫ (Q j').desc ((Cocone.precompose (E j').inv).obj (Cocone.whisker (Prod.sectR j' K) s)) =
    (D.obj j).ι.app k ≫
      (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)) ≫ ((const J).obj s.pt).map f

Tactic:
simpa [E] using s.ι.naturality ((Prod.sectL J k).map f)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ ObjectProperty.Small.{u, max u v, max u (v + 1)} (freeYoneda R)

Tactic:
dsimp [freeYoneda]
  infer_instance

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
R✝ : C✝ᵒᵖ ⥤ RingCat
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
S : ShortComplex (PresheafOfModules R) :=
  { X₁ := (kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct, X₂ := M.freeYonedaCoproduct, X₃ := M,
    f := M.toFreeYonedaCoproduct, g := M.fromFreeYonedaCoproduct, zero := ⋯ }
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork

Tactic:
let T := ShortComplex.mk _ _ (kernel.condition M.fromFreeYonedaCoproduct)

Goal state after:
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
R✝ : C✝ᵒᵖ ⥤ RingCat
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
S : ShortComplex (PresheafOfModules R) :=
  { X₁ := (kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct, X₂ := M.freeYonedaCoproduct, X₃ := M,
    f := M.toFreeYonedaCoproduct, g := M.fromFreeYonedaCoproduct, zero := ⋯ }
T : ShortComplex (PresheafOfModules R) :=
  { X₁ := kernel M.fromFreeYonedaCoproduct, X₂ := M.freeYonedaCoproduct, X₃ := M,
    f := kernel.ι M.fromFreeYonedaCoproduct, g := M.fromFreeYonedaCoproduct, zero := ⋯ }
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork
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).inv ≫ limit.π G (j, k) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
← cancel_epi (limitIsoLimitCurryCompLim G).hom

Goal state after:
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 ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) =
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
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' : Subfunctor F✝
S : Set (Subfunctor F✝)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F✝.obj U✝
hx : x ∈ sInf ((fun T ↦ T.obj U✝) '' S)
F : Subfunctor F✝
h : F ∈ S
⊢ (hom (F✝.map f)) x ∈ (fun T ↦ T.obj V✝) F

Tactic:
exact F.map f (hx _ ⟨_, h, rfl⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
S₁ S₂ T : Subfunctor F
⊢ (S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
ι : Sort u_1
S : ι → Subfunctor F
T : Subfunctor F
⊢ (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T

Tactic:
by
  aesop

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
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ x✝

Tactic:
by ext1; apply leftUnitor_naturality

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

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

Tactic:
apply Sieve.pullback_monotone _ Hss

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

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

Tactic:
rintro X Y S hS f _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩
        apply J.pullback_stable _ (f _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
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:
by simpa using mem_coverings_of_isIso (F.map f)

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
X : C
g : X ⟶ S
hg : R g
⊢ ofArrows (fun f ↦ f.obj.left) (fun f ↦ f.obj.hom) g

Tactic:
exact .mk (ι := R.category) ⟨Over.mk g, hg⟩

Goal state after:
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) (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = Exists.choose ⋯

Tactic:
by
        intro s Fs HFs
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        apply H.choose_spec.2 Fs
        exact fun _ f hf => HFs ⟨Over.mk f, hf⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
rintro Z _ ⟨g, rfl, hg⟩
  exact ⟨_, g, f, h, hg, rfl⟩

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

Tactic:
2,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
| ∀ (a : Presieve.FamilyOfElements P S.arrows),
    ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
          ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
      ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
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
⊢ ∀ (a : Presieve.FamilyOfElements P S.arrows),
    a.Compatible →
      ((∃! t, a.IsAmalgamation t) ↔
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a)

Tactic:
intro x

Goal state after:
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
⊢ x.Compatible →
    ((∃! t, x.IsAmalgamation t) ↔
      ∃! x_1, (ConcreteCategory.hom (forkMap P S.arrows)) x_1 = (firstObjEqFamily P S.arrows).toEquiv.symm 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
| 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:
2,

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

Tactic:
intro x

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
x : Presieve.FamilyOfElements P R
⊢ x.Compatible →
    ((∃! t, x.IsAmalgamation t) ↔
      ∃! x_1, (ConcreteCategory.hom (forkMap P R)) x_1 = (firstObjEqFamily P R).toEquiv.symm x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f →
    ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
      (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
        (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩

Tactic:
rintro rfl Y f hf

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (F.map f.op)) (shrinkYonedaEquiv g) =
    (ConcreteCategory.hom (((shrinkFunctor.{w, v₁, u₁} S).ι ≫ g).app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩
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
⊢ ∀ (a : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π a →
      ((∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = a i) ↔
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm
              ((equivShrink ((j : I) → P.obj (op (X j)))) a))

Tactic:
intro x

Goal state after:
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 : (i : I) → P.obj (op (X i))
⊢ Arrows.Compatible P π x →
    ((∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
      ∃! x_1,
        (ConcreteCategory.hom (forkMap P X π)) x_1 =
          (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) 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
⊢ ∀ (a : FamilyOfElements P R),
    (∀ (t₁ t₂ : P.obj (op X)), a.IsAmalgamation t₁ → a.IsAmalgamation t₂ → t₁ = t₂) ∧
        (a.Compatible → ∃ t, a.IsAmalgamation t) ↔
      a.Compatible → ∃! t, a.IsAmalgamation t

Tactic:
intro x

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₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
      (x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    x.Compatible → ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
intro x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
⊢ x.Compatible → ∃! t, x.IsAmalgamation t
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)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ ∀ (x : unop (op X)),
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
            (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)))
        x =
      (ConcreteCategory.hom (z f hf)) x

Tactic:
intro x

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
x : unop (op X)
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
          (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)))
      x =
    (ConcreteCategory.hom (z f hf)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
⊢ ∀ (x : unop (op X)),
    (ConcreteCategory.hom y) x =
      (ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x

Tactic:
intro x

Goal state after:
case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
x : unop (op X)
⊢ (ConcreteCategory.hom y) x =
    (ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) 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
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
⊢ IsSeparatedFor P' R

Tactic:
intro x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
⊢ ∀ (t₁ t₂ : P'.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
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
h : IsSeparatedFor Q R
⊢ IsSeparatedFor P R

Tactic:
intro x

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
h : IsSeparatedFor Q R
x : FamilyOfElements P R
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ IsSeparatedFor P R

Tactic:
intro x

Goal state after:
case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro x

Goal state after:
case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
⊢ x.Compatible → ∃ t, x.IsAmalgamation t
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✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯ ≫
          (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)))
      x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
ConcreteCategory.comp_apply,

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✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom ((J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
⊢ eqToHom ⋯ ≫ π (i (π j) ⋯) = 𝟙 (X j) ≫ π j

Tactic:
by rw [← h', id_comp]

Goal state after:
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✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom
        ((J.diagramPullback P I.f).app (op S) ≫ colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))))
      ((Meq.equiv P S).symm x)

Tactic:
ConcreteCategory.comp_apply,

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✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ⊤)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯)) (↑x I)) =
    (ConcreteCategory.hom
        ((J.diagramPullback P I.f).app (op S) ≫ colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))))
      ((Meq.equiv P S).symm x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t ↦ hx.familyOfElements.IsAmalgamation t) y → y = t
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
rw [ht₁ _ (ofArrows.mk i), hx.familyOfElements_ofArrows_mk]

Goal state after: