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

Goal state before:
pp: case h1
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite

pp: case h2
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat

pp: case hy
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ x✝ = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((Spec R).isoSpec.hom x✝)

Tactic:
· exact .comp (.of_surjective _ (ConcreteCategory.bijective_of_isIso _).surjective) hf₁

Goal state after:
case h2
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat

case hy
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ x✝ = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((Spec R).isoSpec.hom x✝)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ finrank (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x

Tactic:
by
  rw [finrank_SpecMap_eq_finrank]
  · simp
  · simpa [RingHom.finite_algebraMap]
  · simpa [RingHom.flat_algebraMap_iff]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ↑((⨆ p, ↑p.length) + 1) ≤ ↑(⨆ p, ↑p.length)

Tactic:
ENat.iSup_add,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ↑(⨆ i, ↑i.length + 1) ≤ ↑(⨆ p, ↑p.length)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ x ∣ a * x

Tactic:
exact Dvd.intro_left (algebraMap R R a) rfl

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
⊢ x ∈ nonZeroDivisors R

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ x ∈ nonZeroDivisors R

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsNoetherianRing R
inst✝⁷ : KrullDimLE 1 R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S R K
a : S
ha : (algebraMap S R) a ≠ 0
f : K
j : ¬f = 0
⊢ 1 ≤ (ordFrac R) ((algebraMap S K) a)

Tactic:
simp [IsScalarTower.algebraMap_eq S R K, ordFrac_ge_one_of_ne_zero ha]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ (f ≫ e.hom) ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R

Tactic:
by rwa [Category.assoc]

Goal state after:
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₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α

Tactic:
simpa only [Equiv.apply_symm_apply] using this

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

Goal state before:
pp: 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
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ f x ∈ f ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
by simpa

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

Goal state before:
pp: X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁵ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝⁴ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝³ : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝² :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝¹ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : TopologicalSpace.Opens ↥↑V
this : U.ι ''ᵁ X.homOfLE ⋯ ''ᵁ W = V.ι ''ᵁ W
⊢ ((Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).obj W).left =
    (((Opens.overEquivalence V).symm.functor ⋙ Over.map f).obj W).left

Tactic:
by simpa

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 𝒜
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
e : embedding 𝒜 P x = embedding 𝒜 P y
⊢ (Setoid.ker (embedding ℬ Q)) { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }
    { deg := y.deg, num := ⟨g ↑y.num, ⋯⟩, den := ⟨g ↑y.den, ⋯⟩, den_mem := ⋯ }

Tactic:
apply_fun IsLocalization.map (Localization Q) g.toRingHom comap_le at e

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 𝒜
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
e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (Setoid.ker (embedding ℬ Q)) { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }
    { deg := y.deg, num := ⟨g ↑y.num, ⋯⟩, den := ⟨g ↑y.den, ⋯⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁵ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝⁴ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝³ : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝² :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝¹ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
this :
  (ConcreteCategory.hom (X.presheaf.map ?m.460)) x =
    (ConcreteCategory.hom (Hom.appIso (X.homOfLE ⋯) (Opposite.unop W)).inv) x
⊢ (RingCat.Hom.hom
        (((((Opens.overPullbackSheafEquivOver V).app X.ringCatSheaf).inv ≫
                  ((Opens.overEquivalence V).symm.functor.sheafPushforwardContinuous RingCat
                        (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology ↥X).over V)).map
                    (Sheaf.pushforwardOverMapIso X.ringCatSheaf f).inv) ≫
                (Functor.sheafPushforwardContinuousNatTrans
                      (NatIso.ofComponents (fun W ↦ Over.isoMk (eqToIso ⋯) ⋯) ⋯).hom RingCat
                      (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology ↥X).over U)).app
                  (Sheaf.over X.ringCatSheaf U)).hom.app
          W))
      x =
    (RingCat.Hom.hom
        (({
                  hom :=
                    Functor.whiskerRight
                      { app := fun U_1 ↦ (Hom.appIso (X.homOfLE ⋯) (Opposite.unop U_1)).inv, naturality := ⋯ }
                      (forget₂ CommRingCat RingCat) } ≫
                ((Hom.opensFunctor (X.homOfLE ⋯)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥↑V)
                      (Opens.grothendieckTopology ↥U)).map
                  ((Opens.overPullbackSheafEquivOver U).app X.ringCatSheaf).inv).hom.app
          W))
      x

Tactic:
by simpa

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

