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

Goal state before:
pp: X : Scheme
P✝ : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtSource P✝
S : Scheme
J : Type u_1
inst✝⁸ : Category.{v_1, u_1} J
F : J ⥤ P✝.Over ⊤ S
inst✝⁷ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝⁶ : (F ⋙ MorphismProperty.Over.forget P✝ ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝⁵ : Quiver.IsThin J
inst✝⁴ : Small.{u, u_1} J
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtSource P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.HasOfPostcompProperty P
inst✝ : P.IsMultiplicative
n : ℕ
⊢ HasColimitsOfShape (Discrete (Fin n)) (P.CostructuredArrow ⊤ Scheme.Spec S)

Tactic:
have : (MorphismProperty.commaObj Scheme.Spec (.fromPUnit S) P).IsClosedUnderColimitsOfShape
        (Discrete (Fin n)) :=
      IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete _ _

Goal state after:
X : Scheme
P✝ : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtSource P✝
S : Scheme
J : Type u_1
inst✝⁸ : Category.{v_1, u_1} J
F : J ⥤ P✝.Over ⊤ S
inst✝⁷ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝⁶ : (F ⋙ MorphismProperty.Over.forget P✝ ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝⁵ : Quiver.IsThin J
inst✝⁴ : Small.{u, u_1} J
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtSource P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.HasOfPostcompProperty P
inst✝ : P.IsMultiplicative
n : ℕ
this : (MorphismProperty.commaObj Scheme.Spec (Functor.fromPUnit S) P).IsClosedUnderColimitsOfShape (Discrete (Fin n))
⊢ HasColimitsOfShape (Discrete (Fin n)) (P.CostructuredArrow ⊤ Scheme.Spec S)
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
by
  rw [← ih_η]
  apply Iso.ext (by simp [← whisker_exchange_assoc])

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
simp_rw [left_triangle]; bicategory

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
⊢ (∀ x ∈ U.overEquivalence.functor.obj V,
      ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1) →
    S ∈ ((Opens.grothendieckTopology X).over U) V

Tactic:
intro H x hxV

Goal state after:
case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
x : X
hxV : x ∈ V.left
⊢ ∃ U_1 f, ((Sieve.overEquiv V) S).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
⊢ S ∈ ((Opens.grothendieckTopology X).over U) V →
    ∀ x ∈ U.overEquivalence.functor.obj V,
      ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1

Tactic:
intro H x hxV

Goal state after:
case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
hxV : x ∈ U.overEquivalence.functor.obj V
⊢ ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm

Tactic:
by
  apply Iso.ext
  dsimp [adjointifyCounit, bicategoricalIsoComp]
  calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((g ≫ S.isoSpec.hom) t)

Tactic:
← Scheme.isoSpec_hom_naturality

Goal state after:
X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((T.isoSpec.hom ≫ Spec.map (Scheme.Hom.appTop g)) t)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
h : x ≠ 0
⊢ (ordFrac R) ((algebraMap R K) x) = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹

Tactic:
ordFrac_eq_ord R h,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
h : x ≠ 0
⊢ (ordMonoidWithZeroHom R) x = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den

Tactic:
ProjectiveSpectrum.mem_basicOpen

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
refine sInf_le_sInf_of_isCoinitialFor ?_

Goal state after:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ IsCoinitialFor {J | I ≤ J ∧ J.IsPrime} {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c = 0
⊢ c ∉ DFinsupp.support ((DirectSum.decompose 𝒜) x)

Tactic:
simpa [hc] using hx

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ a ∈ Subalgebra.toSubmodule ⊤

Tactic:
trivial

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

Goal state before:
pp: case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
      ((algebraMap A (Localization.Away x.snd.fst)).comp (algebraMap (↥(𝒜 0)) A)) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))

Tactic:
← RingHom.comp_assoc,

Goal state after:
case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ ((IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp (algebraMap A (Localization.Away x.snd.fst))).comp
      (algebraMap (↥(𝒜 0)) A) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜 = X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A)))

Tactic:
refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_
  simp only [fromOfGlobalSections, toBasicOpenOfGlobalSections, CommRingCat.ofHom_comp,
    Category.assoc, Scheme.Cover.ι_glueMorphisms_assoc, basicOpenIsoSpec_inv_ι_assoc,
    awayι_toSpecZero, Iso.inv_comp_eq]
  simp only [openCoverOfMapIrrelevantEqTop,
    Scheme.openCoverOfIsOpenCover_f, Scheme.isoOfEq_hom_ι_assoc, ← morphismRestrict_ι_assoc]
  congr 1
  simp only [basicOpenIsoSpecAway, ← CommRingCat.ofHom_comp, ← Spec.map_comp, ← Iso.eq_inv_comp,
    IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, ← HomogeneousLocalization.algebraMap_eq]
  congr 2
  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ A,
    ← RingHom.comp_assoc, IsLocalization.map_comp, RingHom.comp_assoc]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
s : (x : ↥U) → AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule
hs : (ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred s
⊢ (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ).pred (comapStructureSheafFun f hf U V hUV s)

Tactic:
rintro ⟨p, hpV⟩
  rcases hs ⟨.comap f hf p, hUV hpV⟩ with ⟨W, m, iWU, i, a, b, hb, h_frac⟩
  refine ⟨W.comap (ProjectiveSpectrum.comap f hf) ⊓ V, ⟨m, hpV⟩, Opens.infLERight _ _, i,
    f.gradedAddHom i a, f.gradedAddHom i b, fun ⟨q, ⟨hqW, hqV⟩⟩ ↦ hb ⟨_, hqW⟩,
    fun ⟨q, ⟨hqW, hqV⟩⟩ ↦ ?_⟩
  ext
  specialize h_frac ⟨_, hqW⟩
  simp_all [comapStructureSheafFun]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ IsIntegral O x → v x ≤ 1

Tactic:
rintro ⟨f, hm, hf⟩
    by_cases hn : f.natDegree = 0
    · rw [Polynomial.natDegree_eq_zero] at hn
      obtain ⟨c, rfl⟩ := hn
      simp [map_eq_zero_iff _ hv.hom_inj, hm.ne_zero_of_C] at hf
    simp only [Polynomial.eval₂_eq_sum_range, Finset.sum_range_succ, hm.coeff_natDegree, map_one,
      one_mul, add_eq_zero_iff_eq_neg] at hf
    apply_fun v at hf
    simp only [map_neg, map_pow] at hf
    contrapose! hf
    refine ne_of_lt (v.map_sum_lt ?_ ?_)
    · simp [hn, (hf.trans' (zero_lt_one)).ne']
    · simp only [Finset.mem_range, map_mul, map_pow]
      intro _ hi
      exact mul_lt_of_le_one_of_lt (hv.map_le_one _) <| pow_lt_pow_right₀ hf hi

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case refine_1.inl
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
i : ι'
hi : dv i = 0
⊢ v i ∈ ↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (v ∘ Subtype.val)))

Tactic:
exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
⊢ (Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver) = Sieve.ofArrows 𝒰.X 𝒰.f

Tactic:
by
  ext V f
  simp only [Sieve.overEquiv_iff, Sieve.generate_apply]
  constructor
  · rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
    exact ⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩
  · rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
    have : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S := comp_over (𝒰.f k) S
    refine ⟨(𝒰.X k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.f k).asOver S, ⟨k⟩, ?_⟩
    ext : 1
    simpa

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

Goal state before:
pp: case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ (pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯).inv ≫
      (pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j)
            (toSpecZero 𝒜)).inv ≫
        snd (diagonal (toSpecZero 𝒜))
            ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                  (toSpecZero 𝒜)).f
              (i, j)) ≫
          fst ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)

Tactic:
pullbackDiagonalMapIdIso_inv_snd_fst

Goal state after:
case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ (pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯).inv ≫ fst ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ 𝒰.toPresieveOverProp p (Hom.asOverProp (𝒰.f (𝒰.idx x)) S)

Tactic:
use 𝒰.idx x

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasCoproducts A
inst✝² : HasSeparator A
inst✝¹ : HasZeroMorphisms A
inst✝ : HasCoproducts A
⊢ (ObjectProperty.ofObj fun x ↦ separator A).IsSeparating

Tactic:
by simpa using! isSeparator_separator A

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasCoproducts A
inst✝³ : HasWeakSheafify J A
inst✝² : HasSeparator A
inst✝¹ : Preadditive A
inst✝ : HasCoproducts A
⊢ (ObjectProperty.ofObj fun x ↦ separator A).IsSeparating

Tactic:
by simpa using! isSeparator_separator A

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h₁ : ∀ {X : C}, P.property.IsClosedUnderIsomorphisms
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y

Tactic:
let F : PreZeroHypercover Y := ⟨_, _, p₁⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h₁ : ∀ {X : C}, P.property.IsClosedUnderIsomorphisms
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: S : Scheme
T : Type v
inst✝¹ : TopologicalSpace T
inst✝ : TotallyDisconnectedSpace T
U : Scheme
f : C(ConnectedComponents ↥U, T)
⊢ (fun f ↦ { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ })
      ((fun f ↦ f.comp { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ }) f) =
    f

Tactic:
apply ContinuousMap.coe_injective
    dsimp
    exact (Continuous.connectedComponentsLift_unique _ _ (by simp)).symm

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

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
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk f

Tactic:
· rw [le_iSup_iff]
    intro s H
    induction s using Subobject.ind with | _ g
    let c' : Cocone (F ⋙ MonoOver.forget _ ⋙ Over.forget _) := Cocone.mk _
      { app j := Subobject.ofMkLEMk _ _ (H j)
        naturality j j' f := by
          dsimp
          simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp,
            Category.comp_id] using MonoOver.w (F.map f) }
    exact Subobject.mk_le_mk_of_comm (hc.desc c')
      (hc.hom_ext (fun j ↦ by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]))

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
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk f