mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑⟨a, b⟩)

Tactic:
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ Submonoid.powers (unop r) ≤
    Submonoid.comap
      (algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                  (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
              r)))
      (IsUnit.submonoid
        (Module.End ↑R
          ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                  (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
              r)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑⟨a, b⟩)

Tactic:
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _

Goal state after:
case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ Submonoid.powers (unop r) ≤
    Submonoid.comap
      (algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
      (IsUnit.submonoid
        (Module.End ↑R
          ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x) = x

Tactic:
by
  refine Subtype.ext <| ProjectiveSpectrum.ext <| HomogeneousIdeal.ext' ?_
  intro i z hzi
  refine (FromSpec.mem_carrier_iff_of_mem f_deg hm _ _ hzi).trans ?_
  exact (ToSpec.mk_mem_carrier _ _).trans (x.1.2.pow_mem_iff_mem m hm)

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝² x✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝² + x✝¹), ⋯⟩ x✝) =
    HomogeneousLocalization.val
      (↑(⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝², ⋯⟩ + ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩)
        x✝)

Tactic:
simp only [map_add, HomogeneousLocalization.val_add, Proj.add_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ LocallyOfFiniteType (awayι 𝒜 ↑i ⋯ ⋯ ≫ toSpecZero 𝒜)

Tactic:
Proj.awayι_toSpecZero,

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i))))
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i i' : I
f : i ⟶ i'
⊢ ↑(((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).map f ≫ ⟨limit.π (F ⋙ π A) i', ⋯⟩) =
    ↑(⟨limit.π (F ⋙ π A) i, ⋯⟩ ≫ F.map f)

Tactic:
simpa using! (limit.w _ _).symm

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

Goal state before:
pp: case mp
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
Y : C
y : Φ.fiber.obj Y
f : (unop (op ⟨Y, y⟩)).fst ⟶ (unop (op ⟨X, x⟩)).fst
hf : (ConcreteCategory.hom (Φ.fiber.map f)) (unop (op ⟨Y, y⟩)).snd = (unop (op ⟨X, x⟩)).snd
hf' :
  (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map (op ⟨f, hf⟩))) z₁ =
    (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map (op ⟨f, hf⟩))) z₂
⊢ ∃ Y f y,
    (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
      (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂

Tactic:
exact ⟨Y, f, y, hf, hf'⟩

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

Goal state before:
pp: case refine_1.refine_2
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ (a ≫ b) ≫ p = d ≫ F.map x₁

Tactic:
· rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : qcCoverFamily.property E
hF : ∀ (i : E.I₀), qcCoverFamily.property (F i)
⊢ qcCoverFamily.property (E.bind F)

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Goal state after:
S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : QuasiCompactCover E
hF : ∀ (i : E.I₀), QuasiCompactCover (F i)
⊢ QuasiCompactCover (E.bind F)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
⊢ qcCoverFamily.property (E.sum F)

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Goal state after:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : QuasiCompactCover E
hF : QuasiCompactCover F
⊢ QuasiCompactCover (E.sum F)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover f trivial
⊢ qcCoverFamily.property (cover f trivial).toPreZeroHypercover

Tactic:
simp only [qcCoverFamily_property, quasiCompactCover_iff]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover f trivial
⊢ QuasiCompactCover (cover f trivial).toPreZeroHypercover
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
f : X ⟶ Y
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
⊢ restriction data G₀ ((data X).f ((data X).multicospanShape.fst ⟨(i₁, i₂), j⟩) ≫ f) ≫
      ((data X).multicospanIndex G₀.obj).fst ⟨(i₁, i₂), j⟩ =
    restriction data G₀ ((data X).f ((data X).multicospanShape.snd ⟨(i₁, i₂), j⟩) ≫ f) ≫
      ((data X).multicospanIndex G₀.obj).snd ⟨(i₁, i₂), j⟩

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, cover_lift F J₀ _ (J.pullback_stable a (data Y).mem₀)⟩ _ _ ?_

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
f : X ⟶ Y
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.functorPullback F (Sieve.pullback a (data Y).toPreOneHypercover.sieve₀), ⋯⟩),
    (restriction data G₀ ((data X).f ((data X).multicospanShape.fst ⟨(i₁, i₂), j⟩) ≫ f) ≫
          ((data X).multicospanIndex G₀.obj).fst ⟨(i₁, i₂), j⟩) ≫
        G₀.obj.map I.f.op =
      (restriction data G₀ ((data X).f ((data X).multicospanShape.snd ⟨(i₁, i₂), j⟩) ≫ f) ≫
          ((data X).multicospanIndex G₀.obj).snd ⟨(i₁, i₂), j⟩) ≫
        G₀.obj.map I.f.op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this : ∃ i, i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ ⋯.HasLift

Tactic:
obtain ⟨i, hi⟩ := this

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ ⋯.HasLift
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ (Presieve.singleton f).EffectiveEpimorphic → EffectiveEpi f

Tactic:
intro (h : Nonempty _)
    rw [Sieve.generateSingleton_eq] at h
    constructor
    apply Nonempty.map (effectiveEpiStructOfIsColimit _) h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
⊢ Presieve.IsSheafFor F (Presieve.singleton (𝒰.forgetQc.sigma.f default))

Tactic:
obtain ⟨φ, hφ⟩ := Spec.map_surjective f

Goal state after:
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Presieve.IsSheafFor F (Presieve.singleton (𝒰.forgetQc.sigma.f default))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (continuousMapPresheafIsoUlift T)]
  apply Scheme.forgetToTop.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology
  apply TopCat.uliftFunctor.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology
  rw [isSheaf_iff_isSheaf_of_type]
  exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))

