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

Goal state before:
pp: case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ (k : C) → IsLimit (((evaluation C D).obj k).mapCone (PullbackCone.mk (c'.ι.app j) (α.app j) ⋯))

Tactic:
refine fun x => (isLimitMapConePullbackConeEquiv _ _).symm ?_

Goal state after:
case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
x : C
⊢ IsLimit (PullbackCone.mk (((evaluation C D).obj x).map (c'.ι.app j)) (((evaluation C D).obj x).map (α.app j)) ⋯)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
⊢ IsColimit (BinaryCofan.mk (↾fun p ↦ (↑p).1) (↾fun p ↦ (↑p).1))

Tactic:
let eX : { p : Z × PUnit // f p.fst = Sum.inl p.snd } ≃ { x : Z // f x = Sum.inl PUnit.unit } :=
      ⟨fun p => ⟨p.1.1, by convert! p.2⟩, fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl,
        fun _ => by ext; rfl⟩

Goal state after:
case h₂
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ IsColimit (BinaryCofan.mk (↾fun p ↦ (↑p).1) (↾fun p ↦ (↑p).1))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄✝ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' αY (𝟙 Z' ≫ αZ) i

Tactic:
← show cmp ≫ pullback.snd _ _ = αY from pullback.lift_snd _ _ _

Goal state after:
case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄✝ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' (cmp ≫ pullback.snd αZ i) (𝟙 Z' ≫ αZ) i
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
⊢ H.IsVanKampen

Tactic:
obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H
  introv W' hf hg hh hi w
  obtain ⟨hc₂⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
    (BinaryCofan.mk _ (pullback.fst _ _)) _ _ _ hg.w.symm pullback.condition.symm).mpr
    ⟨hg, IsPullback.of_hasPullback αY c.inr⟩
  refine (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_
  refine ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_
  · dsimp; rw [← pullback.condition_assoc, Category.assoc, hi.w]
  constructor
  · rintro ⟨hc₃, hc₄⟩
    refine ⟨hc₄, ?_⟩
    let Y'' := pullback αZ i
    let cmp : Y' ⟶ Y'' := pullback.lift i' αY hi.w
    have e₁ : (g' ≫ cmp) ≫ pullback.snd _ _ = αW ≫ c.inl := by
      rw [Category.assoc, pullback.lift_snd, hg.w]
    have e₂ : (pullback.fst _ _ ≫ cmp : pullback αY c.inr ⟶ _) ≫ pullback.snd _ _ =
        pullback.snd _ _ ≫ c.inr := by
      rw [Category.assoc, pullback.lift_snd, pullback.condition]
    obtain ⟨hc₄⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
      (BinaryCofan.mk _ _) αW _ _ e₁.symm e₂.symm).mpr <| by
        constructor
        · apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄
        · apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst]; exact hc₃
    rw [← Category.id_comp αZ, ← show cmp ≫ pullback.snd _ _ = αY from pullback.lift_snd _ _ _]
    apply IsPullback.paste_vert _ (IsPullback.of_hasPullback αZ i)
    have : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom := by
      apply BinaryCofan.IsColimit.hom_ext hc₂
      exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
        (hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
    rw [this]
    exact IsPullback.of_vert_isIso ⟨by rw [← this, Category.comp_id, pullback.lift_fst]⟩
  · rintro ⟨hc₃, hc₄⟩
    exact ⟨(IsPullback.of_hasPullback αY c.inr).paste_horiz hc₄, hc₃⟩

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)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Cᵒᵖ ⥤ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
i : (unop W).shape.R
⊢ liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
    liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op

Tactic:
ext 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)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Cᵒᵖ ⥤ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
i : (unop W).shape.R
k : K
⊢ (liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op) ≫ (limit.π F k).app (op i.r.Z) =
    (liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op) ≫ (limit.π F k).app (op i.r.Z)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X Y : C
f : X ⟶ Y
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) f ↔ IsIso (F.map f)

Tactic:
have := adj.counit.naturality f
  dsimp at this
  rw [← (isColocal _).precomp_iff _ _ (isColocal_adj_counit_app adj X),
    ← this, (isColocal _).postcomp_iff _ _ (isColocal_adj_counit_app adj Y),
    isColocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]
  exact ⟨fun _ ↦ isIso_of_fully_faithful G (F.map f), fun _ ↦ inferInstance⟩

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

Goal state before:
pp: 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
F₁ F₂ : Sheaf J A
φ : F₁ ⟶ F₂
⊢ J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

Tactic:
W_eq_isLocal_range_sheafToPresheaf_obj,

Goal state after:
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
F₁ F₂ : Sheaf J A
φ : F₁ ⟶ F₂
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) ((sheafToPresheaf J A).map φ) ↔ IsIso φ
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: 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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
⊢ J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G

Tactic:
W_eq_isLocal_range_sheafToPresheaf_obj,

Goal state after:
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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
⊢ (ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) =
    (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G
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
M N : SheafOfModules R
s : M.sections
p : M ⟶ N
⊢ N.unitHomEquiv (M.unitHomEquiv.symm s ≫ p) = N.unitHomEquiv (N.unitHomEquiv.symm (sectionsMap p s))

Tactic:
simp [unitHomEquiv_comp_apply]

Goal state after:
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
⊢ (ConcreteCategory.hom (N.presheaf.map p.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
    (ConcreteCategory.hom (N.presheaf.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)

Tactic:
have hφ' : ∀ (z : M₂.obj X), φ.app _ (M₂.map p.op z) =
            N.map p.op (φ.app _ z) := CategoryTheory.congr_fun (φ.naturality p.op)

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 (N.presheaf.map p.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
    (ConcreteCategory.hom (N.presheaf.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (PullbackCone.IsLimit.lift ht ((s j.as).fst ≫ a.inj j.as) (s j.as).snd ⋯ ≫ t.snd) (s j.as).fst v
    (a.inj j.as ≫ u)

Tactic:
simpa [hu] using (IsPullback.of_isLimit (hs j.1)).flip

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext X Y d
hd✝ : d = n + (k + 1)
p : InjectivePresentation Y
h : { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
⊢ e.comp (Ext.mk₀ { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.f) ⋯ = 0

Tactic:
subst hd; apply Ext.eq_zero_of_injective

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : projectiveDimension X = ↑⊤
⊢ ↑⊤ ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n

Tactic:
| top =>

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₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
ha₂ : (ConcreteCategory.hom (α.app (Opposite.op Y₂))) a₂ = (ConcreteCategory.hom (R.map f₂.op)) r
hb₁ : (ConcreteCategory.hom (φ.app (Opposite.op Y₁))) b₁ = (ConcreteCategory.hom (A.map f₁.op)) m
hb₂ : (ConcreteCategory.hom (φ.app (Opposite.op Y₂))) b₂ = (ConcreteCategory.hom (A.map f₂.op)) m
ha₀ : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₁.op ≫ g₁.op))) r
hb₀ : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₁.op ≫ g₁.op))) m
ha₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₂.op ≫ g₂.op))) r
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₂.op ≫ g₂.op))) m

