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

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
this : (fun x ↦ x') = ⇑(hom ↑(Fork.IsLimit.lift' t y' hy'))
⊢ x' = (hom ↑(Fork.IsLimit.lift' t y' hy')) PUnit.unit

Tactic:
rw [← this]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit S.arrows.cocone

Tactic:
exact
    { desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
        (yonedaFamily_fromCocone_compatible S s) |>.choose
      fac := by
        intro s f
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        have ht := H.choose_spec.1 f.obj.hom f.property
        cat_disch
      uniq := by
        intro s Fs HFs
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        apply H.choose_spec.2 Fs
        exact fun _ f hf => HFs ⟨Over.mk f, hf⟩ }

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S

Tactic:
rintro ⟨_, _⟩ ⟨_, _⟩ rfl

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
hf : x✝².arrows f
⊢ x✝¹.arrows f

Tactic:
· exact h₂ _ hf

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

Tactic:
by
  rw [Sieve.functorPushforward_le_iff_le_functorPullback, Sieve.functorPullback_pullback]
  apply Sieve.pullback_monotone
  exact Sieve.le_functorPushforward_pullback _ _

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ sieveOfSubfunctor S.functorInclusion = S

Tactic:
by
  ext
  simp only [functorInclusion_app, sieveOfSubfunctor_apply]
  constructor
  · rintro ⟨⟨f, hf⟩, rfl⟩
    exact hf
  · intro hf
    exact ⟨⟨_, hf⟩, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ (η ≫ J.toPlus Q).app x✝ = (J.toPlus P ≫ J.plusMap η).app x✝

Tactic:
dsimp [toPlus, plusMap]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ η.app x✝ ≫ ⊤.toMultiequalizer Q ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop x✝)) (op ⊤)) ≫ colimMap (J.diagramNatTrans η (unop x✝))
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ s ∈ G.obj U

Tactic:
rw [← this]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) ∈ G.obj U
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible

Tactic:
intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
hf₁ : (B H).arrows f₁
hf₂ : (B H).arrows f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (y H f₁ hf₁) = (ConcreteCategory.hom (P.map g₂.op)) (y H f₂ hf₂)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
⊢ ∀ (s : Cocone (Discrete.functor β)) (m : (sigmaCofan β).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = s.ι.app j) →
      m = ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ }

Tactic:
intro S m h
    ext ⟨i, x⟩
    simp only [← h]
    congr

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (empty C)
α : empty C ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)

Tactic:
have := h.isIso_to f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (empty C)
α : empty C ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: 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₂
⊢ m = ↾fun x ↦ Sum.casesOn x (fun x ↦ (ConcreteCategory.hom f₁) x) fun x ↦ (ConcreteCategory.hom f₂) x

Tactic:
ext x
          rcases x with x | x
          · exact ConcreteCategory.congr_hom h₁ x
          · exact ConcreteCategory.congr_hom h₂ x

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.right
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
⊢ { l //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd → m = l }

Tactic:
have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · exact ⟨val, rfl, fun y h => Sum.inr_injective h.symm⟩

Goal state after:
case h₁.right
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
this : ∀ (x : ↑s.pt), ∃! y, (ConcreteCategory.hom s.fst) x = Sum.inr y
⊢ { l //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
⊢ FinitaryExtensive D

Tactic:
by
  have : PreservesColimitsOfSize Gl := adj.leftAdjoint_preservesColimits
  constructor
  intro X Y c hc
  apply (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp
  have : ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
        PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl := by
    have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
    rw [this]
    rintro Z ⟨_ | _⟩ f <;> dsimp <;> infer_instance
  refine ((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective
    adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)
  · exact isColimitOfPreserves Gl (colimit.isColimit _)
  · exact (IsColimit.precomposeHomEquiv _ _).symm hc

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j ↦ f ↑j :=
  { hom := Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j ↦ f ↑j
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (c.ι.app { as := i })

Tactic:
rw [← this]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j ↦ f ↑j :=
  { hom := Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j ↦ f ↑j
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ HasPullback g (coprod.inl ≫ e'.inv)
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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P : Cᵒᵖ ⥤ A
⊢ J.W (adj.unit.app P)

Tactic:
W_eq_isLocal_range_sheafToPresheaf_obj

Goal state after:
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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P : Cᵒᵖ ⥤ A
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) (adj.unit.app P)
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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ J.W f ↔ IsIso (G.map f)

Tactic:
W_eq_isLocal_range_sheafToPresheaf_obj

Goal state after:
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
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f ↔ IsIso (G.map f)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive C

Tactic:
apply Adhesive.mk (hasPullback_of_mono_left := H₁) (hasPushout_of_mono_left := H₂)
  intro W X Y Z f g h i hf H
  rw [IsPushout.isVanKampen_iff]
  refine IsVanKampenColimit.of_mapCocone F ?_
  refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_
  refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm
  refine (IsPushout.isVanKampen_iff (H.map F)).mp ?_
  apply Adhesive.van_kampen

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₂
⊢ IsLocallyInjective J (Functor.whiskerRight φ (forget D)) → IsLocallyInjective J φ

Tactic:
intro
    exact ⟨fun x y h => equalizerSieve_mem J (Functor.whiskerRight φ (forget D)) x y h⟩

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
⊢ Subsingleton (Ext X Y i)

Tactic:
let := HasExt.standard C
  have := hX.subsingleton' i hi
  exact Ext.chgUniv.{w, max u v}.symm.subsingleton

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
M₀ : PresheafOfModules R₀
⊢ (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯).val =
    (𝟙 (sheafify α (CategoryTheory.toSheafify J M₀.presheaf))).val

Tactic:
apply (toPresheaf _).map_injective

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
M₀ : PresheafOfModules R₀
⊢ (toPresheaf R.obj).map
      (sheafifyMap α (CategoryTheory.toSheafify J M₀.presheaf) (CategoryTheory.toSheafify J M₀.presheaf) (𝟙 M₀)
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (𝟙 M₀)) ⋯).val =
    (toPresheaf R.obj).map (𝟙 (sheafify α (CategoryTheory.toSheafify J M₀.presheaf))).val
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
⊢ Projective X ↔ ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)

Tactic:
by
  refine ⟨fun h ↦ HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl),
    fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩
  obtain ⟨φ, hφ⟩ :=
    Ext.covariant_sequence_exact₃ _ { exact := ShortComplex.exact_kernel g }
      (Ext.mk₀ f) (zero_add 1) (by subsingleton)
  obtain ⟨φ, rfl⟩ := Ext.homEquiv₀.symm.surjective φ
  exact ⟨φ, Ext.homEquiv₀.symm.injective (by simpa using hφ)⟩

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
X✝ Y✝ Z✝ : PresheafOfModules R₀
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) (x✝¹ ≫ x✝)
        ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x✝¹ ≫ x✝)) ⋯).val =
    (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) x✝¹
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝¹) ⋯ ≫
        sheafifyMap α (CategoryTheory.toSheafify J Y✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) x✝
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝) ⋯).val

Tactic:
apply (toPresheaf _).map_injective

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
X✝ Y✝ Z✝ : PresheafOfModules R₀
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (toPresheaf R.obj).map
      (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) (x✝¹ ≫ x✝)
          ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map (x✝¹ ≫ x✝)) ⋯).val =
    (toPresheaf R.obj).map
      (sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) x✝¹
            ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝¹) ⋯ ≫
          sheafifyMap α (CategoryTheory.toSheafify J Y✝.presheaf) (CategoryTheory.toSheafify J Z✝.presheaf) x✝
            ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map x✝) ⋯).val
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
⊢ (sheafificationHomEquiv α) (f ≫ g) =
    (sheafificationHomEquiv α) f ≫ (SheafOfModules.forget R ⋙ restrictScalars α).map g

Tactic:
apply (toPresheaf _).map_injective

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 α
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)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : projectiveDimension X < ↑n
⊢ HasProjectiveDimensionLT X n

Tactic:
have : projectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : projectiveDimension X < ↑n
this : projectiveDimension X ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}
⊢ HasProjectiveDimensionLT X n
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

Tactic:
cases g
      apply BiconeHom.left

Goal state after: