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

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ φ (f'.resultant (g₁' * g₂') f.natDegree (g₁.natDegree + g₂.natDegree)) =
    φ (f'.resultant g₁' f.natDegree g₁.natDegree) * φ (f'.resultant g₂' f.natDegree g₂.natDegree)

Tactic:
← natDegree_eq_natDegree e₁,

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ φ (f'.resultant (g₁' * g₂') f.natDegree (g₁'.natDegree + g₂.natDegree)) =
    φ (f'.resultant g₁' f.natDegree) * φ (f'.resultant g₂' f.natDegree g₂.natDegree)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [natDegree_scaleRoots, natDegree_scaleRoots]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
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
pq : ↥R[X]_m × ↥R[X]_n
⊢ f * ↑pq.2 + g * ↑pq.1 ∈ R[X]_(m + n)

Tactic:
obtain ⟨⟨p, hp⟩, ⟨q, hq⟩⟩ := pq

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2 + g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1 ∈ R[X]_(m + n)
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: 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))
⊢ IsCommMonObj G

Tactic:
have : IsProper γ.left := .of_comp _ (fst G G).left

Goal state after:
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 γ)
⊢ IsCommMonObj G
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := ⋯
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) := ⋯
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) := ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := ⋯
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
W₂ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := ⋯
⊢ (pullback.fst f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)) ↑⟨g { asIdeal := P', isPrime := w✝¹ }, ⋯⟩ =
    (IsAffineOpen.fromSpec hV) { asIdeal := Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P', isPrime := ⋯ }

Tactic:
simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base, g, reassoc_of% he₁]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: case hsnd
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ Smooth (Limits.pullback.snd f g)

Tactic:
let : GrpObj (Over.mk (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd

Goal state after:
case hsnd
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := AlgebraicClosure K
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom (algebraMap K Ω))
this : GrpObj (Over.mk (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd
⊢ Smooth (Limits.pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom

Tactic:
let 𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
    (Scheme.IsLocallyDirected.openCover _).pushforwardIso e.inv

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
apply surjective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
⊢ ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Subsingleton (Localization.AtPrime p ⊗[R] S)

Tactic:
apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Module.rank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 0
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ ((ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 r₃

Tactic:
dsimp only [rightAdjointSquare.vcomp]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ ((ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      ((α_ r₁ (𝟙 c) (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 c ≫
            (α_ (𝟙 d) r₂ (𝟙 c)).hom ≫
              𝟙 d ◁ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ (𝟙 d) (𝟙 d) r₃).inv) ⊗≫
        𝟙 r₃
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))
⊢ IsOpenImmersion.lift (𝒰.f (j i)) (f ↑⟨i, ⋯⟩) ⋯ ≫ 𝒰.f (j i) = f i

Tactic:
IsOpenImmersion.lift_fac

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))
⊢ f ↑⟨i, ⋯⟩ = f i
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_ofPred_eq]

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ (∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) →
    ∀ x ∈ t ∩ t', r ∈ x.asHomogeneousIdeal

Tactic:
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ (vanishingIdeal t).toIdeal
g : A
hg : g ∈ (vanishingIdeal t').toIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ z ∈ ⨆ i, basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f)

Tactic:
iSup,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ z ∈ sSup (Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv)) ((mateEquiv adj₂ adj₃) β) ⊗≫
        𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)

Tactic:
by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      bicategory

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

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ∀ i ∈ {x ∈ s | n x ≠ 0}, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩

Goal state after:
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
e : ∃ c, ↑c * (↑g.den * ↑f.num) = ↑c * (↑f.den * ↑g.num)
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (sectionInBasicOpen 𝒜 x f) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑g.den) x ⋯))
      (sectionInBasicOpen 𝒜 x g)

Tactic:
obtain ⟨⟨c, hc⟩, hc'⟩ := e

Goal state after:
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)
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (sectionInBasicOpen 𝒜 x f) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑g.den) x ⋯))
      (sectionInBasicOpen 𝒜 x g)
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case inr
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
max_lt : max₂ < j
⊢ (proj 𝒜 (i, j).1) x * (proj 𝒜 (i, j).2) y ∈ I

Tactic:
have notMem : j ∉ set₂ := fun h =>
            lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h)
          rw [set₂_eq] at notMem
          simp only [not_and, Classical.not_not, mem_filter] at notMem
          exact Ideal.mul_mem_left I _ (notMem H₃)

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
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx : IsUnit ((localRingHom f I J hIJ) x)
⊢ IsUnit x

Tactic:
rw [← isUnit_iff_isUnit_val] at hx ⊢
    rw [val_localRingHom] at hx
    exact IsLocalHom.map_nonunit _ hx

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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
have (U) (e : U = ⊤) : (basicOpen 𝒜 f).ι ≫ (Scheme.topIso _).inv ≫ (Scheme.isoOfEq _ e).inv =
      Scheme.homOfLE _ (le_top.trans_eq e.symm) := by
    simp only [← Category.assoc, Iso.comp_inv_eq]
    simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]

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
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).ι ≫
      (Proj 𝒜).topIso.inv ≫
        ((Proj 𝒜).isoOfEq ⋯).inv ≫
          (basicOpen 𝒜 1).toSpecΓ ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))
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
⊢ CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x = awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op

Tactic:
by
  ext a
  apply Subtype.ext
  ext ⟨i, hi⟩
  obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a
  simp only [homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
  erw [ProjectiveSpectrum.Proj.awayToSection_apply]
  rw [CommRingCat.hom_ofHom, val_awayMap_mk, Localization.mk_eq_mk', IsLocalization.map_mk',
    ← Localization.mk_eq_mk']
  refine Localization.mk_eq_mk_iff.mpr ?_
  rw [Localization.r_iff_exists]
  use 1
  simp [hx]
  ring

Goal state after: