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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
⊢ IsOpen {⟨a, ⋯⟩}

Tactic:
rw [← (f.fiberHomeo _).symm.isOpen_image, Set.image_singleton]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
a : ↥X
⊢ IsOpen {(fiberHomeo f (f a)).symm ⟨a, ⋯⟩}
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ map
      ((CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R S) ≫
          CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv)) ≫
        CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫ Over.Hom.left μ

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

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ (map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
        map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
      map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R S)) =
    (pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
        (pullbackSpecIso R S S).hom) ≫
      map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R S))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e_a.h₀
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ ((map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
          map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
        (pullbackSpecIso R S S).inv) ≫
      pullback.fst (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      pullback.fst (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))

pp: case h₁
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ ((map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
          map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
        (pullbackSpecIso R S S).inv) ≫
      pullback.snd (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      pullback.snd (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))

Tactic:
all_goals
    · simp only [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
      ← AlgHom.comp_toRingHom, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
      congr 3
      ext; simp

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

Goal state before:
pp: case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ ((pullbackSpecIso' R T S).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
have : (RingHomClass.toRingHom (Algebra.TensorProduct.comm R S T)).comp
      Algebra.TensorProduct.includeLeftRingHom =
      RingHomClass.toRingHom Algebra.TensorProduct.includeRight := rfl

Goal state after:
case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ ((pullbackSpecIso' R T S).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
x : X
⊢ x ∈ V.left → ∃ U_1 f, ((Sieve.overEquiv V) S).arrows f ∧ x ∈ U_1

Tactic:
hxV

Goal state after:
case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
x : X
hxV : x ∈ V.left
⊢ ∃ U_1 f, ((Sieve.overEquiv V) S).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
⊢ x ∈ U.overEquivalence.functor.obj V →
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1

Tactic:
hxV

Goal state after:
case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
hxV : x ∈ U.overEquivalence.functor.obj V
⊢ ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
hxV : x ∈ U.overEquivalence.functor.obj V
W : Opens X
hxW : ↑x ∈ W
W' : Over U
hW'V : W' ⟶ V
hWW' : W ⟶ (Over.forget U).obj W'
hSW'V : S.arrows hW'V
⊢ ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1

Tactic:
exact ⟨_, U.overEquivalence.functor.map hW'V,
        S.downward_closed hSW'V (U.overEquivalence.unitInv.app W'), hWW'.le hxW⟩

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (mateEquiv adj₁ adj₂) α = β ↔ adj₁.homEquiv₁.symm β = adj₂.homEquiv₂ α ≫ (α_ l₁ h r₂).hom

Tactic:
conv_lhs => rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']
  rw [mateEquiv_apply, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := ⋯
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
x✝ : ↥↑U
x : ↥Y
y : ↥X
hy : f y = x
⊢ U.ι (f' y) = U.ι ⟨x, ⋯⟩

Tactic:
simp [← Scheme.Hom.comp_apply, f', hy]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ Smooth f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := @Smooth) X.affineCover]
    intro i
    have _ (y) : Smooth (pullback.snd f ((Spec R).fromSpecResidueField y)) :=
      inferInstanceAs <| Smooth (f.fiberToSpecResidueField y)
    refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
    rw [Scheme.Hom.fiberToSpecResidueField, ← pullbackRightPullbackFstIso_inv_snd_snd]
    infer_instance

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
⊢ (if x * y ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) else 0) =
    (if x ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) else 0) *
      if y ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y) else 0

Tactic:
split_ifs with _ _ b

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) =
    0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) = 0 * 0

case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∈ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) * 0

case pos
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∈ nonZeroDivisors R
⊢ 0 = 0 * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y)

case neg
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_ : x * y ∉ nonZeroDivisors R
h✝¹ : x ∉ nonZeroDivisors R
h✝ : y ∉ nonZeroDivisors R
⊢ 0 = 0 * 0
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
i : ι
⊢ (Finsupp.equivFunOnFinite.symm fun i x ↦ (f x) i).sum (fun i a ↦ a * ↑i) i = 1 i

Tactic:
simpa [Finsupp.sum_fintype] using hf i

Goal state after:
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 ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).carrier

Tactic:
obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])

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 : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).carrier
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 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s

Tactic:
← isOpen_compl_iff,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen Zᶜ ↔ ∃ s, Z = zeroLocus 𝒜 s
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]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
s : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1
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
hxy : x✝ * y ∈ I
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}
x : A
hx : x ∉ I
⊢ {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty

Tactic:
rw [filter_nonempty_iff]

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
hxy : x✝ * y ∈ I
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}
x : A
hx : x ∉ I
⊢ ∃ a ∈ DFinsupp.support ((decompose 𝒜) x), (proj 𝒜 a) x ∉ I
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 ^ n).num ⟨↑(c1 ^ n).den, ⋯⟩ = Localization.mk ↑(c2 ^ n).num ⟨↑(c2 ^ n).den, ⋯⟩

