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

Goal state before:
pp: case neg.hg
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
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous ⇑(ConcreteCategory.hom g)

Tactic:
exact g.hom.continuous_toFun

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)

Tactic:
refine .of_iso_pullback (by simp) ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ Y ≅ pullback (c.inj i) (c.inj j)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ Iso.hom ?refine_1 ≫ pullback.fst (c.inj i) (c.inj j) = hY.to (X i)

case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ Iso.hom ?refine_1 ≫ pullback.snd (c.inj i) (c.inj j) = hY.to (X j)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case h.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)

Tactic:
exact IsPullback.paste_horiz (IsPullback.of_hasPullback αX f) hh

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case h.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)

Tactic:
exact IsPullback.paste_horiz (IsPullback.of_hasPullback αX f) hh

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

Goal state before:
pp: case mpr
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✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')

Tactic:
exact fun H => ⟨evaluationJointlyReflectsColimits _ fun x =>
      ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩

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₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'

Tactic:
j₃

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₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
    iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
· intro m e₁ e₂
      apply BinaryCofan.IsColimit.hom_ext h
      · dsimp
        rw [Category.assoc, e₂, eq_comm]; exact h.fac _ ⟨WalkingPair.left⟩
      · refine e₁.trans (Eq.symm ?_); exact h.fac _ _

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)
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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f ≫ i f))) (y j) =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ i f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j))

Tactic:
← comp_apply,

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f ≫ i f))) (y j) =
    (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f) ≫ F.map (𝟙 j' ×ₘ i f))) (y j)
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)
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' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ i f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j')) =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f ≫ i f))) (y j')

Tactic:
← comp_apply,

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f) ≫ F.map (𝟙 j' ×ₘ i f))) (y j') =
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f ≫ i f))) (y 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
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsIso
    (Sigma.desc fun p ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯)

Tactic:
let c : Cofan _ := Cofan.mk _ <| fun (p : ι × ι') ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι _ p.1)
        (Sigma.ι _ p.2) (𝟙 S) (by simp) (by simp)
  apply c.nonempty_isColimit_iff_isIso_sigmaDesc.mp
  refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)
  · exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)
  · exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)
  · exact pullback.isLimit (Sigma.desc f) (Sigma.desc g)

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)

Tactic:
refine (IsPushout.isVanKampen_iff (H.map ((evaluation _ _).obj x))).mp ?_

Goal state after:
J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ ⋯.IsVanKampen
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: case mpr
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
P : Cᵒᵖ ⥤ A
⊢ P ∈ Set.range (sheafToPresheaf J A).obj → Presheaf.IsSheaf J P

Tactic:
rintro ⟨F, rfl⟩
    exact F.property

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

Goal state before:
pp: case mp
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₂
hsep : Presieve.IsSeparated J (F₁ ⋙ forget D)
⊢ IsLocallyInjective J φ → ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))

Tactic:
intro _ X x y h
    exact (hsep _ (equalizerSieve_mem J φ x y h)).ext (fun _ _ hf => hf)

Goal state after:
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₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
CD : D → Type (max u v)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
P : Cᵒᵖ ⥤ D
inst✝² : HasWeakSheafify J D
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : J.PreservesSheafification (forget D)
⊢ IsLocallyInjective J (toSheafify J P)

Tactic:
by
  rw [← isLocallyInjective_forget_iff, ← sheafComposeIso_hom_fac,
    ← toSheafify_plusPlusIsoSheafify_hom]
  infer_instance

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
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext X Y (n + k)
⊢ e = 0

Tactic:
exact this e k rfl

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

Goal state before:
pp: case bot
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : projectiveDimension X = ⊥
⊢ ⊥ ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n

Tactic:
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
    exact ⟨0, by simp [← projectiveDimension_le_iff, hd]⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝⁶ : Presheaf.IsLocallyInjective J α
inst✝⁵ : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝⁴ : Presheaf.IsLocallyInjective J φ
inst✝³ : Presheaf.IsLocallySurjective J φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')
⊢ (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map τ₀ ≫ (toPresheaf R₀).map (toSheafify α φ')

Tactic:
toPresheaf_map_toSheafify

Goal state after:
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 φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')
⊢ (toPresheaf R₀).map τ₀ ≫ φ' = (toPresheaf R₀).map τ₀ ≫ φ'
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case e'_2.e'_7
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (c₀.π.app (Bicone.diagram j)).left =
    (c₀.π.app Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (c₀.π.app (Bicone.diagram j)).right =
    (c₀.π.app Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (c₀.π.app (Bicone.diagram j)).left =
    (c₀.π.app Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫ (c₀.π.app (Bicone.diagram j)).right =
    (c₀.π.app Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
e_1✝ :
  (c₀.pt.right ⟶ K.obj j) =
    ((((Functor.const (Bicone J)).obj c₀.pt).obj Bicone.left).right ⟶ ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right)
e_4✝ : c₁.pt.right = ((biconeMk J c₁ c₂).obj Bicone.left).right
e_5✝ : K.obj j = ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right
⊢ c.π.app j = ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right

Tactic:
simp [c₁, c₂]

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

Goal state before:
pp: case e'_3.e'_7
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (c₀.π.app (Bicone.diagram j)).left =
    (c₀.π.app Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (c₀.π.app (Bicone.diagram j)).right =
    (c₀.π.app Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (c₀.π.app (Bicone.diagram j)).left =
    (c₀.π.app Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫ (c₀.π.app (Bicone.diagram j)).right =
    (c₀.π.app Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
e_1✝ :
  (c₀.pt.right ⟶ K.obj j) =
    ((((Functor.const (Bicone J)).obj c₀.pt).obj Bicone.left).right ⟶ ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right)
e_4✝ : c₂.pt.right = ((biconeMk J c₁ c₂).obj Bicone.right).right
e_5✝ : K.obj j = ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right
⊢ c.π.app j = ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right

Tactic:
simp [c₁, c₂]

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
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
⊢ Presieve.IsSheafFor P E₀.presieve₀

Tactic:
Presieve.isSheafFor_iff_generate

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 (Sieve.generate E₀.presieve₀).arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_2
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
x✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ S ∈ J.toGrothendieck X

Tactic:
rw [← Sieve.generate_le_iff] at hle
    apply GrothendieckTopology.superset_covering _ hle
    exact generate_mem_toGrothendieck hR

Goal state after: