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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
⊢ B ≤ Sx

Tactic:
rintro Y f ⟨Z, e1, e2, he2, he1, hee⟩
        rw [← hee]
        apply leOfHom (h1 ⟨_, _, he2⟩)
        exact he1

Goal state after:
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
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
x y : CD (P.obj (op X))
h : (ConcreteCategory.hom ((J.toPlus P).app (op X))) x = (ConcreteCategory.hom ((J.toPlus P).app (op X))) y
⊢ x = y

Tactic:
simp only [toPlus_eq_mk] at h

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
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
x y : CD (P.obj (op X))
h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ x = y
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ (coneOfConeForget (forget.mapCone c)).pt ≅ c.pt

Tactic:
refine TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }

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

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✝³ : ∀ (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
P : Cᵒᵖ ⥤ D
⊢ ∀ {X : Cᵒᵖ ⥤ D} {Y : Sheaf J D} (f : P ⟶ X) (g : X ⟶ (sheafToPresheaf J D).obj Y),
    { toFun := fun e ↦ J.toSheafify P ≫ 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
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_1
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
⊢ (coconeOfCoconeForget (forget.mapCocone c)).pt ≅ c.pt

Tactic:
refine TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }

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

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom (prod.map f g))) (induced (⇑(ConcreteCategory.hom prod.fst)) X.str) ⊓
      induced (⇑(ConcreteCategory.hom (prod.map f g))) (induced (⇑(ConcreteCategory.hom prod.snd)) Z.str)

Tactic:
induced_compose,

Goal state after:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst) ∘ ⇑(ConcreteCategory.hom (prod.map f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom prod.snd) ∘ ⇑(ConcreteCategory.hom (prod.map f g))) Z.str
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 (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
refine .of_comp (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from
        ContinuousMap.continuous_toFun _)
      ?_
  suffices
    IsEmbedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by
    simpa [← coe_comp] using this
  rw [coe_comp]
  exact (isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _)

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

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt ⟶ T✝
h₁ : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl ≫ m = f₁
h₂ : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inr ≫ m = f₂
x : B
⊢ (ConcreteCategory.hom m).toFun (Sum.inr x) =
    (ConcreteCategory.hom
          (↾fun x ↦ Sum.casesOn x (fun x ↦ (ConcreteCategory.hom f₁) x) fun x ↦ (ConcreteCategory.hom f₂) x)).toFun
      (Sum.inr x)

Tactic:
· exact ConcreteCategory.congr_hom h₂ x

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ PullbackCone (Cofan.inj c i) (Cofan.inj c j)

Tactic:
match i, j with
    | .left, .right => exact s
    | .right, .left => exact s.flip

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
⊢ αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
      BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f →
    IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ f
        (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
      IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ f
        (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
hαY

Goal state after:
case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ f
      (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
    IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ f
      (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
⊢ αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f →
    IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
      IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr

Tactic:
hαY

Goal state after:
case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
⊢ IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
    IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
exact ⟨val, rfl, fun y h => Sum.inr_injective h.symm⟩

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

Goal state before:
pp: case h
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'
j : J
⊢ (ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj k'') j ≫ colimit.ι ((curry.obj F).obj j) k''))
      (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
        (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j))
        ⋯) =
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x

Tactic:
generalize_proofs _ _ _ _ h

Goal state after:
case h
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'
j : J
pf✝⁵ : HasColimit ((curry.obj F).obj j)
pf✝⁴ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝³ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝² : HasColimit ((curry.obj F).obj j)
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j') ≫ F.map (𝟙 j' ×ₘ gf (𝟙 j')) ≫ F.map (𝟙 j' ×ₘ i (𝟙 j')))) (y j')
pf✝¹ : HasColimitsOfShape K (Type v)
pf✝ : HasLimit (curry.obj F ⋙ colim)
⊢ (ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj k'') j ≫ colimit.ι ((curry.obj F).obj j) k''))
      (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
        (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j))
        h) =
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: 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 : X ⟶ Z
a : Y ⟶ Z'
h : (fun g ↦ f ≫ g) a = g ≫ e.hom
⊢ (fun g ↦ f ≫ g) (a ≫ e.inv) = g

Tactic:
simp only [reassoc_of% h, e.hom_inv_id, comp_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) (adj.counit.app X)

Tactic:
by
  rintro _ ⟨Y, rfl⟩
  convert!
    ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective using 1
  dsimp [Adjunction.homEquiv]
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ ∀ (a : Cᵒᵖ ⥤ A),
    IsIso (G₂.map (whiskerRight (adj₁.unit.app a) F)) ↔ IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app a)

Tactic:
intro P

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
⊢ IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F)) ↔ IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app P)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ (imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
        (shrinkYonedaObjObjEquiv.symm g)).arrows
    v

Tactic:
refine ⟨(c.inj i).app (op V) (shrinkYonedaObjObjEquiv.symm a),
      (ConcreteCategory.congr_hom (NatTrans.congr_app
      ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
        (shrinkYonedaObjObjEquiv.symm a)).trans ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map (f i)).app (op V))) (shrinkYonedaObjObjEquiv.symm a) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
p : ι × ι'
⊢ (d.inj p ≫ e.hom) ≫ t.snd = (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj p ≫ t.snd

Tactic:
· simp [c', c, he₂]

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

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P₀ : PresheafOfModules R₀
M N : SheafOfModules R
f : (sheafification α).obj P₀ ⟶ M
g : M ⟶ N
⊢ (toPresheaf R₀).map ((sheafificationHomEquiv α) (f ≫ g)) =
    (toPresheaf R₀).map ((sheafificationHomEquiv α) f ≫ (SheafOfModules.forget R ⋙ restrictScalars α).map g)

Tactic:
erw [toPresheaf_map_sheafificationHomEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ
hd : projectiveDimension X = ↑↑d
⊢ HasProjectiveDimensionLE X d

Tactic:
by simpa only [← projectiveDimension_le_iff] using! hd.le

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

Goal state before:
pp: case a.inr
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
· exact ⟨Sum.inr i⟩

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
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P

Tactic:
intro P

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f (Sieve.generate S))

Tactic:
obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]

Goal state after: