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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
let e : (pullback.snd f fT).normalization ≅ V ⨿ (W.ι ≫ pullback.snd f fT).normalization :=
      (Scheme.Hom.normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
        coprod.mapIso (asIso (V.ι ≫ pullback.snd f fT).toNormalization).symm (.refl _)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
⊢ opensRange (toNormalization f ∣_ V y) ⊓ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r =
    (toNormalization f ∣_ V y) ''ᵁ (toNormalization f ∣_ V y ≫ (V y).ι) ⁻¹ᵁ (normalization f).basicOpen r

Tactic:
Scheme.Hom.comp_preimage,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
⊢ opensRange (toNormalization f ∣_ V y) ⊓ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r =
    (toNormalization f ∣_ V y) ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource (@Flat ⊓ MorphismProperty.diagonal @Flat)
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@Flat ⊓ MorphismProperty.diagonal @Flat)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
    by simpa only [Equiv.symm_apply_apply] using this
  infer_instance

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

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ ↑(basicOpen 𝒜 f) ⊆ U

Tactic:
← Set.compl_subset_compl,

Goal state after:
case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ Uᶜ ⊆ (↑(basicOpen 𝒜 f))ᶜ
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
x : ↥(unop U)
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal
hy :
  ∀ (x : ↥V),
    (fun x ↦ a (i x)) x = HomogeneousLocalization.mk { deg := j, num := ⟨r, r_mem⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
y : ↥V
⊢ (fun x ↦ (-a) (i x)) y = HomogeneousLocalization.mk { deg := j, num := ⟨-r, ⋯⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }

Tactic:
simp only [ext_iff_val, val_mk] at hy

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
x : ↥(unop U)
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
m : ↑x ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal
y : ↥V
hy : ∀ (x : ↥V), val (a (i x)) = Localization.mk r ⟨s, ⋯⟩
⊢ (fun x ↦ (-a) (i x)) y = HomogeneousLocalization.mk { deg := j, num := ⟨-r, ⋯⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case a
ι : 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
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
exact sInf_le_sInf fun J => And.right

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

Goal state before:
pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ {
          hom :=
            Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
              (forget₂ CommRingCat RingCat) }.hom ≫
      (Hom.opensFunctor f).op.whiskerLeft (Hom.toRingCatSheafHom f).hom ≫
        Functor.whiskerRight (NatTrans.op ⋯.adjunction.unit) X.ringCatSheaf.obj =
    𝟙 X.ringCatSheaf.obj

Tactic:
ext U x
    have : (f.appIso U.unop).inv ≫ f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq U.unop).symm).op = 𝟙 _ := by
      rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]; rfl
    exact congr($this x)

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 𝒜
𝔭 : 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)
this : ↑f.num ∉ 𝔭
⊢ mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this } = 1

Tactic:
rw [← mk_mul, ext_iff_val, val_mk]

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)
this : ↑f.num ∉ 𝔭
⊢ Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num
      ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ =
    val 1
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
a : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (val a)

Tactic:
by
  rw [val_awayMap_eq_aux]
  rfl

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

Goal state before:
pp: case pos.e_a.e_x
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m - j) * ↑(((decompose 𝒜) b) i) ^ m

Tactic:
rw [mul_assoc, ← pow_add, add_comm (m - j), Nat.add_sub_assoc h1]

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

Goal state before:
pp: R : CommRingCat
M N P : ModuleCat ↑R
f : M ⟶ N
g : N ⟶ P
⊢ tilde.map (f ≫ g) = tilde.map f ≫ tilde.map g

