mathlib-initiative/mathlib-tactics huggingface dataset:
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 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (valuation O K) (φ (Away.mk 𝒜 ⋯ (a * d i₀) ((∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1))) H)) ^ (d j * ∏ i, d i) =
    (∏ i, ψ i ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1))

Tactic:
by

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)
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y

Tactic:
by

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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ res data G₀ h₁ = res data G₀ h₂

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨(data X).sieve f, ⋯⟩⦄ (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
        G₀.obj.map r.g₁.op =
      (match I₂ with
        | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
        G₀.obj.map r.g₂.op

Tactic:
rintro ⟨Z₁, g₁, ⟨h₁⟩⟩ ⟨Z₂, g₂, ⟨h₂⟩⟩ ⟨T₀, p₁, p₂, w⟩

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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ { Y := Z₁, f := g₁, hf := ⋯ }.Y
p₂ : T₀ ⟶ { Y := Z₂, f := g₂, hf := ⋯ }.Y
w : p₁ ≫ { Y := Z₁, f := g₁, hf := ⋯ }.f = p₂ ≫ { Y := Z₂, f := g₂, hf := ⋯ }.f
⊢ (match { Y := Z₁, f := g₁, hf := ⋯ } with
      | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
      G₀.obj.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := w }.g₁.op =
    (match { Y := Z₂, f := g₂, hf := ⋯ } with
      | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
      G₀.obj.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := w }.g₂.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ P.precoverage.coverings S

Tactic:
by

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 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (∏ i, ψ i ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) ≤ (∏ i, ψ i₀ ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1))

Tactic:
by

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⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
R S : Presieve X
hR : R ∈ P.precoverage.coverings X
hS : S ∈ P.precoverage.coverings X
⊢ R ⊔ S ∈ P.precoverage.coverings X

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
⊢ F.map q₁ ≫ (data X).f h₁.i₀ = F.map q₂ ≫ (data X).f h₂.i₀

Tactic:
by

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

Goal state before:
pp: S : Scheme
E : PreZeroHypercover S
⊢ E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E

Tactic:
by

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

Goal state before:
pp: S : Scheme
X Y : Scheme
f : X ⟶ Y
hf : IsIso f
⊢ qcCoverFamily.property (PreZeroHypercover.singleton f)

Tactic:
by

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

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderBaseChange

Tactic:
by

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

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderComposition

Tactic:
by

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

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderSup

Tactic:
by

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

Goal state before:
pp: X : Scheme
inst✝ : IsEmpty ↥X
⊢ ⊥ ∈ qcPrecoverage.coverings X

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
hP : P ≤ fun x x_1 f ↦ IsOpenMap ⇑f
⊢ precoverage P ≤ qcPrecoverage

Tactic:
by

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

Goal state before:
pp: S : Scheme
⊢ Functor.IsDenseSubsite (topology S) S.smallEtaleTopology (AffineEtale.Spec S)

Tactic:
dsimp [topology]

Goal state after:
S : Scheme
⊢ Functor.IsDenseSubsite ((AffineEtale.Spec S).inducedTopology S.smallEtaleTopology) S.smallEtaleTopology
    (AffineEtale.Spec S)
Module: Mathlib.AlgebraicGeometry.Sites.AffineEtale

Goal state before:
pp: S : Scheme
⊢ Functor.IsDenseSubsite (topology S) S.smallEtaleTopology (AffineEtale.Spec S)

Tactic:
by

Goal state after:
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
⊢ Presieve.singleton f = (cover f trivial).presieve₀

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Presieve.singleton f ∈ qcPrecoverage.coverings Y

Tactic:
by

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

Goal state before:
pp: ⊢ Monotone propQCPrecoverage

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ propQCPrecoverage P

Tactic:
by

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover

Tactic:
by

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨(data X).sieve f, ⋯⟩⦄ (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
        G₀.obj.map r.g₁.op =
      (match I₂ with
        | { Y := Y₀, f := g, hf := hg } => restriction.res data G₀ (Nonempty.some hg)) ≫
        G₀.obj.map r.g₂.op

Tactic:
by

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ (𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).presieve₀ ∈ (precoverage P).coverings S

Tactic:
by

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ ∀ (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀),
    𝟙 ((QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i) ≫
        (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).f
          (Sum.inr i) =
      (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).f i

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
⊢ restriction data G₀ f ≫ G₀.obj.map g.op = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
by

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ Precoverage.ZeroHypercover.Small 𝒰

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ p ≫ (data X).f i = F.map (𝟙 X₀) ≫ f

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
R : Presieve S
x✝ : ∃ 𝒰, QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
𝒰 : Cover (precoverage P) S
left✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
h : R = 𝒰.presieve₀
⊢ 𝒰.presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
by

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
X₀ : C₀
f : F.obj X₀ ⟶ X
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ restriction data G₀ f = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
R : Presieve S
⊢ R ∈ (propQCPrecoverage P).coverings S ↔ ∃ 𝒰, QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ ⊥ ∈ (propQCTopology P) X

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Sieve.generate (Presieve.singleton f) ∈ (propQCTopology P) Y

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ∈ (propQCTopology P) S

Tactic:
by

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 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (∏ i, ψ i₀ ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) = ψ i₀ ^ (d i₀ * a * d j)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
W Z : C
e : W ⟶ Y
q : Z ⟶ W
⊢ (q ≫ e) ≫ f = q ≫ e ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ ∀ {Y_1 Z : C} {f_1 : Y_1 ⟶ X}, (∃ e, e ≫ f = f_1) → ∀ (g : Z ⟶ Y_1), ∃ e, e ≫ f = g ≫ f_1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ generate (Presieve.singleton f) = generateSingleton f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
R : Presieve X
⊢ R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (yoneda.obj Y) R

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : R.EffectiveEpimorphic
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor F R

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
⊢ 𝟙 (Over.mk f).left ≫ f = (Over.mk f).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
⊢ 𝟙 (Over.mk f).left ≫ f = (Over.mk f).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
Y' : D := { obj := Over.mk f, property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ f), property := ⋯ }
g₁' : Z' ⟶ Y' := ObjectProperty.homMk (Over.homMk g₁ ⋯)
⊢ g₂ ≫ Y'.obj.hom = Z'.obj.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
Y' : D := { obj := Over.mk f, property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ f), property := ⋯ }
g₁' : Z' ⟶ Y' := ObjectProperty.homMk (Over.homMk g₁ ⋯)
⊢ g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }

Tactic:
let g₂' : Z' ⟶ Y' := ObjectProperty.homMk (Over.homMk g₂ (by simp [Y', Z', h]))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
Y' : D := { obj := Over.mk f, property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ f), property := ⋯ }
g₁' : Z' ⟶ Y' := ObjectProperty.homMk (Over.homMk g₁ ⋯)
g₂' : Z' ⟶ Y' := ObjectProperty.homMk (Over.homMk g₂ ⋯)
⊢ g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }
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
⊢ ∀ (b : (data X).multicospanShape.R),
    restriction data G₀ ((data X).f ((data X).multicospanShape.fst b) ≫ f) ≫ ((data X).multicospanIndex G₀.obj).fst b =
      restriction data G₀ ((data X).f ((data X).multicospanShape.snd b) ≫ f) ≫ ((data X).multicospanIndex G₀.obj).snd b

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
⊢ ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
    g₁ ≫ f = g₂ ≫ f →
      g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }

Tactic:
by

Goal state after: