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

Goal state before:
pp: case e'_3
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
kf : {j j' : J} → (j ⟶ j') → K := ⋯
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
j j' : J
f : j ⟶ j'
q :
  (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
e_1✝ : (fun X ↦ X) (F.obj (j', kf f)) = (fun X ↦ X) (((curry.obj F).obj j').obj (kf f))
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))

Tactic:
· simp [← comp_apply, -types_comp_apply, ← F.map_comp]

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

Goal state before:
pp: case mpr.refine_5.mpr.none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
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' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (f' ≫ w.cocone.inl) αW αZ (f ≫ h)

Tactic:
exact hf.paste_horiz h₁

Goal state after:
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.Adhesive.Basic

Goal state before:
pp: case mpr.uniq.h₁.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 : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

Tactic:
erw [hc.fac]
          erw [← H.w_assoc]
          rw [e₂]
          rfl

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

Goal state before:
pp: case w
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ (fun X ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))

Tactic:
apply colimit.ι (curry.obj (swap K J ⋙ F) ⋙ Limits.lim) k'' _
      dsimp
      -- This representative is meant to be an element of a limit,
      -- so we need to construct a family of elements in `F.obj (j, k'')` for varying `j`,
      -- then show that are coherent with respect to morphisms in the `j` direction.
      apply Limit.mk
      swap
      · -- We construct the elements as the images of the `y j`.
        exact fun j => F.map (𝟙 j ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j)
      · -- After which it's just a calculation, using `s` and `wf`, to see they are coherent.
        dsimp
        intro j j' f
        simp only [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, comp_id]
        calc
          F.map (f ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j) =
              F.map (f ×ₘ (g j ≫ hf f ≫ i f)) (y j) := by
            rw [s (𝟙 j) f]
          _ =
              F.map (𝟙 j' ×ₘ i f) (F.map (f ×ₘ (g j ≫ hf f)) (y j)) := by
            rw [← comp_apply, ← Functor.map_comp, prod_comp, comp_id, assoc]
          _ =
              F.map (𝟙 j' ×ₘ i f) (F.map (𝟙 j' ×ₘ (g j' ≫ gf f)) (y j')) := by
            rw [← wf f]
          _ = F.map (𝟙 j' ×ₘ (g j' ≫ gf f ≫ i f)) (y j') := by
            rw [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, assoc]
          _ = F.map (𝟙 j' ×ₘ (g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) (y j') := by
            rw [s f (𝟙 j'), ← s (𝟙 j') (𝟙 j')]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective ((fun g ↦ f ≫ g) ∘ ⇑e.homToEquiv)
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : W.isColocal.colimitsOfShape J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : W.isColocal.ColimitOfShape J X
f₁ f₂ : X ⟶ Y
h : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
j : J
⊢ (fun f ↦ f ≫ g) ({ pt := X, ι := p.ι }.ι.app j ≫ f₁) = (fun f ↦ f ≫ g) ({ pt := X, ι := p.ι }.ι.app j ≫ f₂)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝² : W.isColocal.colimitsOfShape J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : W.isColocal.ColimitOfShape J X
f : X ⟶ Z
app : (j : J) → p.diag.obj j ⟶ Y
h : ∀ (j : J), (fun f ↦ f ≫ g) (app j) = p.ι.app j ≫ f
x✝¹ x✝ : J
a : x✝¹ ⟶ x✝
⊢ (fun f ↦ f ≫ g) (p.diag.map a ≫ app x✝) = (fun f ↦ f ≫ g) (app x✝¹ ≫ ((Functor.const J).obj Y).map a)

Tactic:
by simp [h]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)) →
    IsVanKampenColimit c

Tactic:
introv H F' hα h
    let X' := F'.obj ⟨WalkingPair.left⟩
    let Y' := F'.obj ⟨WalkingPair.right⟩
    have : F' = pair X' Y' := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X', Y']
    clear_value X' Y'
    subst this
    change BinaryCofan X' Y' at c'
    rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
        (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]
    constructor
    · rintro H ⟨⟨⟩⟩
      exacts [H.1, H.2]
    · intro H
      exact ⟨H _, H _⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f : X ⟶ Z
a : X' ⟶ Y
h : (fun f ↦ f ≫ g) a = e.inv ≫ f
⊢ (fun f ↦ f ≫ g) (e.hom ≫ a) = f

Tactic:
by simp [h]

Goal state after:
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 : C
Y : D
⊢ Function.Bijective fun f ↦ f ≫ adj.counit.app X

Tactic:
convert!
    ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective using 1

Goal state after:
case e'_3
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 : C
Y : D
e_1✝ : (G.obj Y ⟶ (F ⋙ G).obj X) = (G.obj Y ⟶ G.obj (F.obj X))
e_2✝ : (G.obj Y ⟶ (𝟭 C).obj X) = (G.obj Y ⟶ X)
⊢ (fun f ↦ f ≫ adj.counit.app X) =
    ⇑((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans (adj.homEquiv Y X).symm)
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₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ :
  ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType (F₁.obj X)),
    equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X) →
      equalizerSieve x y ∈ J (unop X)
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)

Tactic:
by simp [h]

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₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ (ConcreteCategory.hom ((φ ≫ ψ).app X)) x = (ConcreteCategory.hom ((φ ≫ ψ).app X)) y

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} E
F : D ⥤ E
inst✝¹³ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁸ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
this :
  (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    { hom := (J.sheafifyCompIso F P).inv }
⊢ (sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) =
    (J.sheafifyCompIso F P).inv

Tactic:
by
    rw [this]
    rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
⊢ imageSieve f₁ x ∈ J X

Tactic:
let S := imageSieve (f₁ ≫ f₂) (f₂.app _ x)
    let T : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (_ : S f), Sieve Y := fun Y f hf =>
      equalizerSieve (f₁.app _ (localPreimage (f₁ ≫ f₂) (f₂.app _ x) f hf)) (F₂.map f.op x)
    refine J.superset_covering ?_ (J.transitive (imageSieve_mem J (f₁ ≫ f₂) (f₂.app _ x))
      (Sieve.bind S.1 T) ?_)
    · rintro Y _ ⟨Z, a, g, hg, ha, rfl⟩
      exact ⟨F₁.map a.op (localPreimage (f₁ ≫ f₂) _ _ hg), by simpa using! ha⟩
    · intro Y f hf
      apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)
      apply equalizerSieve_mem J f₂
      rw [NatTrans.naturality_apply, ← app_localPreimage (f₁ ≫ f₂) _ _ hf,
        NatTrans.comp_app, ConcreteCategory.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
P✝ Q✝ R✝ : SheafOfModules R
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝.val + f'✝.val) ≫ g✝.val = f✝.val ≫ g✝.val + f'✝.val ≫ g✝.val

Tactic:
simp only [Preadditive.add_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
P : Cᵒᵖ ⥤ Type (max u v)
U✝ : C
S : J.Cover U✝
x : Meq P S
Y : C
f : Y ⟶ U✝
hf : (↑S).arrows f
Z : C
g : Z ⟶ Y
hg : (↑(S.pullback f)).arrows g
⊢ ↑((Meq.mk ⊤ (↑x { Y := Y, f := f, hf := hf })).refine (homOfLE ⋯)) { Y := Z, f := g, hf := hg } =
    ↑((x.pullback f).refine (𝟙 (S.pullback f))) { Y := Z, f := g, hf := hg }

Tactic:
simpa using!
      x.2 { fst.hf := hf, snd.hf := S.1.downward_closed hf g, r.g₁ := g, r.g₂ := 𝟙 Z, .. }

Goal state after:
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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (PullbackCone.IsLimit.lift ht (s j.as).fst ((s j.as).snd ≫ a.inj j.as) ⋯) (s j.as).snd t.snd (a.inj j.as)

Tactic:
refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht)

Goal state after:
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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (PullbackCone.IsLimit.lift ht (s j.as).fst ((s j.as).snd ≫ a.inj j.as) ⋯ ≫ t.fst) (s j.as).snd v
    (a.inj j.as ≫ u)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case x.rj
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
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ Presheaf.equalizerSieve r₀ r₀' ∈ J (Opposite.unop (Opposite.op Y))

pp: case x.sj
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
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ Presheaf.equalizerSieve m₀ m₀' ∈ J (Opposite.unop (Opposite.op Y))

Tactic:
· exact Presheaf.equalizerSieve_mem J α _ _ hr₀

Goal state after:
case x.sj
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
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ Presheaf.equalizerSieve m₀ m₀' ∈ J (Opposite.unop (Opposite.op Y))
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext S.X₁ Y i
⊢ x₁ = 0

Tactic:
obtain ⟨x₂, rfl⟩ := Ext.contravariant_sequence_exact₁ hS _ x₁ (add_comm _ _)
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) (by lia))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ (Ext.mk₀ S.f).comp x₂ ⋯ = 0
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: 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
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage

Tactic:
constructor
    · intro H X S hS
      exact H _ <| Saturate.of _ _ hS
    · intro H X S hS
      induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : Coverage C
⊢ J.toGrothendieck = J.toGrothendieck

Tactic:
Coverage.toGrothendieck,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : Coverage C
⊢ J.toGrothendieck = J.toGrothendieck.copy (fun X ↦ Set.ofPred (J.Saturate X)) ⋯
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presieve.IsSheaf J (((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op).obj U)

Tactic:
exact IsContinuous.op_comp_isSheaf_of_types (F := F) ⟨U, hU⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
let adj : H ⊣ (Functor.whiskeringLeft _ _ _).obj F.op := F.op.lanAdjunction _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
U V : Dᵒᵖ
i : U ⟶ V
⊢ ((ℱ ⋙ yoneda).map i ≫
      let α_1 := sheafCoyonedaHom α;
      { app := fun X ↦ (α_1.app X).app V, naturality := ⋯ }) =
    (let α_1 := sheafCoyonedaHom α;
      { app := fun X ↦ (α_1.app X).app U, naturality := ⋯ }) ≫
      (ℱ'.obj ⋙ yoneda).map i

Tactic:
by
    ext X x
    exact ConcreteCategory.congr_hom (((sheafCoyonedaHom α).app X).naturality i) x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
𝒢 : Dᵒᵖ ⥤ A
f : 𝒢 ⟶ ℱ
g : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
⊢ restrictHomEquivHom (G.op.whiskerLeft f ≫ g) = f ≫ restrictHomEquivHom g

Tactic:
apply (restrictHomEquivHom (G := G)).symm.injective
  simpa only [Equiv.symm_apply_apply] using
    (restrictHomEquivHom_naturality_left_symm (G := G) (f := f)
      (g := restrictHomEquivHom g)).symm

Goal state after: