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

Goal state before:
pp: case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ ∀ (j : K),
    IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app j) f
      (c.ι.app j)

Tactic:
intro k

Goal state after:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_2.mp
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) →
    ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)

pp: case e'_2.mpr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ (∀ (j : K),
      IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)) →
    ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))

Tactic:
· intro H k
      rw [← Category.comp_id f]
      refine (H (e.inverse.obj k)).paste_vert ?_
      have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance
      exact IsPullback.of_vert_isIso ⟨by simp⟩

Goal state after:
case e'_2.mpr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ (∀ (j : K),
      IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)) →
    ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1.h₂
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
⊢ c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
rw [← Category.assoc]; exact h.fac _ ⟨WalkingPair.left⟩

Goal state after:
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✝⁴ : (forget D).ReflectsIsomorphisms
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝² : SmallCategory K
inst✝¹ : FinCategory K
inst✝ : HasLimitsOfShape K D
⊢ HasSheafify J (Type (max u v))

Tactic:
by
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → P.isColocal f

Tactic:
· apply isColocal_of_isIso

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
· exact (IsColimit.precomposeHomEquiv _ _).symm H.isColimit

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : (ConcreteCategory.hom ((J.toPlus P).app X)) x = (ConcreteCategory.hom ((J.toPlus P).app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
rw [toPlus_eq_mk, toPlus_eq_mk, eq_mk_iff_exists] at h
    obtain ⟨W, h₁, h₂, eq⟩ := h
    exact J.superset_covering (fun Y f hf => congr_fun (congr_arg Subtype.val eq) ⟨Y, f, hf⟩) W.2

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

Goal state before:
pp: case refine_4.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ : IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i))
⊢ Nonempty (IsColimit c)

Tactic:
clear_value F'

Goal state after:
case refine_4.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ : IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i))
⊢ Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
⊢ IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ }))

Tactic:
clear_value F'

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C
this : F = Discrete.functor F'
⊢ IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ }))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) (r • y)) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)

Tactic:
M₂.map_smul,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y)))
      ((ConcreteCategory.hom (R.map p.op)) r • (ConcreteCategory.hom (M₂.map p.op)) y) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) (r' • m)) =
    (ConcreteCategory.hom (M₂.map p.op)) (r' • (ConcreteCategory.hom (g.app X)) m)

Tactic:
M₂.map_smul,

Goal state after:
C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) (r' • m)) =
    (ConcreteCategory.hom (R'.map p.op)) r' • (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) m)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
i : ι
⊢ c.inj i ≫ (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S =
    c.inj i ≫ Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)

Tactic:
by
      rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]
      simp [Cofan.inj, e]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
⊢ Nonempty (IsColimit d)

Tactic:
let c' : Cofan (fun i : ι ↦ (c i).pt) :=
    Cofan.mk t.pt fun i ↦
      PullbackCone.IsLimit.lift ht (pullback.fst _ _ ≫ a.inj i) (pullback.snd _ _)
      (by simp [hu, pullback.condition])

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
⊢ Nonempty (IsColimit d)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P₀.presheaf
          ((SheafOfModules.toSheaf R).obj N)).symm
      ((toPresheaf R₀).map (f ≫ g)) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv Q₀.presheaf
            ((SheafOfModules.toSheaf R).obj N)).symm
        ((toPresheaf R₀).map g)

Tactic:
Functor.map_comp

Goal state after:
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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P₀.presheaf
          ((SheafOfModules.toSheaf R).obj N)).symm
      ((toPresheaf R₀).map f ≫ (toPresheaf R₀).map g) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv Q₀.presheaf
            ((SheafOfModules.toSheaf R).obj N)).symm
        ((toPresheaf R₀).map g)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case refine_2
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 φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (A.obj.map (f ≫ g.op))) m =
    (ConcreteCategory.hom (A.obj.map g.op)) ((ConcreteCategory.hom (A.obj.map f)) m)

Tactic:
Functor.map_comp

Goal state after:
case refine_2
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 φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (A.obj.map f ≫ A.obj.map g.op)) m =
    (ConcreteCategory.hom (A.obj.map g.op)) ((ConcreteCategory.hom (A.obj.map f)) m)
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 J : Type u
⊢ coprod.inl ≫ (freeSumIso I J).hom = freeMap Sum.inl

Tactic:
by
  rw [← dsimp% freeFunctor_map (↾(Sum.inl : I → I ⊕ J))]
  exact IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)

Goal state after: