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

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ModuleCat.Hom.hom
      (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g)) ≫
        ModuleCat.ofHom
          (IsLocalizedModule.lift (Submonoid.powers (unop g))
            (ModuleCat.Hom.hom
              (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
            (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)) =
    ModuleCat.Hom.hom
      (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f)) ≫
        ModuleCat.ofHom
            (IsLocalizedModule.lift (Submonoid.powers (unop f))
              (ModuleCat.Hom.hom
                (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
              (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
          (modulesSpecToSheaf.obj M).obj.map i.unop.hom.op)

Tactic:
ext x

Goal state after:
case h
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
x : ↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤))
⊢ (ModuleCat.Hom.hom
        (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g)) ≫
          ModuleCat.ofHom
            (IsLocalizedModule.lift (Submonoid.powers (unop g))
              (ModuleCat.Hom.hom
                (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
              (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)))
      x =
    (ModuleCat.Hom.hom
        (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f)) ≫
          ModuleCat.ofHom
              (IsLocalizedModule.lift (Submonoid.powers (unop f))
                (ModuleCat.Hom.hom
                  (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
                (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
            (modulesSpecToSheaf.obj M).obj.map i.unop.hom.op))
      x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers 1)
          (ModuleCat.Hom.hom (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen 1)))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

Tactic:
ext x

Goal state after:
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
x : ↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤))
⊢ (ModuleCat.Hom.hom
        (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
          ModuleCat.ofHom
            (IsLocalizedModule.lift (Submonoid.powers 1)
              (ModuleCat.Hom.hom (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen 1)))
              (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)))
      x =
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
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 (𝒜₊)
i : ℕ
s : A
hs : s ∈ 𝒜 i
⊢ awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ (f s)) ⋯ =
    CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ (f s)

Tactic:
ext x

Goal state after:
A B σ τ : Type u
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 (𝒜₊)
i : ℕ
s : A
hs : s ∈ 𝒜 i
x : ↑(CommRingCat.of (Away 𝒜 s))
⊢ (CommRingCat.Hom.hom (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ (f s)) ⋯)) x =
    (CommRingCat.Hom.hom (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ (f s))) x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
⊢ IsIso tilde.adjunction.unit

Tactic:
dsimp [tilde.adjunction]; infer_instance

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
inst✝¹ : IsLocalRing R
inst✝ : Nontrivial S
f : R →+* S
⊢ ↑f.range = ↑(map f { toSubring := ⊤, isLocalRing := ⋯ }).toSubring

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
K : Type u_3
inst✝² : Field K
inst✝¹ : IsLocalRing R
inst✝ : Nontrivial S
f : R →+* S
x : S
⊢ x ∈ ↑f.range ↔ x ∈ ↑(map f { toSubring := ⊤, isLocalRing := ⋯ }).toSubring
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
⊢ IsMax R.toLocalSubring

Tactic:
by
  intro S hS
  refine (LocalSubring.toSubring_injective (hS.1.antisymm fun x hx ↦ (R.2 x).elim id fun h ↦ ?_)).ge
  by_contra h'
  have hx0 : x ≠ 0 := by rintro rfl; exact h' R.zero_mem
  have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩
  obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)
  have : x' = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'
  exact h' (this ▸ x'.2)

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

Goal state before:
pp: case inl
K : Type u_3
inst✝¹ : Field K
R : Subring K
inst✝ : IsIntegrallyClosedIn (↥R) K
hxR : 0 ∉ R
⊢ ∃ V, R ≤ V.toSubring ∧ 0 ∉ V

Tactic:
exact (hxR R.zero_mem).elim

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

Goal state before:
pp: case pq
K : Type u_3
inst✝ : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
⊢ s ⊆ ↑V.toSubring ↔ Subring.ofClass (Subring.closure s) ≤ V.toSubring

Tactic:
exact Subring.closure_le.symm

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
⊢ awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv

Tactic:
by
  ext z
  apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr
  apply Proj.stalkIso'_germ

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

Goal state before:
pp: case exists_of_eq
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
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ HomogeneousLocalization.val
      (↑⟨HomogeneousLocalization.mk { deg := m * i, num := ⟨c ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }, ⋯⟩ *
        HomogeneousLocalization.mk y) =
    HomogeneousLocalization.val
      (↑⟨HomogeneousLocalization.mk { deg := m * i, num := ⟨c ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }, ⋯⟩ *
        HomogeneousLocalization.mk z)

