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

Goal state before:
pp: case left
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x y : (forget D).obj ((J.plusObj P).obj (op X))
h :
  (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) x =
    (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) y
⊢ x = y

Tactic:
apply sep P S _ _

Goal state after:
case left
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x y : (forget D).obj ((J.plusObj P).obj (op X))
h :
  (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) x =
    (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) y
⊢ ∀ (I : S.Arrow),
    (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case val
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt

pp: case property
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ?val ≫ (pullbackCone f g).fst = S.fst ∧
    ?val ≫ (pullbackCone f g).snd = S.snd ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ (pullbackCone f g).fst = S.fst → m ≫ (pullbackCone f g).snd = S.snd → m = ?val

Tactic:
· exact ofHom
          { toFun := fun x =>
              ⟨⟨S.fst x, S.snd x⟩, by simpa using! ConcreteCategory.congr_hom S.condition x⟩
            continuous_toFun := by fun_prop }

Goal state after:
case property
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
          { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
            continuous_toFun := ⋯ } ≫
        (pullbackCone f g).fst =
      S.fst ∧
    ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (pullbackCone f g).snd =
        S.snd ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ (pullbackCone f g).fst = S.fst →
          m ≫ (pullbackCone f g).snd = S.snd →
            m =
              ofHom
                { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                  continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (sigmaIsoSigma α).inv)
      ((ConcreteCategory.hom (sigmaIsoSigma α).hom) ((ConcreteCategory.hom (Sigma.ι α i)) x)) =
    (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
← comp_app,

Goal state after:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom ((sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv)) ((ConcreteCategory.hom (Sigma.ι α i)) x) =
    (ConcreteCategory.hom (Sigma.ι α i)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom ((sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv)) ((ConcreteCategory.hom (Sigma.ι α i)) x) =
    (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
← comp_app,

Goal state after:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (Sigma.ι α i ≫ (sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv)) x =
    (ConcreteCategory.hom (Sigma.ι α i)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑X
y : ↑Y
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩

Goal state after:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑X
y : ↑Y
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), eq⟩) = x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩

Goal state after:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), eq⟩) = y
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: 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₁ : IsEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ prod.map i₁ i₂))

Tactic:
coe_comp

Goal state after:
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₁ : IsEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding
    (⇑(ConcreteCategory.hom (prod.map i₁ i₂)) ∘
      ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂))))
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k ↦ X ↑k
ι : Unit → I := fun x ↦ i
hι : Function.Injective ι
⊢ Mono (c.inj i)

Tactic:
exact mono_of_injective X ι hι c (Cofan.mk (X i) (fun _ ↦ 𝟙 _)) h
    (Cofan.IsColimit.mk _ (fun s => s.inj ()))

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'
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)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
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'
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x

Tactic:
clear s' i' H kfO k'O O

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'
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'
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
⊢ ((isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F)).conePointUniqueUpToIso
              (limit.isLimit (F ⋙ J.diagramFunctor D (unop X)))).hom.app
        k ≫
      (limit.π (F ⋙ J.diagramFunctor D (unop X)) k✝).app k ≫
        colimit.ι ((F ⋙ J.diagramFunctor D (unop X)).flip ⋙ (evaluation K D).obj k✝) k =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k

Tactic:
conv_lhs =>
      dsimp [IsLimit.conePointUniqueUpToIso]

Goal state after:
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
⊢ (limit.lift (F ⋙ J.diagramFunctor D (unop X)) ((J.diagramFunctor D (unop X)).mapCone (limit.cone F))).app k ≫
      (limit.π (F ⋙ J.diagramFunctor D (unop X)) k✝).app k ≫
        colimit.ι ((F ⋙ J.diagramFunctor D (unop X)).flip ⋙ (evaluation K D).obj k✝) k =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k
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
X Y : C
f : X ⟶ Y
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ g₁ ≫ e.hom = g₂ ≫ e.hom

Tactic:
apply (hf _ hZ').1

Goal state after:
case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.isLocal f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ (fun g ↦ f ≫ g) (g₁ ≫ e.hom) = (fun g ↦ f ≫ g) (g₂ ≫ e.hom)
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
⊢ J.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
by
  apply congr_arg
  ext P
  constructor
  · intro hP
    exact ⟨⟨P, hP⟩, rfl⟩
  · rintro ⟨F, rfl⟩
    exact F.property

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

Goal state before:
pp: case mpr
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)
⊢ IsLocallyInjective J φ

Tactic:
exact ⟨fun {X} x y h => hφ x y (by simp [h])⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
⊢ t.Compatible

Tactic:
intro Y₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Opposite.unop X⦄ ⦃f₂ : Y₂ ⟶ Opposite.unop X⦄
    (h₁ : (Presheaf.imageSieve f.hom s).arrows f₁) (h₂ : (Presheaf.imageSieve f.hom s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ h₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ h₂)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
  convert! isPullback_of_cofan_isVanKampen hc i.as j.as
  exact (if_neg (mt Discrete.ext hi.symm)).symm

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
⊢ ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).Compatible

Tactic:
intro Y₁

Goal state after:
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₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : P f₁) (h₂ : P f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
        (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: 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)
m : ↑M
r : Shrink.{v, u} R
⊢ ((Hom.hom S'.g ∘ₛₗ ↑e2) ∘ₛₗ Finsupp.lsingle m) r = ((↑e' ∘ₛₗ Hom.hom S.g) ∘ₛₗ Finsupp.lsingle m) r

Tactic:
simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
⊢ (ConcreteCategory.hom (A.obj.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.obj.map π)) r) ((ConcreteCategory.hom (A.obj.map π)) m)

Tactic:
by
  let S := Presheaf.imageSieve α (R.obj.map π r) ⊓ Presheaf.imageSieve φ (A.obj.map π m)
  have hS : S ∈ J Y.unop := by
    apply J.intersection_covering
    all_goals apply Presheaf.imageSieve_mem
  apply A.isSeparated _ _ hS
  rintro Y f ⟨⟨r₀,
    (hr₀ : (α.app (Opposite.op Y)).hom r₀ = (R.obj.map f.op).hom ((R.obj.map π).hom r))⟩,
    ⟨m₀, (hm₀ : (φ.app _) _ = _)⟩⟩
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp,
    map_smul_eq α φ r m (π ≫ f.op) r₀ (by rw [hr₀, Functor.map_comp, RingCat.comp_apply]) m₀
      (by rw [hm₀, Functor.map_comp, ConcreteCategory.comp_apply]),
    map_smul_eq α φ (R.obj.map π r) (A.obj.map π m) f.op r₀ hr₀ m₀ hm₀]

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
⊢ y.Compatible

Tactic:
intro Y₁

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
Y₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : S f₁) (h₂ : S f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (y f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y f₂ h₂)
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
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ (E.map F).sieve₀ = Sieve.functorPushforward F E.sieve₀

Tactic:
PreZeroHypercover.sieve₀,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ Sieve.ofArrows (E.map F).X (E.map F).f = Sieve.functorPushforward F E.sieve₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt).hom ≫
      (E.forkOfIsColimit hc hd F).ι =
    Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
      (Iso.refl c'.pt).hom

Tactic:
refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
    simp
    simp [c']

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
⊢ (trivial S).sieve₀ = ⊤

Tactic:
PreZeroHypercover.sieve₀,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
⊢ Sieve.ofArrows (trivial S).X (trivial S).f = ⊤