mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x : ToType (F.obj X)
⊢ equalizerSieve x x = ⊤

Tactic:
aesop

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₃
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
X : Cᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (G.ι.app X))

Tactic:
intro ⟨x, _⟩ ⟨y, _⟩ h

Goal state after:
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₃
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property✝¹ : x ∈ G.obj X
y : F.obj X
property✝ : y ∈ G.obj X
h : (ConcreteCategory.hom (G.ι.app X)) ⟨x, property✝¹⟩ = (ConcreteCategory.hom (G.ι.app X)) ⟨y, property✝⟩
⊢ ⟨x, property✝¹⟩ = ⟨y, property✝⟩
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case mp
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₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
a✝ : IsLocallySurjective J f₃
⊢ IsLocallySurjective J f₂

Tactic:
exact isLocallySurjective_of_isLocallySurjective_fac J fac

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

Goal state before:
pp: case mp
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₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂) → IsLocallySurjective J f₁

Tactic:
intro
    exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

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

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

Tactic:
obtain ⟨w, hw⟩ := hv
    obtain ⟨⟨i⟩, a, rfl⟩ := Types.jointly_surjective_of_isColimit
      (isColimitOfPreserves ((evaluation _ _).obj (op V)) hc) w
    obtain ⟨a : V ⟶ X i, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a
    refine ⟨_, a, _, ⟨i⟩, shrinkYonedaObjObjEquiv.symm.injective ?_⟩
    rw [← shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]
    convert! hw using 1
    · exact (ConcreteCategory.congr_hom (NatTrans.congr_app
        ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
          (shrinkYonedaObjObjEquiv.symm a)).symm
    · exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

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

Goal state before:
pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg : (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows g
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z)))
      ((ConcreteCategory.hom (R₀.map g.op)) r₀ • (ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z)))
      ((ConcreteCategory.hom (R₀.map g.op)) r₀' • (ConcreteCategory.hom (M₀.map g.op)) m₀')

Tactic:
hg.1,

Goal state after:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg : (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows g
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z)))
      ((ConcreteCategory.hom (R₀.map g.op)) r₀' • (ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z)))
      ((ConcreteCategory.hom (R₀.map g.op)) r₀' • (ConcreteCategory.hom (M₀.map g.op)) m₀')
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
h : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)
E✝ X✝ : C
f : X ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ (Ext.mk₀ f).comp ⋯.extClass ⋯ = 0

Tactic:
by subsingleton

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✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
by
    apply +allowSynthFailures preservesColimitsOfShape_unop
    exact preservesLimitsOfShape_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
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 := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
X : J
⊢ ((F.mapCone c).toStructuredArrow ⋙ map f₂).obj X = s.toStructuredArrow.obj X

Tactic:
simp [← h₂]

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
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 := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₁ = hc.lift (c.extend (Hom.right g₁))

Tactic:
apply hc.uniq (c.extend _)
      simp

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.left ⟶ Bicone.right
⊢ f ∈ ∅

Tactic:
by cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.right ⟶ Bicone.left
⊢ f ∈ ∅

Tactic:
by cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.left
⊢ f ∈ ∅

Tactic:
by cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.right
⊢ f ∈ ∅

Tactic:
by cases f

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

Goal state before:
pp: case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g

Tactic:
obtain ⟨W, i, e, h1, h2⟩ := hT2 hg

Goal state after:
case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ (∀ (E : D) {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (P ⋙ coyoneda.obj (Opposite.op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ coyoneda.obj E) R

Tactic:
aesop

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒱.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
← Presieve.isSheafFor_iff_generate

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f) ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Module: Mathlib.CategoryTheory.Sites.Continuous

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
G : Dᵒᵖ ⥤ Type u_1
h : Presieve.IsSheaf K G
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type] at h ⊢
  exact F.op_comp_isSheaf_of_isSheaf _ _ _ h

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
⊢ lift hF hR s ≫ R.map i.f.op = s.ι i

Tactic:
apply (hR (op i.Y)).hom_ext
  intro j
  have eq := fac' hF hR s (StructuredArrow.mk (i.f.op ≫ j.hom))
  dsimp at eq ⊢
  simp only [Functor.map_comp, Category.assoc] at eq
  rw [Category.assoc, eq]
  simpa using liftAux_map hF α s (j.hom.unop ≫ i.f) (𝟙 _) i j.hom.unop (by simp)

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

Goal state before:
pp: case hex
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
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
⊢ ∃ x_1, x.IsAmalgamation x_1

pp: case hunique
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
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.obj).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
· have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)
      exact ⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
        fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
          (hF₁.apply_map _ hx hf)⟩

Goal state after:
case hunique
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
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.obj).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
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) (Sieve.generate (ofArrows Y f)).arrows
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))

Tactic:
← Presieve.isSheafFor_iff_generate

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 : 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))
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
U V : C
f₁ f₂ : U ⟶ V
⊢ ∀ {Y Z : C} {f : Y ⟶ U}, f ≫ f₁ = f ≫ f₂ → ∀ (g : Z ⟶ Y), (g ≫ f) ≫ f₁ = (g ≫ f) ≫ f₂

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.equalizer f₁ f₂, ⋯⟩),
    F.obj.map f₁.op ≫ F.obj.map I.f.op = F.obj.map f₂.op ≫ F.obj.map I.f.op

Tactic:
rintro ⟨W₀, a, ha⟩
      dsimp at ha ⊢
      simp only [← Functor.map_comp, ← op_comp, ha]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝⁴ : Category.{v_4, u_4} A
inst✝³ : IsDenseSubsite J K G
inst✝² : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
⊢ HasSheafify K A

Tactic:
by
  have : PreservesFiniteLimits (presheafToSheaf J A ⋙
    (G.sheafPushforwardContinuous A J K).inv) := by
    apply comp_preservesFiniteLimits
  have : PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A) := by
    apply comp_preservesFiniteLimits
  exact HasSheafify.mk' _ _ (sheafifyAdjunctionOfIsEquivalence J K G A)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
H : Sieve.functorPushforward e.functor S ∈ K (e.functor.obj X)
⊢ Sieve.functorPullback e.functor (Sieve.functorPushforward e.functor S) ≤ S

Tactic:
rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := ⋯
c : T ⟶ Y₁ := ⋯
d : T ⟶ W := ⋯
⊢ Over.Hom.left (c ≫ f) = Over.Hom.left (d ≫ a)

Tactic:
exact w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
Z : C
f : Z ⟶ Y.left
⊢ ((overEquiv Y) S).arrows f ↔ S.arrows (Over.homMk f ⋯)

Tactic:
by
  obtain ⟨S, rfl⟩ := (overEquiv Y).symm.surjective S
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hunique
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
⊢ ∀ (y₁ y₂ : ↑F.sections),
    (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂

Tactic:
· intro y₁ y₂ hy₁ hy₂
    exact hY.sections_ext ⟨F, hF⟩ (fun i => by rw [hy₁, hy₂])

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
I : Type u_2
X : I → C
hX : J.CoversTop X
I' : I → Type u
Y : (i : I) → I' i → Over (X i)
hY : ∀ (i : I), (J.over (X i)).CoversTop (Y i)
j Z : C
f : Z ⟶ j
x✝ : (Sieve.ofObjects X j).arrows f
i : I
g : Z ⟶ X i
i' : C
⊢ i' ∈ Set.range ((Over.forget (X i)).obj ∘ Y i) → i' ∈ Set.range fun j ↦ (Y j.fst j.snd).left

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f g : X ⟶ Y
h : f = g
⊢ J.overMapPullbackCongr A h = eqToIso ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
⊢ ∃ i, x ∈ coveringOfPresieve U R i

Tactic:
obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ coveringOfPresieve U R i
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case single.pair.right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i i' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.right i' i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i' i))

Tactic:
exact (h i' i).symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
inst✝ : M.IsFinitePresentation
⊢ ∃ σ, σ.IsFiniteType

Tactic:
obtain ⟨σ, _⟩ := IsFinitePresentation.exists_quasicoherentData M
    exact ⟨σ.localGeneratorsData, inferInstance⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : ContinuousAdd M
inst✝² : Module R M
inst✝¹ : ContinuousSMul R M
inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : y ∈ interior ↑s
x : M
⊢ x ∈ s

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : ContinuousAdd M
inst✝² : Module R M
inst✝¹ : ContinuousSMul R M
inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
⊢ x ∈ s
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
⊢ ∃ U, ∃ (m : x ∈ U) (_ : U ∈ B), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
by
  obtain ⟨U, hxU, s, rfl⟩ := F.exists_germ_eq t
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hB.exists_subset_of_mem_open hxU U.2
  exact ⟨V, hxV, hV, F.map (homOfLE hVU).op s, by rw [← ConcreteCategory.comp_apply, F.germ_res']⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case fst
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).1 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).1

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case snd
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).2 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).2

Tactic:
aesop

Goal state after: