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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : K
⊢ ∀ ⦃Y : K⦄ (f : i ⟶ Y),
    ((Functor.const K).obj S.pt).map f ≫
        (Presheaf.isLimitOfIsSheaf J (F.obj Y).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj Y).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app Y).app (op i.Y)) ⋯) =
      (Presheaf.isLimitOfIsSheaf J (F.obj i).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj i).obj) S.pt (fun i_1 ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
j

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
⊢ ∀ (f : i ⟶ j),
    ((Functor.const K).obj S.pt).map f ≫
        (Presheaf.isLimitOfIsSheaf J (F.obj j).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj j).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app j).app (op i.Y)) ⋯) =
      (Presheaf.isLimitOfIsSheaf J (F.obj i).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj i).obj) S.pt (fun i_1 ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩)) =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π]

Goal state after:
case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.left }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right }))
      ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩)) =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π]

Goal state after:
case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.right }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: 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

Tactic:
pullbackIsoProdSubtype_inv_fst_apply

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
⊢ (↑⟨(x, y), eq⟩).1 = x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))

Tactic:
rintro ⟨h⟩
      rw [← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.left⟩,
        ← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.right⟩]
      dsimp
      refine ⟨(homeoOfIso <| h.coconePointUniqueUpToIso
        (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inl,
          (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inr, ?_⟩
      rw [Set.range_comp, ← eq_compl_iff_isCompl]
      conv_rhs => rw [Set.range_comp]
      erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
by
  convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _)
        (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(y, x), eq⟩) = y

Tactic:
pullbackIsoProdSubtype_inv_fst_apply

Goal state after:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (↑⟨(y, x), eq⟩).1 = y
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) = x

Tactic:
pullbackIsoProdSubtype_inv_fst_apply

Goal state after:
case mpr.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (↑⟨(x, y), ⋯⟩).1 = x
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
⊢ t.fst ≫ c.inj i = t.snd ≫ c.inj j

Tactic:
simp [← heq, t.condition_assoc]

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

Goal state before:
pp: case e'_2.mpr
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 : IsVanKampenColimit 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 : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
⊢ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))

Tactic:
j

Goal state after:
case e'_2.mpr
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 : IsVanKampenColimit 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 : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : HasBinaryCoproducts C
F : C ⥤ D
inst✝ : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ X ⨿ Y
⊢ cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl ≅ cospan f coprod.inr

Tactic:
apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
⊢ αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
hY

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
⊢ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)

Tactic:
j

Goal state after:
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
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
F₁ F₂ : Sheaf J A
φ : F₁ ⟶ F₂
⊢ J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]

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

Goal state before:
pp: case h_map
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y), F.map f ≍ (Discrete.functor F').map f

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
      simp [F']

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₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
X : C
⊢ ∀ (s : ToType ((Subfunctor.sheafify J (Subfunctor.range f)).toFunctor.obj (op X))),
    imageSieve (Subfunctor.toRangeSheafify J f) s ∈ J X

Tactic:
by
    rintro ⟨s, hs⟩
    refine J.superset_covering ?_ hs
    rintro Y g ⟨t, ht⟩
    exact ⟨t, Subtype.ext ht⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) (r' • m)) =
    (ConcreteCategory.hom (α.app (Opposite.op Y))) r •
      (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) m)

Tactic:
← (g.app _).hom.map_smul

Goal state after:
C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
hg :
  ∀ (z : ↑(M₁.obj X)),
    (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) z) =
      (ConcreteCategory.hom (M₂.map p.op)) ((ConcreteCategory.hom (g.app X)) z)
⊢ (ConcreteCategory.hom (g.app (Opposite.op Y))) ((ConcreteCategory.hom (M₁.map p.op)) (r' • m)) =
    (ModuleCat.Hom.hom (g.app (Opposite.op Y))) (r • (ConcreteCategory.hom (M₁.map p.op)) m)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
⊢ ∀ (j : ι),
    (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
      t.inj j

Tactic:
j

Goal state after:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
j : ι
⊢ (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
    t.inj j
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.fst v u ≫ (Iso.refl B).hom = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₁

Tactic:
refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_fst _ _ _

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun x ↦ q₁ x ≫ a.inj x

Tactic:
refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_fst _ _ _

Goal state after:
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
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₁ p.1 p.2 ≫ a.inj p.1

Tactic:
refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_fst _ _ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)

Tactic:
have := hX.subsingleton' i hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this✝ : HasExt C := HasExt.standard C
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT Y i
i : ℕ
hi : n < ↑i
this : HasProjectiveDimensionLT Y i
⊢ HasProjectiveDimensionLT X i

Tactic:
exact h.hasProjectiveDimensionLT i

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

Goal state before:
pp: case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)

pp: case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

pp: case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

pp: case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
· exact
      { elems := {BiconeHom.right_id}
        complete := fun f => by cases f; simp }

Goal state after:
case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)

case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)

case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)

case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀

Tactic:
rw [presieve₀, presieve₀, presieve₀]
  apply le_antisymm
  · intro Z g ⟨i⟩
    cases i
    · exact Or.inl (.mk _)
    · exact Or.inr (.mk _)
  · rintro Z g (⟨⟨i⟩⟩ | ⟨⟨i⟩⟩)
    · exact ⟨Sum.inl i⟩
    · exact ⟨Sum.inr i⟩

Goal state after: