mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩ *
        (algebraMap A (Localization (Submonoid.powers f))) ↑z.num ∈
      Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
Ideal.unit_mul_mem_iff_mem,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (algebraMap A (Localization (Submonoid.powers f))) ↑z.num ∈
      Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

case hy
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩)
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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : (algebraMap A (at 𝔭.primeCompl)) (↑f.num * b) = (algebraMap A (at 𝔭.primeCompl)) ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
IsLocalization.eq_iff_exists (M := 𝔭.primeCompl)

Goal state after:
ι : 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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0

Goal state after:
ι : 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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
⊢ IsUnit (mk f)
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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
      (Quotient.mk'' x + Quotient.mk'' y) =
    Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' x) +
      Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' y)

Tactic:
by
    simp only [← mk_add, Quotient.map'_mk'', num_add, map_add, map_mul, den_add]; rfl

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Away 𝒜 f →+* Away 𝒜 x

Tactic:
by
  let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)
  refine RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion ?_))
    (awayMapAux 𝒜 (f := f) ⟨_, hx⟩).rangeRestrict
  exact range_awayMapAux_subset 𝒜 hg hx

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

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
⊢ ∀ (m : ↑((Spec R).ringCatSheaf.obj.obj U)) (x : ↑(M.val.1 U)),
    (ModuleCat.Hom.hom (f.hom.app U)).toFun (m • x) =
      (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) m • (ModuleCat.Hom.hom (f.hom.app U)).toFun x

Tactic:
intro t m

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
⊢ (ModuleCat.Hom.hom (f.hom.app U)).toFun (t • m) =
    (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) t • (ModuleCat.Hom.hom (f.hom.app U)).toFun m
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 = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r = X.basicOpen (f r)

Tactic:
by
  apply le_antisymm
  · intro x hx
    obtain ⟨i, x, rfl⟩ := (openCoverOfMapIrrelevantEqTop 𝒜 f hf).exists_eq x
    rw [← SetLike.mem_coe] at hx -- TODO : mem version of TopologicalSpace.Opens.map_coe
    simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage, SetLike.mem_coe,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections, Scheme.Cover.ι_glueMorphisms] at hx
    simp only [openCoverOfMapIrrelevantEqTop,
      toBasicOpenOfGlobalSections, Scheme.isoOfEq_inv, Category.assoc, basicOpenIsoSpec_inv_ι] at hx
    simp only [Scheme.Hom.comp_base, Scheme.homOfLE_base, homOfLE_leOfHom, TopCat.hom_comp,
      ContinuousMap.comp_assoc, ContinuousMap.comp_apply, morphismRestrict_base,
      TopologicalSpace.Opens.carrier_eq_coe] at hx
    rw [← SetLike.mem_coe, ← Set.mem_preimage, ← TopologicalSpace.Opens.map_coe,
      Proj.awayι_preimage_basicOpen (𝒜 := 𝒜) i.2.2.2 i.2.2.1 hr hn,
      ← Set.mem_preimage, ← TopologicalSpace.Opens.map_coe, ← Function.Injective.mem_set_image
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(X, ⊤) _))).isOpenEmbedding.injective,
      ← Scheme.Hom.comp_apply, basicOpenIsoSpecAway, IsOpenImmersion.isoOfRangeEq_hom_fac] at hx
    rw [← SetLike.mem_coe, ← Scheme.toSpecΓ_preimage_basicOpen, TopologicalSpace.Opens.map_coe,
        Set.mem_preimage]
    refine Set.mem_of_subset_of_mem (Set.image_subset_iff.mpr ?_) hx
    change PrimeSpectrum.basicOpen _ ≤ PrimeSpectrum.basicOpen _
    simp only [CommRingCat.ofHom_comp, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
      RingHom.coe_comp, Function.comp_apply, HomogeneousLocalization.algebraMap_apply,
      HomogeneousLocalization.Away.val_mk, Localization.mk_eq_mk', IsLocalization.map_mk', map_pow,
      PrimeSpectrum.basicOpen_le_basicOpen_iff, IsLocalization.mk'_mem_iff]
    exact Ideal.pow_mem_of_mem _ (Ideal.le_radical (Ideal.mem_span_singleton_self _)) _ i.2.2.1
  · intro x hx
    let I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, r, hn, hr⟩
    obtain ⟨x, rfl⟩ : x ∈ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I).opensRange := by
      simpa [openCoverOfMapIrrelevantEqTop] using hx
    rw [← SetLike.mem_coe] -- TODO : mem version of TopologicalSpace.Opens.map_coe
    simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections]
    simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = IsLocalization.mk' (Localization.AtPrime P) y t

Tactic:
have : x.1 = y.1 * t.1.1⁻¹ * s.1.1 := by
    simpa [IsLocalization.lift_mk', Algebra.ofId_apply, H,
      Algebra.algebraMap_ofSubsemiring_apply, IsUnit.coe_liftRight] using congr($e * s.1.1)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = IsLocalization.mk' (Localization.AtPrime P) y t
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup W = ⊤
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : I
⊢ ⨆ j, ↑⟨i, j⟩.snd = W i

Tactic:
heq i,

Goal state after:
case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup W = ⊤
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : I
⊢ ⨆ j, ↑⟨i, j⟩.snd = sSup (κ i)
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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ((HomogeneousLocalization.mapId 𝒜 ⋯) (HomogeneousLocalization.mk x)).val =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.mk x).val

Tactic:
dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Localization.mk ↑x.num ⟨↑x.den, ⋯⟩ =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (Localization.mk ↑x.num ⟨↑x.den, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ l₀ ≫ f = commSq.i₂ ≫ Y'_to_Y

Tactic:
simp_all only [commSq']

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
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P Q).toGrothendieck X ↔ ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
rw [Pretopology.mem_toGrothendieck]

Goal state after:
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
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) ↔
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case right.add
σ : 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 x y : Away 𝒜 (x✝ i₀)
hx :
  x ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hy :
  y ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hhx : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) x) ≤ 1
hhy : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) y) ≤ 1
⊢ (valuation O K) (φ' ((awayMap 𝒜 ⋯ ⋯) x) + φ' ((awayMap 𝒜 ⋯ ⋯) y)) ≤ 1

Tactic:
exact ((valuation O K).map_add _ _).trans <| sup_le_iff.mpr ⟨hhx, hhy⟩

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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
Z : C
g : Z ⟶ W
hg : S.arrows g
⊢ Sieve Z

Tactic:
by
    letI str := Presieve.getFunctorPushforwardStructure hg.bindStruct.hg
    exact Sieve.pullback str.lift
      (Sieve.functorPushforward F (data.sieve₁₀ str.cover.1.choose str.cover.2.choose))

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

Goal state before:
pp: 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
p : ToType (Φ.presheafFiber.obj P)
⊢ ∃ X x z, (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z = p

Tactic:
obtain ⟨⟨X, x⟩, z, rfl⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget A)
      (colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P))) p
  exact ⟨X, x, z, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝¹ : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Φ.fiber.map f))

Tactic:
rw [← mono_iff_injective]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝¹ : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst✝ : Mono f
⊢ Mono (Φ.fiber.map f)
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
⊢ data.sieve f ∈ J₀ X₀

Tactic:
have := IsDenseSubsite.isCoverDense J₀ J F
  have := IsDenseSubsite.isLocallyFull J₀ J F
  rw [← functorPushforward_mem_iff J₀ J F]
  let 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 hπ.some.lift
          (Sieve.functorPushforward F (F.imageSieve (hπ.some.map ≫ p))))
  refine J.superset_covering ?_
    (J.bind_covering (J.pullback_stable f (data.toOneHypercover.mem₀)) (R := R)
    (fun W p hp ↦ J.bind_covering (F.is_cover_of_isCoverDense J W) ?_))
  · rintro W' _ ⟨W, _, p, hp, ⟨Y₀, a, b, hb, ⟨U, c, d, ⟨x₁, w₁⟩, fac⟩, rfl⟩, rfl⟩
    have hp' := Sieve.ofArrows.fac hp
    dsimp at hp'
    refine ⟨U, x₁, d, ⟨Sieve.ofArrows.i hp,
      F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp, ?_⟩, ?_⟩
    · rw [w₁, assoc, assoc, assoc, assoc, hp']
    · rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_assoc]
  · intro U π hπ
    apply J.pullback_stable
    apply functorPushforward_imageSieve_mem

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
| lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op

Tactic:
simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
| liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).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}, 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
    let E : PreZeroHypercover S := ⟨ι, X, f⟩
    have (i : E.I₀) : HasPullback g (E.f i) := (h i).hasPullback
    let F : PreZeroHypercover Y := ⟨_, _, p₁⟩
    let e : F ≅ E.pullback₁ g :=
      PreZeroHypercover.isoMk (Equiv.refl _) (fun i ↦ (h i).isoPullback)
    change F.presieve₀ ∈ _
    rw [F.presieve₀_mem_precoverage_iff, (P (X := Y)).prop_iff_of_iso e]
    refine h₂ _ _ ?_
    rwa [← E.presieve₀_mem_precoverage_iff]

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

Goal state before:
pp: case succ
σ : 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)
n✝ : ℕ
h : d j = n✝ + 1
⊢ ψ i₀ ^ (a * d i₀ + d i₀ * a * n✝) = ψ i₀ ^ (d i₀ * a * (n✝ + 1))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone transfiniteCompositions.{w, v, u}

Tactic:
intro W₁ W₂ h X Y f hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ transfiniteCompositions.{w, v, u} W₂ f