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

Goal state before:
pp: case inl
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
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom f) ((ConcreteCategory.hom s.fst) x) = (ConcreteCategory.hom f) (Sum.inl val)
⊢ ∃! y, Sum.inl val = Sum.inr y

Tactic:
cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

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

Goal state before:
pp: case refine_2.h₀
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit 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
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, 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' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
i j : J
g : i ⟶ j
⊢ Gr.map (F'.map g ≫ c'.ι.app j) = Gr.map (c'.ι.app i)

Tactic:
congr 1
        exact c'.w _

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

Goal state before:
pp: case mp
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),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
h'

Goal state after:
case mp
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),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr
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' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
⊢ ∀ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
h'

Goal state after:
case mpr
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' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
⊢ ∀ (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inl
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 : ↑X'
h : (ConcreteCategory.hom f) ((ConcreteCategory.hom s.fst) x) = (ConcreteCategory.hom f) (Sum.inl val)
⊢ ∃! y, Sum.inl val = Sum.inr y

Tactic:
cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ Nonempty (IsColimit c)

Tactic:
refine hau.nonempty_isColimit_of_pullbackCone_left _ (𝟙 _) _ _ (fun i ↦ ?_)
    (PullbackCone.mk (𝟙 _) f (by simp)) (IsPullback.id_horiz f).isLimit _ (Iso.refl _)
    (by simp) (by simp [c]) (by simp [pullback.condition, c])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
i : α
⊢ IsLimit (limit.cone (cospan f (π i)))
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ 𝟭 D₁ ⟶ G' ⋙ F'

Tactic:
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
    Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso.symm

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso := (CatCommSq.iso (G ⋙ F) L₁ L₁ (G' ⋙ F')).symm }
⊢ 𝟭 D₁ ⟶ G' ⋙ F'
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
· exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
      dsimp
      infer_instance)).some

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
⊢ IsSheaf J (F.op ⋙ G)

Tactic:
intro X S hS
  rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, ← Functor.whiskeringLeft_obj_obj,
    ← adj.map_comp_bijective_iff]
  refine h hS _ ?_
  rwa [isSheaf_iff_isSheaf_of_type]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
· exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
      dsimp
      infer_instance)).some

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ IsIso f

Tactic:
← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _),

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ IsIso ((sheafToPresheaf J (Type w)).map f)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: 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
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
⊢ Nonempty (IsColimit d)

Tactic:
let iso : d ≅ (Cofan.mk _ fun i : ι ↦ PullbackCone.IsLimit.lift ht
      (s i).fst ((s i).snd ≫ a.inj i) (by simp [hu, (s i).condition])) :=
    Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht (by simp [he₁]) (by simp [he₂])

Goal state after:
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
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
⊢ Nonempty (IsColimit d)
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
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)

Tactic:
exact Ext.chgUniv.{w, max u v}.symm.subsingleton

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
⊢ HasProjectiveDimensionLT S.X₃ (n + 1)

Tactic:
let := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  rintro (_ | i) hi Y x₃
  · simp at hi
  · obtain ⟨x₁, rfl⟩ := Ext.contravariant_sequence_exact₃ hS _ x₃
      (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) hi) (add_comm _ _)
    rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]

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₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P₀.presheaf
          ((SheafOfModules.toSheaf R).obj N)).symm
      ((toPresheaf R₀).map (f ≫ g)) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g)

Tactic:
toSheaf_map_sheafificationHomEquiv_symm α g,

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₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P₀.presheaf
          ((SheafOfModules.toSheaf R).obj N)).symm
      ((toPresheaf R₀).map (f ≫ g)) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv Q₀.presheaf
            ((SheafOfModules.toSheaf R).obj N)).symm
        ((toPresheaf R₀).map g)
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
⊢ projectiveDimension M = projectiveDimension N

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot => simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_rightOp
    exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F

Tactic:
by
  refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
  · suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _
    apply IsCofiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
  · suffices IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ from isCofiltered_of_isFiltered_op _
    suffices IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ from
      IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).op
    apply IsFiltered.of_equivalence (opOpEquivalence _)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G✝ : D ⥤ E
G : D ⥤ Type u_4
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered G.Elements
⊢ IsCofiltered (F ⋙ G).Elements

Tactic:
by
  suffices h : IsCofiltered (StructuredArrow PUnit (F ⋙ G)) from
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _).symm
  have : IsCofiltered (StructuredArrow PUnit G) :=
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _)
  infer_instance

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

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
⊢ IsSeparatedFor P T

Tactic:
intro x y₁ y₂ h₁ h₂
    refine hS.1.ext (fun Y g hg => ?_)
    simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
by
    obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows
    have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) :
        ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j := by
      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
      use j, rfl
      simp
    choose j h₁ h₂ using this
    refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
    convert! E.mem₀
    exact le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))

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

Goal state before:
pp: case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun Y f hf ↦ S' ⋯) u
⊢ S.arrows u

Tactic:
· obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
          exact hS'le _ _ _ hg

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
this : IsSheafFor (F.op ⋙ (Functor.closedSieves K).toFunctor) (ofArrows Y f)
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))

Tactic:
Presieve.isSheafFor_arrows_iff

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
this :
  ∀ (x : (i : ι) → (F.op ⋙ (Functor.closedSieves K).toFunctor).obj (op (Y i))),
    Arrows.Compatible (F.op ⋙ (Functor.closedSieves K).toFunctor) f x →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ (Functor.closedSieves K).toFunctor).map (f i).op)) t = x i
⊢ ∀ (x : (i : ι) → (Functor.closedSieves K).toFunctor.obj (op (F.obj (Y i)))),
    Arrows.Compatible (Functor.closedSieves K).toFunctor (fun i ↦ F.map (f i)) x →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((Functor.closedSieves K).toFunctor.map (F.map (f i)).op)) t = x i
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.restrictedTopology K = F.inducedTopology K

Tactic:
refine le_antisymm ?_ inducedTopology_le_restrictedTopology

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.restrictedTopology K ≤ F.inducedTopology K
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (i : WidePullbackShape J), F i = F none

Tactic:
rintro ⟨⟩

Goal state after:
case none
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

case some
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
val✝ : J
⊢ F (some val✝) = F none
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (i : WidePushoutShape J), F i = F none

Tactic:
rintro ⟨⟩

Goal state after:
case none
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

case some
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
val✝ : J
⊢ F (some val✝) = F none
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h : (ConcreteCategory.hom (F.map (𝟙 X).op)) (⋯.amalgamate (x.familyOfElements X) ⋯) = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)