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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ ∀ {X' X : Cᵒᵖ ⥤ D} {Y : Sheaf J D} (f : X' ⟶ X) (g : X ⟶ (sheafToPresheaf J D).obj Y),
    { toFun := fun e ↦ J.toSheafify X' ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (f ≫ g) =
      (plusPlusSheaf J D).map f ≫
        { toFun := fun e ↦ J.toSheafify X ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g

Tactic:
intro P Q R η γ; ext1; dsimp; symm
        apply J.sheafifyMap_sheafifyLift

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
⊢ Nonempty (IsColimit c) ↔ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
refine ⟨fun ⟨hc⟩ ↦ coinduced_of_isColimit _ hc, fun h ↦ ⟨?_⟩⟩

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ IsColimit c
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).1 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).1

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).2 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).2

Tactic:
· specialize h ⟨WalkingPair.left⟩
      apply_fun fun e => e x at h
      exact h

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).2 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).2
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding
      ⇑(ConcreteCategory.hom
          ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
            (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) ∧
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl
        (range
          ⇑(ConcreteCategory.hom
              ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)))
        (range ⇑(ConcreteCategory.hom c.inr))

Tactic:
← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.right⟩

Goal state after:
case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding
      ⇑(ConcreteCategory.hom
          ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
            (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) ∧
    IsOpenEmbedding
        ⇑(ConcreteCategory.hom
            ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
              (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) ∧
      IsCompl
        (range
          ⇑(ConcreteCategory.hom
              ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)))
        (range
          ⇑(ConcreteCategory.hom
              ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
| (range
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
        ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }))))ᶜ

Tactic:
rw [Set.range_comp]

Goal state after:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
| (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ''
      range ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right })))ᶜ
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case ht.a
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))

Tactic:
· exact H₂.isOpen_range

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

Goal state before:
pp: 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'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((curry.obj F ⋙ colim).map f)) ((ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x) =
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') (k j)))
      ((ConcreteCategory.hom (F.map (f ×ₘ 𝟙 (k j)))) (y j))

Tactic:
← e

Goal state after:
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'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((curry.obj F ⋙ colim).map f))
      ((ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j)) =
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') (k j)))
      ((ConcreteCategory.hom (F.map (f ×ₘ 𝟙 (k j)))) (y j))
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
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))
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
refine (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_

Goal state after:
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))
⊢ Nonempty (IsColimit (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e_a
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✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j✝ : J
α' : F' ⟶ F
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j✝ = β.inv.app j✝ ≫ Gl.map (Gr.map (α'.app j✝))
e_1✝ :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶ (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }).pt)
j : J
⊢ c'.ι.app j ≫ f = α.app j ≫ Gl.map (c.ι.app j)

Tactic:
exact (NatTrans.congr_app h j).symm

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

Goal state before:
pp: case mpr.left
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₁ f₂ : X ⟶ Y
eq : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
⊢ (fun f ↦ f ≫ g) (e.inv ≫ f₁) = (fun f ↦ f ≫ g) (e.inv ≫ f₂)

Tactic:
simp [eq]

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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ J.W f ↔ IsIso (G.map f)

Tactic:
by
  rw [W_eq_isLocal_range_sheafToPresheaf_obj]
  exact ObjectProperty.isLocal_iff_isIso_map adj f

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
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Function.Bijective fun g ↦ (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι ≫ g

Tactic:
← Functor.whiskeringLeft_obj_obj,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Function.Bijective fun g ↦ (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι ≫ g
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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallySurjective J f₃ ↔ IsLocallySurjective J f₂

Tactic:
constructor
  · intro
    exact isLocallySurjective_of_isLocallySurjective_fac J fac
  · intro
    rw [← fac]
    infer_instance

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
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 (R.map p.op)) r • (ModuleCat.Hom.hom (ψ.app (Opposite.op Y))) x =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)

Tactic:
← hφ,

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 (R.map p.op)) r •
      (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (f.app (Opposite.op Y))) x) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)
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₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    (Presheaf.imageSieve φ.hom x).arrows f →
      (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)).toFun x) =
        (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)).toFun x)

Tactic:
rintro Y f ⟨s : F₁.obj.obj (op Y), hs : φ.hom.app _ s = F₂.obj.map f.op x⟩

Goal state after:
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₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
⊢ (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)).toFun x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)).toFun x)
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₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
h₁ :
  (ConcreteCategory.hom (F₂.obj.map f.op ≫ f₁.hom.app (op Y))) x =
    (ConcreteCategory.hom (f₁.hom.app (op (unop X)) ≫ Z.obj.map f.op)) x
⊢ (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)

Tactic:
have h₂ := ConcreteCategory.congr_hom (f₂.hom.naturality f.op) x

Goal state after:
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₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
h₁ :
  (ConcreteCategory.hom (F₂.obj.map f.op ≫ f₁.hom.app (op Y))) x =
    (ConcreteCategory.hom (f₁.hom.app (op (unop X)) ≫ Z.obj.map f.op)) x
h₂ :
  (ConcreteCategory.hom (F₂.obj.map f.op ≫ f₂.hom.app (op Y))) x =
    (ConcreteCategory.hom (f₂.hom.app (op (unop X)) ≫ Z.obj.map f.op)) x
⊢ (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case succ
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'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
this : (Hom.hom S.g).ker = Submodule.comap (↑e2) (Hom.hom S'.g).ker
⊢ HasProjectiveDimensionLE N (n + 1)

Tactic:
Submodule.comap_equiv_eq_map_symm

Goal state after:
case succ
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'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
this : (Hom.hom S.g).ker = Submodule.map (↑e2.symm) (Hom.hom S'.g).ker
⊢ HasProjectiveDimensionLE N (n + 1)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed ⊤
⊢ ⟨J.close S, ⋯⟩ = ⟨⊤, this⟩

Tactic:
refine H.isSeparatedFor.ext fun Y f hf ↦ ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom ((Functor.closedSieves J).toFunctor.map f.op)) ⟨J.close S, ⋯⟩ =
    (ConcreteCategory.hom ((Functor.closedSieves J).toFunctor.map f.op)) ⟨⊤, this⟩
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
⊢ sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X} ≤ J.toGrothendieck

Tactic:
exact sInf_le (fun _ _ hS => .of _ _ hS)

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
E : J.ZeroHypercover S
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows
    have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) :
        ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j := by
      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
      use j, rfl
      simp
    choose j h₁ h₂ using this
    refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
    convert! E.mem₀
    exact le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))

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
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f

Tactic:
simp [eq]

Goal state after: