mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: 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)
hxd' : ∀ (i : ι'), 0 < dv i
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤

Tactic:
rw [← top_le_iff]
  change ⊤ ≤ (Algebra.adjoin (𝒜 0) _).toSubmodule
  rw [← HomogeneousLocalization.Away.span_mk_prod_pow_eq_top hf v hx dv hxd, Submodule.span_le]
  rintro _ ⟨a, ai, hai, rfl⟩
  have H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k := by
    rw [smul_eq_mul, tsub_mul, ← smul_eq_mul, ← hai]
    conv => enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
    simp_rw [smul_eq_mul, add_mul, Finset.sum_add_distrib,
      mul_assoc, ← Finset.mul_sum, mul_comm d, mul_comm (_ / _)]
    simp only [add_tsub_cancel_right]
  have H : Away.mk 𝒜 hf a (∏ i, v i ^ ai i)
      (hai ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) =
      Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i, v i ^ (ai i % d))
      (H₀ ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) *
      ∏ i, Away.isLocalizationElem hf (hxd i) ^ (ai i / d) := by
    apply (show Function.Injective (algebraMap (Away 𝒜 f) (Localization.Away f))
      from val_injective _)
    simp only [map_pow, map_prod, map_mul]
    simp only [HomogeneousLocalization.algebraMap_apply, val_mk,
      Localization.mk_pow, Localization.mk_prod, Localization.mk_mul,
      ← Finset.prod_mul_distrib, ← pow_add, ← pow_mul]
    congr
    · ext i
      congr
      exact Eq.symm (Nat.mod_add_div (ai i) d)
    · simp only [SubmonoidClass.coe_finsetProd, ← pow_add, ← pow_mul,
        Finset.prod_pow_eq_pow_sum, SubmonoidClass.coe_pow]
      rw [tsub_add_cancel_of_le]
      rcases d.eq_zero_or_pos with hd | hd
      · simp [hd]
      rw [← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul (a := a), ← hai, Finset.sum_mul]
      simp_rw [smul_eq_mul, mul_comm (ai _), mul_assoc]
      gcongr
      exact Nat.div_mul_le_self (ai _) d
  rw [H, SetLike.mem_coe]
  apply (Algebra.adjoin (𝒜 0) _).mul_mem
  · apply Algebra.subset_adjoin
    refine ⟨a - ∑ i : ι', dv i * (ai i / d), (ai · % d), H₀.symm, ?_, rfl⟩
    rcases d.eq_zero_or_pos with hd | hd
    · have : ∀ (x : ι'), ai x = 0 := by simpa [hd, fun i ↦ (hxd' i).ne'] using hai
      simp [this]
    exact fun i ↦ (Nat.mod_lt _ hd).le
  apply prod_mem
  · classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
| (f ^ ⨆ i, n i) • s' i

Tactic:
rw [hN i]

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
| f ^ ((⨆ i, n i) - n i + n i) • s' i
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝² : IsDomain ↑(CommRingCat.of R)
this✝¹ : ValuationRing ↑(CommRingCat.of R)
this✝ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this : IsLocalHom (CommRingCat.Hom.hom e.hom)
⊢ ⋯.HasLift

Tactic:
have : IsLocalHom α.hom := inferInstanceAs
    (IsLocalHom (((pullback.fst i₂ f).stalkMap x).hom.comp e.hom.hom))

Goal state after:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
⊢ ⋯.HasLift
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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ i * m = i + (m - 1) • i

Tactic:
rw [← succ_nsmul', tsub_add_cancel_of_le (by lia), mul_comm, smul_eq_mul]

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
⊢ ∀ ⦃X : Over S⦄ (S_1 : Presieve X) (Ti : ⦃Y : Over S⦄ → (f : Y ⟶ X) → S_1 f → Presieve Y),
    S_1 ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver} →
      (∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : S_1 f), Ti f H ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}) →
        S_1.bind Ti ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}

Tactic:
rintro X _ T ⟨𝒰, h, rfl⟩ H
    choose V h hV using H
    refine ⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩
    convert!
      Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)
    apply hV

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : UniversallyClosed (pullback.diagonal f)
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
exact .of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)

Tactic:
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop

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 ≫ fst ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)

Tactic:
pullbackAwayιIso_inv_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
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯)) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
⊢ ∃ ι U f,
    Sieve.ofArrows (fun i ↦ (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i)) f ∈
      (smallGrothendieckTopology P S) X

Tactic:
let 𝒱 : Cover (precoverage P) X.left :=
      𝒰.openCover.changeProp (fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _)

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
⊢ ∃ ι U f,
    Sieve.ofArrows (fun i ↦ (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i)) f ∈
      (smallGrothendieckTopology P S) X
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

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

Tactic:
rw [← PreZeroHypercover.presieve₀_shrink, Scheme.qcPrecoverage,
    E.shrink.presieve₀_mem_precoverage_iff]
  simp

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

Goal state before:
pp: case refine_3.inr.refine_1
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F (Sieve.pullback (T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
← Sieve.pullbackArrows_comm,

Goal state after:
case refine_3.inr.refine_1
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.pullbackArrows (T.affineOneHypercover.f i) 𝒰.presieve₀)).arrows
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3.inr.refine_2
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
← Sieve.pullbackArrows_comm,

Goal state after:
case refine_3.inr.refine_2
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.generate
        (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)).arrows
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)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ ⋯.HasLift

Tactic:
have : Set.range i₁ ⊆ (Proj.awayι 𝒜 _ (hxd i i.2) (hd i i.2).bot_lt).opensRange := by
    rw [Proj.opensRange_awayι]
    rintro _ ⟨x, rfl⟩
    obtain rfl := Subsingleton.elim x (IsLocalRing.closedPoint K)
    exact hi

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
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_1
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)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Sieve.pullback (V.affineOneHypercover.f i)
        (Sieve.generate
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).X
            (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f))).arrows

Tactic:
← Sieve.pullbackArrows_comm,

Goal state after:
case refine_1
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)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Sieve.generate
        (Presieve.pullbackArrows (V.affineOneHypercover.f i)
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).X
            (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f))).arrows
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ generate (Presieve.ofArrows X π) = generateFamily X π

Tactic:
ext Y g

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g ↔ (generateFamily X π).arrows g