mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ + x✝).2 + g * ↑(x✝¹ + x✝).1, ⋯⟩ = ⟨f * ↑x✝¹.2 + g * ↑x✝¹.1, ⋯⟩ + ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
by ext1; dsimp; ring

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ η ▷ G ≫ commutator G = toUnit (𝟙_ C ⊗ G) ≫ η

Tactic:
simp [commutator, comp_mul, comp_inv, one_eq_one]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ G ◁ η ≫ commutator G = toUnit (G ⊗ 𝟙_ C) ≫ η

Tactic:
simp [commutator, comp_mul, comp_inv, one_eq_one]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι

Tactic:
rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]
        simpa [← Scheme.Hom.opensRange_comp, ι, e, Scheme.Hom.normalizationCoprodIso,
          Set.range_comp] using Set.subset_preimage_image _ _

Goal state after:
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
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
⊢ fTn ((toNormalization (pullback.snd f fT)) ↑v) = (toNormalization f) x

Tactic:
simp only [← hv₂, ← Scheme.Hom.comp_apply]

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
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
⊢ (toNormalization (pullback.snd f fT) ≫ fTn) ↑v = (pullback.fst f fT ≫ toNormalization f) ↑v
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
⊢ IsClosed {y} → (Over.Hom.left (GrpObj.commutator G)) y = (Over.Hom.left (toUnit (G ⊗ G) ≫ η)) y

Tactic:
hy

Goal state after:
case refine_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
⊢ (Over.Hom.left (GrpObj.commutator G)) y = (Over.Hom.left (toUnit (G ⊗ G) ≫ η)) y
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this✝ : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
⊢ Module.Projective S Ω[S⁄R]

Tactic:
have : Module.Flat (S ⊗[R] T) ((S ⊗[R] T) ⊗[S] Ω[S⁄R]) := .of_linearEquiv e'

Goal state after:
case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this✝¹ : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this✝ : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
this : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
x y : S ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x
hy : (P.tensorCotangentSpace T) (t ⊗ₜ[R] y) = t • (CotangentSpace.map (toBaseChange T)) y
⊢ t • (CotangentSpace.map (toBaseChange T)) x + (P.tensorCotangentSpace T) (t ⊗ₜ[R] y) =
    t • (CotangentSpace.map (toBaseChange T)) x + t • (CotangentSpace.map (toBaseChange T)) y

Tactic:
hy

Goal state after:
case add
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
x y : S ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x
hy : (P.tensorCotangentSpace T) (t ⊗ₜ[R] y) = t • (CotangentSpace.map (toBaseChange T)) y
⊢ t • (CotangentSpace.map (toBaseChange T)) x + t • (CotangentSpace.map (toBaseChange T)) y =
    t • (CotangentSpace.map (toBaseChange T)) x + t • (CotangentSpace.map (toBaseChange T)) y
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
⊢ finrank f (g t) = IsAffine.finrank (pullback.snd f g) t

Tactic:
let i := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
  obtain ⟨y, hyl, hyr⟩ := Scheme.Pullback.exists_preimage_pullback
    (S.affineOpenCover.covers <| g t).choose t (S.affineOpenCover.covers <| g t).choose_spec
  obtain ⟨R, u, hu, z, rfl⟩ := (pullback i g).exists_Spec_apply_eq y
  trans IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd _ _)) z
  · refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm
    · exact pullback.map _ _ _ _ (pullback.fst f g) (u ≫ pullback.fst _ _) g
        pullback.condition.symm (by simp [← pullback.condition]; rfl)
    · exact u ≫ pullback.fst _ _
    · apply IsPullback.map_fst_comp_fst_snd_comp_fst
    · exact hyl
  · simp_rw [← hyr]
    exact IsAffine.finrank_snd (pullback.snd f g) (u ≫ pullback.snd _ _) z

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
⊢ ↑(⨆ i, ↑i.length + 1) ≤ ↑(⨆ p, ↑p.length)

Tactic:
WithBot.coe_le_coe,

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.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
r : R
hr : r ∈ R⁰
hr' : f r = 0
⊢ ringKrullDim S + 1 ≤ ringKrullDim R

Tactic:
refine le_trans ?_ (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
r : R
hr : r ∈ R⁰
hr' : f r = 0
⊢ ringKrullDim S + 1 ≤ ringKrullDim (R ⧸ Ideal.span {r}) + 1
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
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map
        (CommRingCat.ofHom
          ((Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i)))) ≫
      inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i

Tactic:
CommRingCat.ofHom_comp,

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)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map
        (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i)) ≫
          CommRingCat.ofHom (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩)) ≫
      inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i
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 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑g.den * ↑f.num) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑f.den * ↑g.num)

Tactic:
rw [← map_mul, ← map_mul, hc']

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 𝒜
x : Submonoid A
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (↑c1.num ^ n) ⟨↑c1.den ^ n, ⋯⟩ = Localization.mk (↑c2.num ^ n) ⟨↑c2.den ^ n, ⋯⟩

Tactic:
convert! congr_arg (fun z : at x => z ^ n) h <;> rw [Localization.mk_pow]

Goal state after:
case e'_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 𝒜
x : Submonoid A
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (↑c1.num ^ n) ⟨↑c1.den ^ n, ⋯⟩ = Localization.mk (↑c1.num ^ n) (⟨↑c1.den, ⋯⟩ ^ n)

case e'_3
ι : 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 𝒜
x : Submonoid A
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (↑c2.num ^ n) ⟨↑c2.den ^ n, ⋯⟩ = Localization.mk (↑c2.num ^ n) (⟨↑c2.den, ⋯⟩ ^ n)
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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
r : ↥(𝒜 0)
⊢ (algebraMap (↥(𝒜 0)) A) r - (GradedRing.projZeroRingHom 𝒜) ((algebraMap (↥(𝒜 0)) A) r) = 0

Tactic:
rw [sub_eq_zero]

Goal state after:
case e'_5
σ : 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
r : ↥(𝒜 0)
⊢ (algebraMap (↥(𝒜 0)) A) r = (GradedRing.projZeroRingHom 𝒜) ((algebraMap (↥(𝒜 0)) A) r)
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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ val
      (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x))
            (mk { deg := n, num := a, den := ⟨(fun x ↦ f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            (mk { deg := n, num := a, den := ⟨(fun x ↦ f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩)

Tactic:
simp only [homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 x))
            ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
              (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case 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
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 := ⋯ }
⊢ ∑ i ∈ range (m + m + 1), g i ∈ q.asIdeal

Tactic:
refine q.1.sum_mem fun j _ => nsmul_mem ?_ _; split_ifs
    exacts [q.1.zero_mem, q.1.mul_mem_left _ (hb i), q.1.mul_mem_right _ (ha i)]

Goal state after:
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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
x : ↥X
hx : x ∈ X.basicOpen (f r)
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
⊢ x ∈ Scheme.Hom.opensRange ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I)

Tactic:
by
      simpa [openCoverOfMapIrrelevantEqTop] using hx

Goal state after:
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 (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst))).comp
      (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 (Submonoid.powers x.snd.fst))) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))

Tactic:
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ A,
    ← RingHom.comp_assoc, IsLocalization.map_comp, RingHom.comp_assoc]

Goal state after:
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
V : ValuationSubring K
⊢ IsIntegrallyClosed ↥V.toSubring

Tactic:
by
  rw [← V.integer_valuation]; infer_instance

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

Goal state before:
pp: case refine_1.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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i j : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯ ≫ ⋯.hom).op)) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯ ≫ ⋯.hom).op)) (f ^ K • t j)

Tactic:
eqToHom_comp_homOfLE

Goal state after:
case refine_1.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)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i j : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)