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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ toNormalization f ≫
      normalizationDesc f
          ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
            coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
          (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    toNormalization f ≫ 𝟙 (normalization f)

Tactic:
← cancel_epi (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
      toNormalization f ≫
        normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
          coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : f = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
· simp [hf0]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
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))
⊢ IsCommMonObj G

Tactic:
have : Surjective (fst G G).left := by dsimp; infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
hV'W : toNormalization f ⁻¹ᵁ V' = W
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y

Tactic:
obtain ⟨f₁, f₂, e, hxf⟩ := exists_basicOpen_le_affine_inter (hU.preimage f.fromNormalization)
      hV' (f.toNormalization x) ⟨by simpa [← Scheme.Hom.comp_apply], hV'W.ge hxW⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
hV'W : toNormalization f ⁻¹ᵁ V' = W
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
f₁ : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
f₂ : ↑Γ(normalization f, V')
e : (normalization f).basicOpen f₁ = (normalization f).basicOpen f₂
hxf : (toNormalization f) x ∈ (normalization f).basicOpen f₁
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
this : Ideal.map (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (algebraMap R S) I) ⋯
⊢ Module.Finite R ↥I

Tactic:
have : Module.Finite S (S ⊗[R] ↥I) := by
    rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
this✝ : Ideal.map (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (algebraMap R S) I) ⋯
this : Module.Finite S (S ⊗[R] ↥I)
⊢ Module.Finite R ↥I
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsFinite x✝ ↔ (@IsProper ⊓ @LocallyQuasiFinite) x✝

Tactic:
exact IsFinite.iff_isProper_and_locallyQuasiFinite ..

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: 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✝ : Etale T (T ⊗[R] S)
⊢ Etale R S

Tactic:
by
  rw [Etale.iff_formallyUnramified_and_smooth]
  exact ⟨.of_formallyUnramified_tensorProduct_of_faithfullyFlat T,
    .of_smooth_tensorProduct_of_faithfullyFlat T⟩

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

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫
      (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).inv ≫
        pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))

Tactic:
pullbackSymmetry_inv_comp_snd

Goal state after:
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫ pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: 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)
⊢ finrank (Spec.map f) x✝ = (CommRingCat.Hom.hom f).finrank x✝

Tactic:
finrank_eq_of_isAffine,

Goal state after:
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)
⊢ IsAffine.finrank (Spec.map f) x✝ = (CommRingCat.Hom.hom f).finrank x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (algebraMap p.ResidueField (p.Fiber ↑S)).Smooth

Tactic:
← CommRingCat.hom_ofHom (algebraMap p.ResidueField (p.Fiber ↑S)),

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap p.ResidueField (p.Fiber ↑S)))).Smooth
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n + 1 ≤ ringKrullDim R + (↑n + 1)

Tactic:
exact WithBot.le_add_self Order.bot_lt_krullDim.ne' _

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
⊢ IsUnit x ↔ (ordFrac R) ((algebraMap R K) x) = 1

Tactic:
by
  simp [ordFrac_eq_valuation_inv, IsDiscreteValuationRing.maximalIdeal]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
rw [adj₁.right_triangle]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj ((Adjunction.id a).comp adj')) ((λ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (ρ_ r').inv

