mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton (pullback.snd g f)

Tactic:
apply pullback_singleton

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
⊢ pullback f (ofObjects X Y) = ofObjects X Z

Tactic:
by
  ext
  simp [Sieve.ofObjects]

Goal state after:
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
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
⊢ t₁ = t₂

Tactic:
specialize hs 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
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
hs : Subsingleton (hx.cone ⟶ P.mapCone S.arrows.cocone.op)
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ ((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app a✝ =
      (S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝ ↔
    (S.functorInclusion ≫ b).app a✝ = a.app a✝

Tactic:
rw [ConcreteCategory.hom_ext_iff, ConcreteCategory.hom_ext_iff]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a✝),
      (ConcreteCategory.hom
            (((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫
                  (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
              a✝))
          x =
        (ConcreteCategory.hom ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝)) x) ↔
    ∀ (x : S.functor.obj a✝),
      (ConcreteCategory.hom ((S.functorInclusion ≫ b).app a✝)) x = (ConcreteCategory.hom (a.app a✝)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
Y : A
⊢ Unique (Y ⟶ F.obj.obj (op X))

Tactic:
choose t h using F.2 Y _ H (by tauto) (by tauto)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
Y : A
t : (F.obj ⋙ coyoneda.obj (op Y)).obj (op X)
h :
  (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : (F.obj ⋙ coyoneda.obj (op Y)).obj (op X)),
      (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a ↦ ⋯.elim) t) y → y = t
⊢ Unique (Y ⟶ F.obj.obj (op X))
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
⊢ m = hP.amalgamate S (fun x ↦ E.ι x) ⋯

Tactic:
apply hP.hom_ext S

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), m ≫ P.map I.f.op = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let T : J.Cover X := ⟨S, hS⟩

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
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case mpr
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
⊢ ∃ k f g,
    (ConcreteCategory.hom ((J.diagram P X).map f)) ((Meq.equiv P S✝).symm x) =
      (ConcreteCategory.hom ((J.diagram P X).map g)) ((Meq.equiv P T).symm y)

Tactic:
use op S, h1.op, h2.op

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
e : x.refine h1 = y.refine h2
⊢ (ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x) =
    (ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2
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
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    ↑(x.refine h1) i

Tactic:
dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases i; rfl

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

Goal state before:
pp: case e'_3
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
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y)) =
    ↑(y.refine h2) i

Tactic:
dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases i; rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom f.inv) ((ConcreteCategory.hom f.hom) x) = x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
y : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) y) = y

Tactic:
by
  simp

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

Goal state before:
pp: case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr
⊢ m = ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }

Tactic:
ext (x | x)

Goal state after:
case refine_4.inl
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr
x : ↑X
⊢ (ConcreteCategory.hom m) (Sum.inl x) =
    (ConcreteCategory.hom
        (ofHom
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      (Sum.inl x)

case refine_4.inr
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr
x : ↑Y
⊢ (ConcreteCategory.hom m) (Sum.inr x) =
    (ConcreteCategory.hom
        (ofHom
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      (Sum.inr x)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
⊢ ∀ (x : IsColimit c₂), Mono c₁.inl → Mono c₂.inl

Tactic:
hc₂

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono c₁.inl → Mono c₂.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
⊢ Nonempty (IsInitial t.pt)

Tactic:
have heq (i) : d.inj i ≫ e.hom.hom = c.inj i := e.hom.w ⟨i⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
⊢ Nonempty (IsInitial t.pt)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr

Tactic:
apply BinaryCofan.IsColimit.hom_ext hc
      · rw [← H.w_assoc]; erw [h.fac _ ⟨WalkingPair.right⟩]; exact s.condition
      · rw [← Category.assoc]; exact h.fac _ ⟨WalkingPair.left⟩

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

Goal state before:
pp: case mpr.fac_right
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y),
    iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr

pp: case mpr.uniq
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl →
      iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
· intro s; exact H.isColimit.fac _ WalkingSpan.left

Goal state after:
case mpr.uniq
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl →
      iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ 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
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ (limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫
        (HasLimit.isoOfNatIso
              (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                  ⋯).symm).hom ≫
          (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
            (HasColimit.isoOfNatIso
                ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                  (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    S.π.app k

Tactic:
← (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).fac S k,

Goal state after:
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ 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
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ (limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫
        (HasLimit.isoOfNatIso
              (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                  ⋯).symm).hom ≫
          (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
            (HasColimit.isoOfNatIso
                ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                  (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).lift S ≫
      (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ P ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
exact ⟨⟨P, hP⟩, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M 0
this : CategoryTheory.Projective M
⊢ CategoryTheory.Projective N

Tactic:
← IsProjective.iff_projective

Goal state after:
case zero
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M 0
this : Module.Projective R ↑M
⊢ Module.Projective R' ↑N
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
M : SheafOfModules R
f : free I ⟶ M
i : I
⊢ M.unitHomEquiv.symm (M.freeHomEquiv f i) = ιFree i ≫ f

Tactic:
simp [freeHomEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
⊢ IsLocallyInjective J (toSheafify α φ)

Tactic:
by
  dsimp [IsLocallyInjective]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S T : C
f : S ⟶ T
⊢ (singleton f).presieve₀ = Presieve.singleton f

Tactic:
simp [singleton, presieve₀, Presieve.ofArrows_pUnit]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F✝ : C ⥤ D
K : Precoverage D
F : C ⥤ D
E : J.ZeroHypercover S
h : J ≤ comap F K
⊢ (PreZeroHypercover.map F E.toPreZeroHypercover).presieve₀ ∈ K.coverings (F.obj S)

Tactic:
by
    rw [PreZeroHypercover.presieve₀_map, ← mem_comap_iff]
    exact h _ E.mem₀

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P

Tactic:
· intro hP
    rw [Presheaf.isSheaf_iff_multifork]
    rintro X ⟨S, hS⟩
    obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS
    exact ⟨IsSheafIff.isLimit hP hE le⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
left_eq✝¹ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).left ≫ (c'.π.app one).left =
    (c'.π.app left).left ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).left
e₁ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).right ≫ (c'.π.app one).right =
    (c'.π.app left).right ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).right
left_eq✝ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).left ≫ (c'.π.app one).left =
    (c'.π.app right).left ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).left
e₂ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).right ≫ (c'.π.app one).right =
    (c'.π.app right).right ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).right
⊢ (ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app left))).op))
      ((ConcreteCategory.hom (eqToHom ⋯)) (x g₁ hg₁)) =
    (ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app right))).op))
      ((ConcreteCategory.hom (eqToHom ⋯)) (x g₂ hg₂))

Tactic:
exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)

Goal state after: