mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ s ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 s]

Goal state after:
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
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ ∑ i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s), ↑(((DirectSum.decompose 𝒜) s) i) ∈
    ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
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
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one,
    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_under,
    IsLocalization.under_map_of_isPrime_disjoint (.powers f)]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ↑z.num ∈ (↑x).asHomogeneousIdeal.toIdeal ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal

case hI
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑x).asHomogeneousIdeal.toIdeal.IsPrime

case hM
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Disjoint ↑(Submonoid.powers f) ↑(↑x).asHomogeneousIdeal.toIdeal

case hy
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.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✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ Set.Ici k ⊆ {x | (fun n ↦ f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

Tactic:
rintro k' (hk' : k ≤ k')

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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ k' ∈ {x | (fun n ↦ f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) 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
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
this : f ^ n ≠ 0
⊢ HomogeneousLocalization.mk z =
    HomogeneousLocalization.mk { deg := m * n, num := ⟨↑z.num, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }

Tactic:
apply HomogeneousLocalization.val_injective; simp only [hn, HomogeneousLocalization.val_mk]

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ x ^ 1 = f * g

Tactic:
by simp [hx]

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ val ((awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a)) =
    ((fromZeroRingHom 𝒜 (Submonoid.powers x)) a).val

Tactic:
simp only [fromZeroRingHom, val_awayMap]

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯)
      ({ toFun := fun f_1 ↦ mk { deg := 0, num := f_1, den := 1, den_mem := ⋯ }, map_one' := ⋯, map_mul' := ⋯,
            map_zero' := ⋯, map_add' := ⋯ }
          a).val =
    ({ toFun := fun f ↦ mk { deg := 0, num := f, den := 1, den_mem := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        a).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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • (d + e))

Tactic:
rw [smul_add]

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • d + n • e)
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'
hm' : 0 < m'
⊢ ↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) = Set.range ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))

Tactic:
rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]

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'
hm' : 0 < m'
⊢ ↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) =
    Set.range
      ⇑((pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯).inv ≫ Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  ((IsOpenImmersion.isoOfRangeEq (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
            (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ⋯).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst)))))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
      (unop f))

Tactic:
obtain ⟨n, a, e⟩ : ∃ n, f.unop ∣ g.unop ^ n := by
            simpa only [Ideal.mem_radical_iff, Ideal.mem_span_singleton] using
              (basicOpen_le_basicOpen_iff _ _).mp (i.1.hom.le)

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
n : ℕ
a : ↑R
e : unop g ^ n = unop f * a
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
      (unop f))
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
i : ι
b : B
hb : b ∈ Ideal.span (⇑f '' ↑I.toIdeal)
⊢ ↑(((DirectSum.decompose ℬ) b) i) ∈ Ideal.map f I.toIdeal

Tactic:
induction hb using Submodule.span_induction generalizing i with

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

Goal state before:
pp: case e_y.inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ i, dv i * (ai i / d) * d ≤ ∑ x, dv x * ai x

Tactic:
mul_assoc

Goal state after:
case e_y.inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
hd : d > 0
⊢ ∑ x, dv x * (ai x / d * d) ≤ ∑ x, dv x * ai x
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 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom ≫
          CommRingCat.ofHom
              (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal
                p.asHomogeneousIdeal.toIdeal ⋯) ≫
            (stalkIso ℬ p).inv))
      x)
⊢ IsUnit x

Tactic:
simp only [CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp,
      Function.comp_apply] at 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))
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)))
⊢ IsUnit x
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:
by
  have : IsFractionRing O K := hv.isFractionRing
  exact
    (IsIntegrallyClosed.integralClosure_eq_bot_iff K).mp (Valuation.Integers.integralClosure hv)

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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑z.den * ↑y.num))) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + z.deg + y.deg))
| ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + z.deg + y.deg))

Tactic:
rw [add_right_comm]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑z.den * ↑y.num))) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + z.deg + y.deg))
| ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ l₀ ≫ f = commSq.i₂ ≫ Y'_to_Y

Tactic:
by simp_all only [commSq']

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver f) → Cover.Over S (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver f), T f H = (V f H).toPresieveOver
⊢ 𝒰.toPresieveOver.bind T ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}

Tactic:
refine ⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver f) → Cover.Over S (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver f), T f H = (V f H).toPresieveOver
⊢ 𝒰.toPresieveOver.bind T = Cover.toPresieveOver (Precoverage.ZeroHypercover.bind 𝒰 fun j ↦ V (Hom.asOver (𝒰.f j) S) ⋯)
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 :=
  { 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

Tactic:
exact congrArg CommSq.LiftStruct.l h₁₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ S.i₁ ≫ pullback.diagonal f = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h

Tactic:
apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
        · simpa using hl₁.symm
        · simpa using hl₂.symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
⊢ ∀ ⦃X_1 Y : WalkingMulticospan data.multicospanShape⦄ (f_1 : X_1 ⟶ Y),
    ((data.multicospanIndex P).multicospan.map f_1 ≫
        match Y with
        | WalkingMulticospan.left i => f.app (op (data.X i))
        | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
      (match X_1 with
        | WalkingMulticospan.left i => f.app (op (data.X i))
        | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
        (data.multicospanIndex Q).multicospan.map f_1

Tactic:
by
    rintro (i₁ | j₁) (i₂ | j₂) (_ | _) <;>
    simp [MulticospanIndex.multicospan]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
E : F.Elements
he : IsInitial E
X✝ : C
f : X✝ ⟶ unop E.fst
this : ↑(he.to ⟨op X✝, (ConcreteCategory.hom (F.map f.op)) E.snd⟩) = ↑⟨f.op, ⋯⟩
⊢ (fun y ↦ (↑(he.to ⟨op X✝, y⟩)).unop) ((fun f ↦ (ConcreteCategory.hom (F.map f.op)) E.snd) f) = f

Tactic:
simp only [this, Quiver.Hom.unop_op]

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
⊢ IsLocalizing (modulesSpecToSheaf.obj M) ↔ Aux M ⊤

Tactic:
by
  let φ (f : R) := ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op).hom
  refine ⟨fun h ↦ ?_, fun h f ↦ IsLocalizedModule.Away.mk_of_addCommGroup ?_ ?_ ?_⟩
  · have hf (f : R) : IsLocalizedModule.Away f (φ f) := h f
    refine ⟨fun f hle s ↦ ?_, fun f hle s hs ↦ ?_⟩
    · obtain ⟨n, y, hy⟩ := (hf f).surj _ _ s
      use n, y, hy.symm
    · obtain ⟨⟨_, n, rfl⟩, hn⟩ := (IsLocalizedModule.eq_zero_iff (.powers f) (φ f)).mp hs
      use n, hn
  · exact Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen f le_rfl
  · intro x
    obtain ⟨n, t, ht⟩ := h.existence _ _ x
    use n, t, ht.symm
  · intro x hx
    obtain ⟨n, hn⟩ := h.uniqueness _ _ _ hx
    use n, hn

Goal state after: