mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (pullbackCone f g).fst = s.fst ∧
        l ≫ (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 = l }

Tactic:
intro S
      constructor; swap
      · 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 }
      refine ⟨?_, ?_, ?_⟩
      · delta pullbackCone
        ext a
        dsimp
      · delta pullbackCone
        ext a
        dsimp
      · intro m h₁ h₂
        ext x
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): used to be `ext x`.
        apply Subtype.ext
        apply Prod.ext
        · simpa using! ConcreteCategory.congr_hom h₁ x
        · simpa using! ConcreteCategory.congr_hom h₂ x

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

Goal state before:
pp: X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (range ⇑(ConcreteCategory.hom c.inl))ᶜ

Tactic:
← eq_compl_iff_isCompl.mpr h₃.symm

Goal state after:
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (range ⇑(ConcreteCategory.hom c.inr))
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
⊢ Function.Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl)

Tactic:
intro a₁ a₂ h

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
h :
  (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₁ =
    (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₂
⊢ a₁ = a₂
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ ∀ (j : K),
    IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app j) f
      (c.ι.app j)

Tactic:
intro k
    rw [← Category.comp_id f]
    refine (H (e.inverse.obj k)).paste_vert ?_
    exact IsPullback.of_vert_isIso ⟨by simp⟩

Goal state after:
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 s
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 (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫
      colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫
          limit.π (colimit (F ⋙ J.diagramFunctor D X).flip) k ≫
            (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom

Tactic:
ι_colimitLimitIso_limit_π_assoc

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 s
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 (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫
      (limit.π (F ⋙ J.diagramFunctor D X) k).app j ≫
        (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫
          (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
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 ≫
      colimit.ι (limit (F ⋙ J.diagramFunctor D (unop X))) k ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))).hom ≫
          limit.π (colimit (F ⋙ J.diagramFunctor D (unop X)).flip) k✝ ≫
            (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D (unop X)).flip k✝).hom =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k

Tactic:
ι_colimitLimitIso_limit_π_assoc

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))ᵒᵖ
⊢ ((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 k).app k✝ ≫
          (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D (unop X)).flip k✝).hom =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k
Module: Mathlib.CategoryTheory.ObjectProperty.Local

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

Tactic:
by
    rw [← Function.Bijective.of_comp_iff _ (Iso.homFromEquiv e).bijective]
    convert! (Iso.homFromEquiv e).bijective.comp (hX g hg) using 1
    aesop

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

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Injective fun g ↦ f ≫ g

pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun g ↦ f ≫ g

Tactic:
· intro g₁ g₂ _
    simpa only [← cancel_epi f]

Goal state after:
case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presheaf.IsSheaf J Z
⊢ Function.Bijective fun g ↦ (shrinkFunctor.{w, v_1, u_1} S).ι ≫ g

Tactic:
isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presieve.IsSheaf J Z
⊢ Function.Bijective fun g ↦ (shrinkFunctor.{w, v_1, u_1} S).ι ≫ g
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
⊢ Presheaf.IsSheaf K G

Tactic:
isSheaf_iff_isSheaf_of_type

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
⊢ IsSheaf K G
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ᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (equalizerSieve x y).arrows f ↔ ⊤.arrows f

Tactic:
simp only [equalizerSieve_apply, op_unop, Sieve.top_apply, iff_true]

Goal state after:
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ᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (ConcreteCategory.hom (F₁.map f.op)) x = (ConcreteCategory.hom (F₁.map f.op)) y
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₂
⊢ IsLocallyInjective J φ ↔
    ∀ ⦃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)

Tactic:
by
  constructor
  · intro _ X x y h
    let S := equalizerSieve (φ.app _ x) (φ.app _ y)
    let T : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X.unop⦄ (_ : S f), Sieve Y := fun Y f _ =>
      equalizerSieve (F₁.map f.op x) ((F₁.map f.op y))
    refine J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)
    · rintro Y f ⟨Z, a, g, hg, ha, rfl⟩
      simpa using! ha
    · intro Y f hf
      refine J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf)
        (equalizerSieve_mem J φ _ _ ?_)
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply]
      exact hf
  · intro hφ
    exact ⟨fun {X} x y h => hφ x y (by simp [h])⟩

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₃ : 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)) 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
⊢ (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.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ projectiveDimension X = ⊥ ↔ Limits.IsZero X

Tactic:
← hasProjectiveDimensionLT_zero_iff_isZero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ projectiveDimension X = ⊥ ↔ HasProjectiveDimensionLT X 0
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ᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 0 m = 0

Tactic:
by
  apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
  rintro Y f ⟨m₀, hm₀⟩
  rw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero,
    (A.obj.map f.op).hom.map_zero]

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom J j k
⊢ Decidable (f = g)

Tactic:
classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
⊢ (F.lan ⋙ (evaluation D E).obj X).map φ ≫
      (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
          (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
          (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
      ((Functor.whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map φ

Tactic:
apply (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G₁ X).hom_ext

Goal state after:
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
⊢ ∀ (j : CostructuredArrow F X),
    ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
        (F.lan ⋙ (evaluation D E).obj X).map φ ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
      ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
          ((Functor.whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map φ
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.transitive.refine_2
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)

Goal state after:
case mpr.transitive.refine_2
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
⊢ ∃ t, x.IsAmalgamation t
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 T
ι : Type w'
e : ι ≃ E.I₀
⊢ (E.reindex e).presieve₀ ∈ J.coverings T

Tactic:
simp [E.mem₀]

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
inst✝ : Small.{w', w} E.I₀
⊢ (E.restrictIndex ⇑(equivShrink E.I₀).symm).presieve₀ ∈ J.coverings S

Tactic:
simp [E.mem₀]

Goal state after: