mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H' :
  ∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
⊢ Disjoint ↑(Submonoid.powers f) ↑P

Tactic:
Ideal.disjoint_powers_iff_notMem_of_isPrime

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H' :
  ∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
⊢ f ∉ P
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ IsOpen (⋃₀ (irreducibleComponents ↥X \ {Z}))ᶜ

Tactic:
Set.sUnion_eq_biUnion,

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ IsOpen (⋃ i ∈ irreducibleComponents ↥X \ {Z}, i)ᶜ
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = ⋂ U, X.zeroLocus ↑((Hom.ker (X.irreducibleComponentOpen Z).ι).ideal U)

Tactic:
by
    rw [← IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Hom.support_ker, Opens.range_ι]
    exact (closure_sUnion_irreducibleComponents_sdiff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents Z hZ).symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictlyUnitaryPseudofunctor B C
G : StrictlyUnitaryPseudofunctor C D
x✝ : B
⊢ (F.comp G.toPseudofunctor).map (𝟙 x✝) = 𝟙 ((F.comp G.toPseudofunctor).obj x✝)

Tactic:
simp [StrictlyUnitaryPseudofunctor.map_id]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₁ : η ▷ k = η₁
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]

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

Goal state before:
pp: C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
⊢ ((mateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans

Tactic:
ext X

Goal state after:
C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
X : ↑D
⊢ ((mateEquiv adj₁ adj₂) f).toNatTrans.app X =
    ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans).app X
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
⊢ R₁.toFunctor.rightUnitor.inv ≫
      (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂))
          ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
        R₂.toFunctor.leftUnitor.hom =
    (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans

Tactic:
ext X

Goal state after:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
X : ↑D
⊢ (R₁.toFunctor.rightUnitor.inv ≫
          (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂))
              ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
            R₂.toFunctor.leftUnitor.hom).app
      X =
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans).app X
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
hf : Surjective f
hhomeo : IsHomeomorph ⇑f
this✝ : QuasiCompact f
this : IsIso f
⊢ IsOpenImmersion f

Tactic:
exact .of_isIso f

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

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ finrank (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x

Tactic:
rw [finrank_SpecMap_eq_finrank]
  · simp
  · simpa [RingHom.finite_algebraMap]
  · simpa [RingHom.flat_algebraMap_iff]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R (a • x) = ord R x

Tactic:
by
  rw [Algebra.smul_def a x]
  exact ord_mul_of_isUnit_left (RingHom.isUnit_map (algebraMap S R) h) x

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
⊢ (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 l₁

Tactic:
by
  rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = -Localization.mk ↑y.num ⟨↑y.den, ⋯⟩

Tactic:
Localization.neg_mk

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ (-Quotient.mk'' y).val = -val (Quotient.mk'' y)

Tactic:
by rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]; rfl

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
f : NumDenSameDeg 𝒜 x
h : f.den = 0
this : Subsingleton (HomogeneousLocalization 𝒜 x)
⊢ mk f = 0

Tactic:
exact Subsingleton.elim _ _

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
f g : ↥(𝒜 0)
⊢ mk { deg := 0, num := f + g, den := 1, den_mem := ⋯ } =
    mk { deg := 0, num := f, den := 1, den_mem := ⋯ } + mk { deg := 0, num := g, den := 1, den_mem := ⋯ }

Tactic:
by ext; simp [Localization.add_mk, add_comm f.1 g.1]

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

Tactic:
rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_smul]

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 𝒜
P : Submonoid A
x : HomogeneousLocalization 𝒜 P
⊢ ((map (GradedRingHom.id 𝒜) ⋯) x).val = ((RingHom.id (HomogeneousLocalization 𝒜 P)) x).val

Tactic:
obtain ⟨c, rfl⟩ := x.mk_surjective

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 𝒜
P : Submonoid A
c : NumDenSameDeg 𝒜 P
⊢ ((map (GradedRingHom.id 𝒜) ⋯) (mk c)).val = ((RingHom.id (HomogeneousLocalization 𝒜 P)) (mk c)).val
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 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
x : HomogeneousLocalization 𝒜 P
⊢ ((map (g.comp f) ⋯) x).val = (((map g hqr).comp (map f hpq)) x).val

Tactic:
obtain ⟨c, rfl⟩ := x.mk_surjective

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 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
c : NumDenSameDeg 𝒜 P
⊢ ((map (g.comp f) ⋯) (mk c)).val = (((map g hqr).comp (map f hpq)) (mk c)).val
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
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : Subsingleton (Away 𝒜 f)
⊢ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} = ⊤

Tactic:
exact Subsingleton.elim _ _

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

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
x : AtPrime 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal
⊢ val
      ((localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)
        x) =
    val
      (((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p))).comp
          ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p)).comp
            (CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' 𝒜 ((ProjectiveSpectrum.comap f hf) p)).symm))))
        x)

Tactic:
obtain ⟨c, rfl⟩ := x.mk_surjective

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ val
      ((localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)
        (HomogeneousLocalization.mk c)) =
    val
      (((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p))).comp
          ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p)).comp
            (CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' 𝒜 ((ProjectiveSpectrum.comap f hf) p)).symm))))
        (HomogeneousLocalization.mk c))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
⊢ ∀ {i : ℕ} (m_1 : ↥(𝒜 i)), ↑m_1 • x ∈ carrier f_deg q

Tactic:
rintro n ⟨a, ha⟩ i

Goal state after:
case refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(proj 𝒜 i) (↑⟨a, ha⟩ • x) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
hx :
  IsUnit
    ((CommRingCat.Hom.hom (stalkIso ℬ p).inv)
      ((localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)
        ((CommRingCat.Hom.hom (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom) x)))
this : IsLocalHom (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
⊢ IsUnit x

Tactic:
replace hx := (isUnit_map_iff _ _).mp hx

Goal state after:
A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
this : IsLocalHom (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
hx :
  IsUnit
    ((localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)
      ((CommRingCat.Hom.hom (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom) x))
⊢ IsUnit x
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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } *
      HomogeneousLocalization.mk { deg := m * ny, num := ⟨y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } =
    HomogeneousLocalization.mk
      { deg := m * (nx + ny), num := ⟨↑(((decompose 𝒜) (x * y)) (nx + ny)) ^ m, ⋯⟩, den := ⟨f ^ (nx + ny), ⋯⟩,
        den_mem := ⋯ }

Tactic:
decompose_of_mem_same 𝒜 (SetLike.GradedMonoid.toGradedMul.mul_mem hnx hny),

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
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } *
      HomogeneousLocalization.mk { deg := m * ny, num := ⟨y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } =
    HomogeneousLocalization.mk
      { deg := m * (nx + ny), num := ⟨(x * y) ^ m, ⋯⟩, den := ⟨f ^ (nx + ny), ⋯⟩, 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ↑x.num ⟨↑x.den, ⋯⟩ =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (IsLocalization.mk' (Localization (Submonoid.powers f)) ↑x.num ⟨↑x.den, ⋯⟩)

Tactic:
IsLocalization.map_mk'

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ↑x.num ⟨↑x.den, ⋯⟩ =
    IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ((RingHom.id A) ↑x.num)
      ⟨(RingHom.id A) ↑⟨↑x.den, ⋯⟩, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overGrothendieckTopology P S) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
rw [overGrothendieckTopology_eq_toGrothendieck_overPretopology]

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f

Tactic:
simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]

Goal state after:
case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ S.i₂ ≫ pullback.fst f f = S.i₂ ≫ pullback.snd f f