Goal state before:
pp: case pos
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : n = 0
⊢ f i - ↑(((DirectSum.decompose 𝒜) (f i)) 0) ∈ Ideal.span (Set.range f)

Tactic:
rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
      exact zero_mem _

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

Goal state before:
pp: case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map
      (((↑(basicOpen 𝒜 f)).toSpecΓ ≫ Spec.map (basicOpen 𝒜 f).topIso.inv) ≫ Spec.map (awayToSection 𝒜 f)) =
    ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f)) ≫
      Spec.toLocallyRingedSpace.map (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f).op

Tactic:
simp only [Category.assoc, ← Spec.map_comp]

Goal state after:
case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map
      ((↑(basicOpen 𝒜 f)).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv)) =
    ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f)) ≫
      Spec.toLocallyRingedSpace.map (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f).op
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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (basicOpenIsoSpec 𝒜 x ⋯ ⋯).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι =
    (basicOpen 𝒜 x).ι

Tactic:
basicOpenIsoSpec_hom,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ basicOpenToSpec 𝒜 x ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι =
    (basicOpen 𝒜 x).ι
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e_a
σ : 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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ ((IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp (algebraMap A (Localization.Away x.snd.fst))).comp
      (algebraMap (↥(𝒜 0)) A) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))

Tactic:
IsLocalization.map_comp,

Goal state after:
case e_a
σ : 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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ ((algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp f).comp (algebraMap (↥(𝒜 0)) A) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
⊢ Algebra.adjoin (↥(𝒜 0)) (Set.range Subtype.val) = ⊤

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
⊢ ∀ x_1 ∈ {x}, IsIntegral (↥R.toSubring) x_1

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
⊢ ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits

Tactic:
by
  have ⟨M, hM, le⟩ := I.exists_le_maximal hI
  have ⟨V, hV⟩ := (LocalSubring.ofPrime A M).exists_le_valuationSubring
  refine ⟨V, (LocalSubring.le_ofPrime ..).trans hV.1, ?_⟩
  rw [← V.image_maximalIdeal]
  refine .trans ?_ (Set.image_mono <| ((local_hom_TFAE _).out 0 2).mp hV.2)
  rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M, map_map]
  refine .trans ?_ (Set.image_mono <| map_mono le)
  rintro _ ⟨a, ha, rfl⟩
  exact ⟨_, mem_map_of_mem _ ha, rfl⟩

Goal state after:
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, (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = f ^ n • s

Tactic:
obtain ⟨N, t, ht⟩ : ∃ (N : ℕ) (t : ∀ i, Γ(M, basicOpen (g i))),
        ∀ i, f ^ N • s' i = M.presheaf.map (homOfLE (basicOpen_mul_le_right f (g i))).op (t i) := 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:
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)
⊢ ∃ n t, (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = f ^ n • s
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
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
⊢ R ∈ (overPretopology P S).toGrothendieck X

Tactic:
let (i : 𝒰.I₀) : (𝒰.X i).Over S := { hom := 𝒰.f i ≫ X.hom }

Goal state after:
case mp
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 := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
⊢ R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : 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 ι
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
let ψ (i : ι) : ValueGroup O K :=
    valuation O K ((φ (Away.isLocalizationElem (hxdi j) (hxdi i))) ^ ∏ k ∈ Finset.univ.erase i, d k)

Goal state after:
case intro
σ : 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)
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
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
hT : IsTerminal T
x✝¹ x✝ : Φ.fiber.obj U
this : Unique (Φ.fiber.obj T)
⊢ (ConcreteCategory.hom (Φ.fiber.map f)) x✝¹ = (ConcreteCategory.hom (Φ.fiber.map f)) x✝

Tactic:
subsingleton

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

Goal state before:
pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
this✝ : Cover.Over X V := { over := fun w ↦ { hom := (Z (i w)).hom }, isOver_map := ⋯ }
this : ∀ (w : ↥W.left), Etale (V.X w ↘ X)
Y : MorphismProperty.Over @Etale ⊤ X
w : V.I₀
⊢ (Sieve.ofArrows Z f).arrows (Hom.asOverProp (V.f w) X)

Tactic:
refine ⟨_, 𝟙 _, _, ⟨i w⟩, by cat_disch⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
R : Presieve S
x✝ : ∃ 𝒰, QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
𝒰 : Cover (precoverage P) S
left✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
h : R = 𝒰.presieve₀
⊢ 𝒰.presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
by simpa

Goal state after: