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

Goal state before:
pp: case e'_2.e_a.h₀
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ ((pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom) ≫
      pullback.fst (Spec A ↘ Spec R) (Spec A ↘ Spec R) =
    (Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv) ≫
      pullback.fst (Spec A ↘ Spec R) (Spec A ↘ Spec R)

Tactic:
simp [AlgHom.toUnder, specOverSpec, over, OverClass.hom, h₁]

Goal state after:
case e'_2.e_a.h₀
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l

Tactic:
rw [← comp_τl, e.hom_inv_id, id_τl]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))

Tactic:
rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, (basicOpen i).carrier
⊢ V ⊆ (zeroLocus t)ᶜ

Tactic:
simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ f = g

Tactic:
have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
    (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using! congr_fun e i))
    (equalizer.ι f g) (by simp)

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (equalizer.ι f g)
⊢ f = g
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
neither_mem : (proj 𝒜 max₁) x ∉ I ∧ (proj 𝒜 max₂) y ∉ I
⊢ (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∉ I

Tactic:
intro _rid

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
neither_mem : (proj 𝒜 max₁) x ∉ I ∧ (proj 𝒜 max₂) y ∉ I
_rid : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
⊢ False
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case succ
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
ih : ↑(GradedMonoid.GMonoid.gnpow n c.den) ∈ x
⊢ ↑(GradedMonoid.GMonoid.gnpow (n + 1) c.den) ∈ x

Tactic:
simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem

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

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯ ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,
    Iso.hom_inv_id]
  simp

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

Goal state before:
pp: case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + k • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)

Tactic:
DirectSum.degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded _ hf) (hk.symm ▸ z.den_mem_deg) hfk

Goal state after:
case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case w.refine_2
ι : 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
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)

Tactic:
apply SetLike.mul_mem_graded hb'

Goal state after:
case w.refine_2
ι : 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
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
⊢ g ^ j ∈ 𝒜 (j • e)
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ∨
    HomogeneousLocalization.mk { deg := m * ny, num := ⟨(proj 𝒜 ny) y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
apply q.2.mem_or_mem

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } *
      HomogeneousLocalization.mk { deg := m * ny, num := ⟨(proj 𝒜 ny) y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ Function.Injective ⇑(ConcreteCategory.hom (toSpec 𝒜 f))

Tactic:
intro x₁

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x₁ : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ ∀ ⦃a₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace⦄,
    (ConcreteCategory.hom (toSpec 𝒜 f)) x₁ = (ConcreteCategory.hom (toSpec 𝒜 f)) a₂ → x₁ = a₂
Module: Mathlib.RingTheory.Valuation.LocalSubring

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

Tactic:
have : IsIntegrallyClosedIn V.toSubring K := inferInstanceAs (IsIntegrallyClosedIn V K)

Goal state after:
case pq
K : Type u_3
inst✝ : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
⊢ s ⊆ ↑V.toSubring ↔ (integralClosure (↥(Subring.closure s)) K).toSubring ≤ V.toSubring
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
⊢ ∃ a, (g.rangeRestrict.comp f) a = ⟨g x, ⋯⟩

Tactic:
obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : (algebraMap R K) y = g x
⊢ ∃ a, (g.rangeRestrict.comp f) a = ⟨g x, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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 • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj).op))
        ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0

Tactic:
← ht j,

Goal state after:
case refine_1
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 • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj).op)) (f ^ N • s' j) =
    0
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
⊢ LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    (specStalkEquiv 𝒜 f x f_deg hm).hom ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv

Tactic:
by
  refine CommRingCat.hom_ext <|
    IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).base x).asIdeal.primeCompl
      (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) <| ?_
  ext a
  refine congr($(toStalk_stalkMap_toSpec 𝒜 f x) _).trans ?_
  rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]; rfl

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

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
rintro ⟨U, h, g, ⟨k⟩, hcomp⟩

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Over S
k : 𝒰.I₀
h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ (𝒰.X k).asOver S
hcomp : h ≫ Hom.asOver (𝒰.f k) S = Over.homMk f ⋯
⊢ ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
rintro ⟨U, h, g, ⟨k⟩, hcomp⟩

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case right
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := ⋯
this : Cover.Over S 𝒰 := ⋯
⊢ 𝒰.toPresieveOver ≤ R.arrows

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff]

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overGrothendieckTopology P S) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
overGrothendieckTopology_eq_toGrothendieck_overPretopology

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
e : Arrow.mk (CommRingCat.ofHom (algebraMap S.R S.K)) ≅
  Arrow.mk (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))) :=
  arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom (algebraMap S.R S.K))
P : MorphismProperty CommRingCat :=
  RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f).RespectsIso
⊢ P (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))))

Tactic:
← MorphismProperty.arrow_mk_iso_iff (P := P) e

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
e : Arrow.mk (CommRingCat.ofHom (algebraMap S.R S.K)) ≅
  Arrow.mk (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))) :=
  arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom (algebraMap S.R S.K))
P : MorphismProperty CommRingCat :=
  RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f).RespectsIso
⊢ P (CommRingCat.ofHom (algebraMap S.R S.K))
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
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
⊢ J.W.IsInvertedBy Φ.presheafFiber

Tactic:
intro P

Goal state after:
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
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ A
⊢ ∀ ⦃Y : Cᵒᵖ ⥤ A⦄ (f : P ⟶ Y), J.W f → IsIso (Φ.presheafFiber.map f)