Tactic:
simp only [val_mul, val_mk, mk_eq_mk', ← IsLocalization.mk'_mul, Submonoid.mk_mul_mk,
      IsLocalization.mk'_eq_iff_eq, mul_assoc]

Goal state after:
case exists_of_eq
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
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ (algebraMap A (Localization (Submonoid.powers f))) (f ^ i * (↑z.den * (c ^ m * ↑y.num))) =
    (algebraMap A (Localization (Submonoid.powers f))) (f ^ i * (↑y.den * (c ^ m * ↑z.num)))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
⊢ ⋯.HasLift

Tactic:
let S' : ValuativeCommSq f := ⟨S.R, S.K, S.i₁, S.i₂ ≫ pullback.fst f f ≫ f, hc⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
⊢ ⋯.HasLift
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 𝒜
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 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
⊢ IsClosedImmersion
    ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
          (toSpecZero 𝒜)).inv ≫
      snd (diagonal (toSpecZero 𝒜))
        ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
              (toSpecZero 𝒜)).f
          (i, j)))

Tactic:
← MorphismProperty.cancel_right_of_respectsIso (P := @IsClosedImmersion) _ e₁.hom,

Goal state after:
σ : 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 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
⊢ IsClosedImmersion
    (((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
            (toSpecZero 𝒜)).inv ≫
        snd (diagonal (toSpecZero 𝒜))
          ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                (toSpecZero 𝒜)).f
            (i, j))) ≫
      e₁.hom)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
n : ℕ
hn : (f * g i) ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t = 0
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0

Tactic:
rw [mul_pow, mul_comm, mul_smul, ← Scheme.Modules.map_smul_Spec] at hn

Goal state after:
case h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
n : ℕ
hn : g i ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
this : ∃ n, (f * g i) ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t = 0
⊢ ∃ n, (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0

Tactic:
obtain ⟨n, hn⟩ := this
        use n
        rw [mul_pow, mul_comm, mul_smul, ← Scheme.Modules.map_smul_Spec] at hn
        exact ((M.isSMulRegular_of_le_basicOpen le_rfl).pow n).right_eq_zero_of_smul hn

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

Goal state before:
pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
hx : (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0
⊢ ∃ n, f ^ n • x = 0

Tactic:
obtain ⟨n, hn⟩ := h.uniqueness _ _ _ hx

Goal state after:
case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
hx : (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0
n : ℕ
hn : f ^ n • x = 0
⊢ ∃ n, f ^ n • x = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (ConcreteCategory.hom iso.hom) ((ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t) =
    (ConcreteCategory.hom iso.hom) 0
⊢ f ^ n • t = 0

Tactic:
dsimp [iso, ψ] at this

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom)
        ((ConcreteCategory.hom a) f ^ n •
          (AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op)) t))) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom) 0)
⊢ f ^ n • t = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
⊢ SheafOfModules.IsQuasicoherent M ↔ IsIso M.fromTildeΓ

Tactic:
refine ⟨fun h ↦ inferInstance, fun h ↦ ?_⟩
  exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso
    (asIso <| M.fromTildeΓ) inferInstance

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

Goal state before:
pp: R : CommRingCat
⊢ (tilde.functor R).essImage = SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf

Tactic:
by
  refine le_antisymm ?_ ?_
  · intro M ⟨N, ⟨e⟩⟩
    exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso e
      (by dsimp; infer_instance)
  · intro M (h : M.IsQuasicoherent)
    exact ⟨((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)), ⟨asIso <| M.fromTildeΓ⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ toSheafify J ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)) ⋙ U) ≫
      sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom ≫
        ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    toSheafify J ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)) ⋙ U) ≫
      (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).hom ≫
        whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U

Tactic:
ext x

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x : Cᵒᵖ
⊢ (toSheafify J ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)) ⋙ U) ≫
          sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom ≫
            ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom).app
      x =
    (toSheafify J ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)) ⋙ U) ≫
          (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).hom ≫
            whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U).app
      x
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
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
⊢ (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)

Tactic:
ext x

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 ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x✝
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
x : Away 𝒜 ↑i₀
⊢ ((algebraMap O K).comp φ'') x = (φ'.comp (awayMap 𝒜 ⋯ ⋯)) x