Tactic:
simp only [num_pow, den_pow]

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 𝒜
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, ⋯⟩
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
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
obtain rfl := DirectSum.degree_eq_of_mem_mem 𝒜 hn (SetLike.pow_mem_graded n hf) hfn

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
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x ↦ f ^ x) n ∈ 𝒜 (n • d)
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
this : f ^ n ≠ 0
⊢ (HomogeneousLocalization.mk z).val =
    (HomogeneousLocalization.mk { deg := m * n, num := ⟨↑z.num, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }).val

Tactic:
simp only [hn, HomogeneousLocalization.val_mk]

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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (Proj 𝒜).homOfLE ⋯ ≫ (basicOpen 𝒜 f).ι = (basicOpen 𝒜 x).ι

Tactic:
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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 x).ι = (basicOpen 𝒜 x).ι
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
⊢ ∀ (m : ↑((Spec R).ringCatSheaf.obj.obj U)) (x : ↑(M.val.1 U)),
    (ModuleCat.Hom.hom (f.hom.app U)).toFun (m • x) =
      (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) m • (ModuleCat.Hom.hom (f.hom.app U)).toFun x

Tactic:
intro t m
    apply TopCat.Presheaf.IsSheaf.section_ext (modulesSpecToSheaf.obj N).2
    intro x hxU
    obtain ⟨a, ⟨_, ⟨r, rfl⟩, rfl⟩, hxr, hrU : basicOpen _ ≤ _⟩ :=
      PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU U.unop.2
    refine ⟨_, hrU, hxr, ?_⟩
    refine Eq.trans ?_ (N.val.map_smul (homOfLE hrU).op t _).symm
    change N.1.map (homOfLE hrU).op (f.1.app _ _) = _ • N.1.map (homOfLE hrU).op (f.1.app _ _)
    have (x : _) :
        f.1.app _ (M.1.map (homOfLE hrU).op _) = N.1.map (homOfLE hrU).op (f.1.app _ x) :=
      congr($(f.1.naturality (homOfLE hrU).op).hom x)
    rw [← this, ← this, M.val.map_smul]
    generalize (Spec R).ringCatSheaf.obj.map (homOfLE hrU).op t = t
    let := Module.compHom (R := Γ(Spec R, basicOpen r)) Γ(M, basicOpen r)
      (algebraMap R Γ(Spec R, basicOpen r))
    have : IsScalarTower R Γ(Spec R, basicOpen r) Γ(M, basicOpen r) :=
      .of_algebraMap_smul fun _ _ ↦ rfl
    let := Module.compHom Γ(N, basicOpen r) (algebraMap R Γ(Spec R, basicOpen r))
    have : IsScalarTower R Γ(Spec R, basicOpen r) Γ(N, basicOpen r) :=
      .of_algebraMap_smul fun _ _ ↦ rfl
    exact (IsLocalization.linearMap_compatibleSMul (.powers (M := R) r)
      Γ(Spec R, basicOpen r) Γ(M, basicOpen r) Γ(N, basicOpen r)).map_smul
      (f.hom.app _).hom _ _

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
⊢ IsIntegral O x ↔ v x ≤ 1

Tactic:
nontriviality R
  have : Nontrivial O := hv.nontrivial_iff.mpr inferInstance
  constructor
  · rintro ⟨f, hm, hf⟩
    by_cases hn : f.natDegree = 0
    · rw [Polynomial.natDegree_eq_zero] at hn
      obtain ⟨c, rfl⟩ := hn
      simp [map_eq_zero_iff _ hv.hom_inj, hm.ne_zero_of_C] at hf
    simp only [Polynomial.eval₂_eq_sum_range, Finset.sum_range_succ, hm.coeff_natDegree, map_one,
      one_mul, add_eq_zero_iff_eq_neg] at hf
    apply_fun v at hf
    simp only [map_neg, map_pow] at hf
    contrapose! hf
    refine ne_of_lt (v.map_sum_lt ?_ ?_)
    · simp [hn, (hf.trans' (zero_lt_one)).ne']
    · simp only [Finset.mem_range, map_mul, map_pow]
      intro _ hi
      exact mul_lt_of_le_one_of_lt (hv.map_le_one _) <| pow_lt_pow_right₀ hf hi
  · intro h
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one h
    exact ⟨Polynomial.X - .C y, by monicity, by simp⟩

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

Goal state before:
pp: K : Type u
Γ₀ : Type v
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
⊢ IsIntegrallyClosed O

Tactic:
have : IsFractionRing O K := hv.isFractionRing

Goal state after:
K : Type u
Γ₀ : Type v
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
this : IsFractionRing O K
⊢ IsIntegrallyClosed O
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ HomogeneousLocalization.val 1 =
    (HomogeneousLocalization.mk { deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }).val

Tactic:
HomogeneousLocalization.val_one,

Goal state after:
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
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = (HomogeneousLocalization.mk { deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }).val