Tactic:
by
  ext p x
  exact Subtype.ext (funext
    fun y ↦ DFunLike.congr_fun (IsLocalizedModule.map_comp' y.1.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl P) _ _) _)

Goal state after:
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 (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom
            ((toSheafedSpace ℬ).presheaf.germ
              ((Opens.map (sheafedSpaceMap f hf).hom.base).obj (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)) p ⋯))
          ((ConcreteCategory.hom
              ((sheafedSpaceMap f hf).hom.c.app (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))

Tactic:
germ_map_sectionInBasicOpen

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 (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
          (sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c))))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
⊢ SheafOfModules.Presentation (tilde M)

Tactic:
by
  haveI H₁ : Function.Exact
      (ModuleCat.ofHom (Finsupp.linearCombination (α := t) R (↑)))
      (ModuleCat.ofHom (Finsupp.linearCombination (α := s) (M := M) R (↑))) :=
    (LinearMap.exact_iff.mpr (by simp [Finsupp.range_linearCombination, ht]))
  refine SheafOfModules.presentationOfIsCokernelFree.{u}
      ((tildeFinsupp t).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination R (↑))) ≫
        (tildeFinsupp s).hom) ((tildeFinsupp s).inv ≫
          tilde.map (ModuleCat.ofHom (Finsupp.linearCombination R (↑)))) (by
    simp only [Category.assoc, Iso.hom_inv_id_assoc, Preadditive.IsIso.comp_left_eq_zero]
    rw [← tilde.map_comp, ← ModuleCat.ofHom_comp]
    convert! tilde.map_zero
    exact congr(ModuleCat.ofHom $(H₁.linearMap_comp_eq_zero))) ?_
  letI h₁ := ModuleCat.isColimitCokernelCofork _ _ H₁
    (by simp [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hs])
  refine IsCokernel.ofIso _ (CokernelCofork.mapIsColimit _ h₁ (tilde.functor R)) _ (tildeFinsupp t)
    (tildeFinsupp s) (.refl _) (by simp) (by simp)

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

Goal state before:
pp: case refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ { toSubring := ⨆ i, (↑i).toSubring, isLocalRing := ⋯ }.toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (fun x ↦ ↑x) ⟨A, hA⟩ ≤ (fun x ↦ ↑x) C
hCB : (fun x ↦ ↑x) B ≤ (fun x ↦ ↑x) C
⊢ IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)

Tactic:
exact isUnit_iff_exists_inv.mpr ⟨⟨b, hCB.1 hbB⟩, Subtype.ext congr(($e).1)⟩

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 : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)

Tactic:
by
      have (i : ι) : ∃ (n : ℕ) (t : Γ(M, basicOpen (g i))),
          f ^ n • s' i = M.presheaf.map (homOfLE (hfgi i)).op t := by
        obtain ⟨n, t', ht'⟩ := (h₁ i).existence (f * g i) (hfgi i) (s' i)
        rw [mul_pow, mul_smul, smul_comm] at ht'
        obtain ⟨ψ, hψ⟩ := IsUnit.exists_right_inv (hug i n)
        use n, ψ t'
        apply (M.isSMulRegular_of_le_basicOpen (basicOpen_mul_le_right f (g i))).pow n
        dsimp
        rw [← ht', ← Scheme.Modules.map_smul_Spec]
        congr 1
        exact congr($hψ t').symm
      choose n t' ht' using this
      have (i : ι) : n i ≤ ⨆ i, n i := le_ciSup (Finite.bddAbove_range _) _
      have hN (i : ι) : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by grind
      refine ⟨⨆ i, n i, fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i, fun i ↦ ?_⟩
      conv_lhs => rw [hN i]
      rw [pow_add, mul_smul, ht', M.map_smul_Spec]

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ PrimeSpectrum.comap
      ((CommRingCat.Hom.hom ((«Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)).comp
        (CommRingCat.Hom.hom (CommRingCat.ofHom (mapId 𝒜 ⋯))))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
PrimeSpectrum.comap_comp

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
⊢ (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (mapId 𝒜 ⋯))) ∘
        PrimeSpectrum.comap
          (CommRingCat.Hom.hom ((«Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ Existence = (topologically @SpecializingMap).universally

Tactic:
by
  ext
  constructor
  · intro _
    apply MorphismProperty.universally_mono
    · apply specializingMap
    · rwa [MorphismProperty.IsStableUnderBaseChange.universally_eq]
  · apply of_specializingMap

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
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)
⊢ LocallyOfFiniteType (toSpecZero 𝒜)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
    (Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx))]

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
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), LocallyOfFiniteType ((basicOpen 𝒜 ↑i).ι ≫ toSpecZero 𝒜)
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₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
⊢ data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W

Tactic:
have hS : S ∈ J W := by
    apply J.bind_covering
    · apply is_cover_of_isCoverDense
    · intro Y f hf
      apply J.pullback_stable
      rw [Functor.functorPushforward_mem_iff J₀]
      apply J₀.intersection_covering
      all_goals apply IsDenseSubsite.imageSieve_mem J₀ J

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
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₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
⊢ data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W