Tactic:
simp only [conjugateEquiv_apply, mateEquiv_id_comp_right,
    id_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (ρ_ r).inv ≫
      (mateEquiv adj adj') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
        (ρ_ (𝟙 b ≫ r')).inv ≫ (α_ (𝟙 b) r' (𝟙 a)).hom ≫ (λ_ (r' ≫ 𝟙 a)).hom =
    (ρ_ r).inv ≫ (mateEquiv adj adj') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫ (λ_ r').hom ≫ (ρ_ r').inv
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
⊢ Function.Surjective (pointsPi R X)

Tactic:
intro f
  let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
  have (i : _) : ∃ j, Set.range (f i) ⊆ (𝒰.f j).opensRange := by
    refine ⟨𝒰.idx ((f i) (IsLocalRing.closedPoint (R i))), ?_⟩
    rintro _ ⟨x, rfl⟩
    exact ((IsLocalRing.specializes_closedPoint x).map (f i).continuous).mem_open
      (𝒰.f _).opensRange.2 (𝒰.covers _)
  choose j hj using this
  have (j₀ : _) := pointsPi_surjective_of_isAffine (ι := { i // j i = j₀ }) (R ·) (𝒰.X j₀)
    (fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f i.1) (by rcases i with ⟨i, rfl⟩; exact hj i))
  choose g hg using this
  simp_rw [funext_iff, pointsPi] at hg
  let R' (j₀) := CommRingCat.of (Π i : { i // j i = j₀ }, R i)
  let e : (Π i, R i) ≃+* Π j₀, R' j₀ :=
  { toFun f _ i := f i
    invFun f i := f _ ⟨i, rfl⟩
    right_inv _ := funext₂ fun j₀ i ↦ by rcases i with ⟨i, rfl⟩; rfl
    map_mul' _ _ := rfl
    map_add' _ _ := rfl }
  refine ⟨Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫
    Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀, ?_⟩
  ext i : 1
  have : (Pi.evalRingHom (R ·) i).comp e.symm.toRingHom =
    (Pi.evalRingHom _ ⟨i, rfl⟩).comp (Pi.evalRingHom (R' ·) (j i)) := rfl
  rw [pointsPi, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, this, CommRingCat.ofHom_comp,
    Spec.map_comp_assoc, ← ι_sigmaSpec R', Category.assoc, IsIso.hom_inv_id_assoc,
    Sigma.ι_desc, ← Category.assoc, hg, IsOpenImmersion.lift_fac]

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 𝒜
s : Set A
⊢ IsClosed (zeroLocus 𝒜 s)

Tactic:
rw [isClosed_iff_zeroLocus]
  exact ⟨s, rfl⟩

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

Goal state before:
pp: ι : 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
⊢ (proj 𝒜 (max₁ + max₂)) (x * y) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) with x_1.1 + x_1.2 = max₁ + max₂,
      (proj 𝒜 x_1.1) x * (proj 𝒜 x_1.2) y

Tactic:
proj_apply,

Goal state after:
ι : 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
⊢ ↑(((decompose 𝒜) (x * y)) (max₁ + max₂)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) with x_1.1 + x_1.2 = max₁ + max₂,
      ↑(((decompose 𝒜) x) x_1.1) * ↑(((decompose 𝒜) y) x_1.2)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯

Tactic:
let e₁ := pullbackComp (𝟙 _) f
  let e₂ := Functor.isoWhiskerLeft (pullback f) (pullbackId _)
  let e₃ := (pullback f).rightUnitor
  change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
  have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)
  simp [← this]

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ Continuous (ToSpec.toFun f)

Tactic:
rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]
      rintro _ ⟨x, rfl⟩
      obtain ⟨x, rfl⟩ := Quotient.mk''_surjective x
      rw [ToSpec.preimage_basicOpen]
      exact (pbo (x.num : A)).2.preimage continuous_subtype_val

Goal state after:
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
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

Tactic:
refine ⟨0, zero_mem _, ?_⟩

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
⊢ (algebraMap A (at Submonoid.powers f)) 0 = f ^ k' • val z
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 (val ((localRingHom f I J hIJ) x))
⊢ IsUnit (val x)

Tactic:
val_localRingHom

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
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx : IsUnit ((Localization.localRingHom I J (↑f) hIJ) (val x))
⊢ IsUnit (val x)
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 𝒜
ι : Type u_2
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↥(Proj 𝒜)
hx : x ∈ ⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule

Tactic:
Ideal.span_le,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↥(Proj 𝒜)
hx : x ∈ ⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Set.range f ⊆ ↑x.asHomogeneousIdeal.toSubmodule