Tactic:
rw [Presieve.isSheafFor_singleton]

Goal state after:
case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ ∀ (x : (continuousMapPresheaf T).obj (Opposite.op (Spec S))),
    (∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
        p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
          (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
            (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x) →
      ∃! y, (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
⊢ ∀ (y : (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯

Tactic:
intro y hy
      rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]

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

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫ (presheafObjObjIso data G₀ ((data X).X i)).hom = presheafObjπ data G₀ X i

Tactic:
rw [← cancel_mono (presheafObjObjIso data G₀ ((data X).X i)).inv, assoc, Iso.hom_inv_id,
    comp_id]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) = presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : (monomorphisms C).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ monomorphisms C φ

Tactic:
by
    have (j : J) : Mono (f.app j) := hf _
    have := NatTrans.mono_of_mono_app f
    apply colim.map_mono' f hc₁ hc₂ φ (by simp [hφ])

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ }
this : Mono α
⊢ ∀ (j : J), c.ι.app j ≫ f = α.app j ≫ (constCocone J X).ι.app j

Tactic:
simpa using hf

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
⊢ Mono f

Tactic:
let α : F ⋙ MonoOver.forget _ ⋙ Over.forget _ ⟶ (Functor.const _).obj X :=
    { app j := (F.obj j).obj.hom }
  have := NatTrans.mono_of_mono_app α
  exact colim.map_mono' α hc (isColimitConstCocone J X) f (by simpa using hf)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ Subobject.mk f ≤ ⨆ j, Subobject.mk (F.obj j).obj.hom

Tactic:
rw [le_iSup_iff]

Goal state after:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (b : Subobject X), (∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ b) → Subobject.mk f ≤ b
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
j j' : J
g : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map g ≫ (F.obj j').obj.hom =
    (F.obj j).obj.hom ≫ ((Functor.const J).obj X).map g

Tactic:
by simp [MonoOver.forget]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ (colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom =
    ((Over.forget X).mapCocone c).ι.app j

Tactic:
← cancel_mono (c.pt.hom)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
      c.pt.hom =
    ((Over.forget X).mapCocone c).ι.app j ≫ c.pt.hom
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
⊢ functorObjTop f πX ≫ πX = functorObjLeft f πX ≫ π'FunctorObj f πX

Tactic:
by ext; simp [π'FunctorObj]

Goal state after: