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✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) (↑x I) =
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) (Cover.Arrow.base i))) ((Meq.equiv P S).symm x)

Tactic:
dsimp% Meq.equiv_symm_eq_apply x i.base

Goal state after:
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) (↑x I) = ↑x (Cover.Arrow.base i)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      F.map (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      (((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop X) ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom) ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop) ≫ colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op

Tactic:
simp only [Functor.map_comp, Category.assoc]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      F.map (colimMap (J.diagramPullback P f.unop)) ≫
        F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
          ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom ≫
            (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop X) ⋙ F))).hom ≫
        (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
          colimMap (J.diagramPullback (P ⋙ F) f.unop) ≫ colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op
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 ↦ ⟨?_⟩⟩
  refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocone.ext ?_ ?_)
  · refine TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }
  · intro; rfl

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

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

Tactic:
rintro S (_ | _)

Goal state after:
case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.left } =
    S.π.app { as := WalkingPair.left }

case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.right } =
    S.π.app { as := WalkingPair.right }
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 : BinaryCofan X Y
⊢ Continuous (Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr))

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inl

pp: case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

pp: case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }

Tactic:
· fun_prop

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inl

case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.some.right
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
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f₁ f₂).inv ≫
          pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ limit.π (cospan g₁ g₂) (some WalkingPair.right)))
      ⟨(x₁, x₂), this⟩ =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.right))) x✝

Tactic:
simp [hx₂]

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'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ True ∨ ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩ = ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩

Tactic:
true_or

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)
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'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ True
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case refine_2
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),
    (∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = s.π.app j) →
      m = liftToPlusObjLimitObj F (unop X) s

Tactic:
intro S m hm
    dsimp [liftToPlusObjLimitObj]
    simp_rw [← Category.assoc, Iso.eq_comp_inv, ← Iso.comp_inv_eq]
    refine limit.hom_ext (fun k => ?_)
    simp only [limit.lift_π, Category.assoc, ← hm]
    congr 1
    refine colimit.hom_ext (fun k => ?_)
    dsimp [plusMap, plusObj]
    erw [colimit.ι_map, colimit.ι_desc_assoc, limit.lift_π]
    conv_lhs => dsimp
    simp only [Category.assoc]
    rw [ι_colimitLimitIso_limit_π_assoc]
    simp only [colimitObjIsoColimitCompEvaluation_ι_app_hom]
    conv_lhs =>
      dsimp [IsLimit.conePointUniqueUpToIso]
    rw [← Category.assoc, ← NatTrans.comp_app, limit.lift_π]
    rfl

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
⊢ Function.Bijective fun f ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _ (hf X hX)]
    convert! hfg X hX
    cat_disch

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
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]
      intro X
      rw [isIso_iff_bijective]
      exact ⟨h₁ X, this X⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} 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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V : C
g : V ⟶ U
⊢ Sieve.pullback g (imageSieve f s) = imageSieve f ((ConcreteCategory.hom (G.map g.op)) s)

Tactic:
ext W g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} 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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V : C
g✝ : V ⟶ U
W : C
g : W ⟶ V
⊢ (Sieve.pullback g✝ (imageSieve f s)).arrows g ↔ (imageSieve f ((ConcreteCategory.hom (G.map g✝.op)) s)).arrows 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₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
let S := imageSieve f₁ x₁ ⊓ imageSieve f₁ 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₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
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
ht : t.Compatible
⊢ (ConcreteCategory.hom (f.hom.app X)) (H.amalgamate t ht) = s

Tactic:
apply (((isSheaf_iff_isSheaf_of_type J G.obj).1 G.property).isSeparated _
        (Presheaf.imageSieve_mem J f.hom s)).ext

Goal state after:
case mp
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 := ⋯
ht : t.Compatible
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ Opposite.unop X⦄,
    (Presheaf.imageSieve f.hom s).arrows f_1 →
      (ConcreteCategory.hom (G.obj.map f_1.op)) ((ConcreteCategory.hom (f.hom.app X)) (H.amalgamate t ht)) =
        (ConcreteCategory.hom (G.obj.map f_1.op)) s
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 : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r m'

Tactic:
let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
  have hS : S ∈ J X.unop := by
    refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
    all_goals apply Presheaf.imageSieve_mem
  apply A.isSeparated _ _ hS
  rintro Y f ⟨⟨⟨r₀, hr₀⟩, ⟨m₀ : M₀.obj _, hm₀ : (φ.app _) _ = _⟩⟩,
    ⟨m₀' : M₀.obj _, hm₀' : (φ.app _) _ = _⟩⟩
  rw [(A.obj.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
    map_smul_eq α φ r m' f.op r₀ hr₀ m₀' hm₀',
    map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀')
      (by rw [_root_.map_add, _root_.map_add, hm₀, hm₀']),
    smul_add, _root_.map_add]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_unop
    exact reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ J₁.close S = ⊤ → S ∈ J₁ X

Tactic:
intro h
    apply J₁.transitive (J₁.top_mem X)
    intro Y f hf
    change J₁.close S f
    rwa [h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
E : PreZeroHypercover X
⊢ (pushforward f E).presieve₀ = Presieve.pushforward f E.presieve₀

Tactic:
by
  simp [presieve₀, Presieve.pushforward_ofArrows, pushforward]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
R : Presieve X
hR : R ∈ J.coverings X
⊢ R ∈ K.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ J.coverings X
⊢ E.presieve₀ ∈ K.coverings X
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ K.coverings S

Tactic:
· exact of_le (by simp) E.mem₀.2

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
R : Presieve X
hR : R ∈ J.coverings X
⊢ Presieve.IsSheafFor P R

Tactic:
obtain ⟨E₀, rfl⟩ := R.exists_eq_preZeroHypercover

Goal state after:
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
⊢ Presieve.IsSheafFor P E₀.presieve₀
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
a : A
⊢ (L.pointwiseLeftKanExtensionUnit (F ⋙ G)).app a ≫
      (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.pointwiseLeftKanExtensionUnit F).app a)

Tactic:
by
  simpa [-pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Goal state after: