mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⊆ (zeroLocus t)ᶜ
i : ι
⊢ comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i) ⁻¹' zeroLocus t = ∅

Tactic:
← Set.compl_univ_iff,

Goal state after:
ι : 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 ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i) ⁻¹' zeroLocus t)ᶜ = Set.univ
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 ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
rw [Scheme.Hom.opensRange_comp]

Goal state after:
ι : 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 ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : ι), ∃ j, Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f j))
⊢ ∃ a, pointsPi R X a = f

Tactic:
choose j hj using this

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
⊢ ∃ a, pointsPi R X a = f
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)

Tactic:
rw [(isClosed_zeroLocus _ _).closure_subset_iff]

Goal state after:
case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)
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✝ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
⊢ n • y.val = n • y.val

Tactic:
OreLocalization.nsmul_eq_nsmul

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
⊢ n • y.val = n • y.val
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)
⊢ overMap X.ringCatSheaf f ⋙ (overEquiv V).functor ≅ (overEquiv U).functor ⋙ restrictFunctor (X.homOfLE ⋯)

Tactic:
refine (SheafOfModules.pushforwardComp _ _) ≪≫ ?_ ≪≫ (SheafOfModules.pushforwardComp _ _).symm

Goal state after:
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)
⊢ SheafOfModules.pushforward
      (((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) ≅
    SheafOfModules.pushforward
      ({
          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)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos
ι : 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
⊢ 0 = f ^ (k' - k + k) • val z

Tactic:
pow_add,

Goal state after:
case pos
ι : 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
⊢ 0 = (f ^ (k' - k) * f ^ k) • val z
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 + k) • m), (algebraMap A (at Submonoid.powers f)) x = f ^ (k' - k + k) • val z

Tactic:
pow_add,

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 + k) • m), (algebraMap A (at Submonoid.powers f)) x = (f ^ (k' - k) * f ^ k) • val z
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
U : (Proj 𝒜).Opens
e : U = ⊤
⊢ (basicOpen 𝒜 f).ι = ((Proj 𝒜).homOfLE ⋯ ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ (Proj 𝒜).topIso.hom

Tactic:
simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]

Goal state after:
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 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ ↑1 *
      (↑(s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).2 *
        (s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).1) =
    ↑1 *
      (↑(s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).2 *
        (s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).1)

Tactic:
by simp; ring

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
S : CommRingCat
f : R ⟶ S
inst✝ : IsOpenImmersion (Spec.map f)
U : (Spec S).Opens
r : ↑R
x : ↑Γ(M.restrict (Spec.map f), U)
this :
  f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Opens.leTop U).op ≫ (Hom.appIso (Spec.map f) U).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Opens.leTop (Spec.map f ''ᵁ U)).op
⊢ (ConcreteCategory.hom
          (f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Opens.leTop U).op ≫ (Hom.appIso (Spec.map f) U).inv))
        r •
      (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x =
    (ConcreteCategory.hom ((ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Opens.leTop (Spec.map f ''ᵁ U)).op)) r •
      (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x

Tactic:
rw [this]

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

Goal state before:
pp: case refine_2.refine_3
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 : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(if n ≤ i then a * ↑(((decompose 𝒜) x) (i - n)) else 0) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩,
        den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
split_ifs with h
      · convert_to product ∈ q.1
        · dsimp [product]
          rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mul, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mk]
          · simp_rw [mul_pow]; rw [Localization.mk_mul]
            · congr; rw [← pow_add, Nat.add_sub_of_le h]
        · apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)
          rw [(_ : m • n = _)]
          · mem_tac
          · simp only [smul_eq_mul, mul_comm]
      · simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i

Goal state after:
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
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
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' =
    g i ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (ψ t')

Tactic:
← Scheme.Modules.map_smul_Spec

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
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
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (g i ^ n • ψ t')
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]
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ R.toSubring

Tactic:
rw [this]

Goal state after:
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]
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ (ofPrime S.toSubring Q).toSubring
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 : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
⊢ f ^ ((⨆ i, n i) - n i + n i) • s' i =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i) i)

Tactic:
pow_add,

Goal state after:
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 i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
⊢ (f ^ ((⨆ i, n i) - n i) * f ^ n i) • s' i =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i) i)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
s : Set K
⊢ ⨅ V, (↑V).toSubring = (integralClosure (↥(Subring.closure s)) K).toSubring

Tactic:
by
  refine .trans ?_ Subring.eq_iInf_of_isIntegrallyClosedIn.symm
  simp_rw [iInf_subtype]
  congr! with V
  have : IsIntegrallyClosedIn V.toSubring K := inferInstanceAs (IsIntegrallyClosedIn V K)
  rw [Subring.integralClosure_subring_le_iff]
  exact Subring.closure_le.symm

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 : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
m : ι → ι → ℕ
hm :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t j)
K : ℕ := ⨆ i, ⨆ j, m i j
i j : ι
this✝ : m i j ≤ K
this : K = K - m i j + m i j
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ (K - m i j + m i j) • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ (K - m i j + m i j) • t j)

Tactic:
pow_add,

Goal state after:
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)
m : ι → ι → ℕ
hm :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m i j • t j)
K : ℕ := ⨆ i, ⨆ j, m i j
i j : ι
this✝ : m i j ≤ K
this : K = K - m i j + m i j
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((f ^ (K - m i j) * f ^ m i j) • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((f ^ (K - m i j) * f ^ m i j) • t j)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
⊢ j * (d * (e + 1)) = n + (j * (d - 1)) • e

Tactic:
rw [this]

Goal state after:
case e'_4
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
⊢ j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e
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
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ R ∈ (overPretopology P S).toGrothendieck X

Tactic:
use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩

Goal state after:
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