Tactic:
rw [hb₀, ← op_comp, fac, op_comp]

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

Goal state before:
pp: case coe.top
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
⊢ projectiveDimension M ≤ ↑⊤ ↔ projectiveDimension N ≤ ↑⊤

Tactic:
| top =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
s : Cocone (K ⋙ sigmaConst.obj R)
j : J
⊢ (Sigma.map' ⇑(ConcreteCategory.hom (c.ι.app j)) fun x ↦ 𝟙 R) ≫ Sigma.desc (hc.desc (coconeTypes s)) = s.ι.app j

Tactic:
ext k

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
s : Cocone (K ⋙ sigmaConst.obj R)
j : J
k : K.obj j
⊢ Sigma.ι (fun x ↦ R) k ≫
      (Sigma.map' ⇑(ConcreteCategory.hom (c.ι.app j)) fun x ↦ 𝟙 R) ≫ Sigma.desc (hc.desc (coconeTypes s)) =
    Sigma.ι (fun x ↦ R) k ≫ s.ι.app j
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ (J₁.close (Sieve.pullback f S)).arrows g

Tactic:
change _ ∈ J₁ _

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ J₁ Z
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.left)

pp: case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)

pp: case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

pp: case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
· exact
      { elems := {BiconeHom.left_id}
        complete := fun f => by cases f; simp }

Goal state after:
case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)

case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)

case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1.top
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
K : GrothendieckTopology C
hK : K ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}
i✝ : C
a✝ : Sieve i✝
X✝ : C
⊢ ⊤ ∈ K X✝

Tactic:
| top =>

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

Goal state before:
pp: case mpr.top
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve X
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X✝), Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
| top =>

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

Goal state before:
pp: case mpr.top
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
H : K ≤ J.toCoverage
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ J X✝

Tactic:
| top =>

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

Goal state before:
pp: case a.top
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ J X✝

Tactic:
| top =>

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

Goal state before:
pp: case refine_2
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
x✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ Sieve.generate R ∈ J.toGrothendieck X

Tactic:
exact generate_mem_toGrothendieck hR

Goal state after: