mathlib-initiative/mathlib-tactics huggingface dataset:
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 𝒜
⊢ ↑(basicOpen 𝒜 1) = ↑⊤

Tactic:
by simp

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 𝒜
⊢ ↑(basicOpen 𝒜 0) = ↑⊥

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (f ≫ g ≫ h) = pullback ((f ≫ g) ≫ h)

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (f ≫ 𝟙 Y) = pullback f

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ pullback (𝟙 X ≫ f) = pullback f

Tactic:
by simp

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

Goal state before:
pp: case I_ne_top
ι : 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
h : I.IsPrime
⊢ (Ideal.homogeneousCore 𝒜 I).toIdeal ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ restrict (unit Y.ringCatSheaf) f ≅ unit X.ringCatSheaf

Tactic:
refine (fullyFaithfulForget _).preimageIso <| PresheafOfModules.isoMk (fun U ↦ ?_) ?_
  · refine ModuleCat.isoMk
      ((forget₂ CommRingCat RingCat ⋙ forget₂ _ Ab).mapIso (f.appIso U.unop)) ?_
    intro (r : Γ(X, U.unop))
    ext (x : Γ(Y, f ''ᵁ U.unop))
    change r * (f.appIso U.unop).hom x = (f.appIso U.unop).hom ((f.appIso U.unop).inv r * x)
    simp
  · intro U V g
    have : Y.presheaf.map (homOfLE (by grw [leOfHom g.unop])).op ≫
        (f.appIso _).hom = (f.appIso U.unop).hom ≫ X.presheaf.map g := by
      simp [Hom.appIso_hom']
    ext x
    exact congr($(this) x)

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
x✝ : X.Opens
⊢ (𝟭 X.Opens).obj x✝ = 𝟙 X ''ᵁ x✝

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
x✝ : X.Opens
⊢ (Hom.opensFunctor f ⋙ Hom.opensFunctor g).obj x✝ = (f ≫ g) ''ᵁ x✝

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M✝ N K : X.Modules
φ : M✝ ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
M : Z.Modules
⊢ g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U)) = (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
by simp

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

Goal state before:
pp: X Y Z T : Scheme
M✝ N K : X.Modules
φ : M✝ ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
M : Z.Modules
⊢ (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U) = g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U))

Tactic:
by simp

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

Goal state before:
pp: case refine_1.refine_1
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U✝ V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
U : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ
⊢ (CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ) =
    (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)

Tactic:
rw [← CommRingCat.hom_comp, Scheme.ΓSpecIso_inv_naturality, CommRingCat.hom_comp]

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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
⊢ ↑z.num ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal

Tactic:
have : f ^ n ≠ 0 := fun e ↦ by
    have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, e⟩
    exact IsEmpty.elim (inferInstanceAs (IsEmpty (PrimeSpectrum (A⁰_ f)))) q

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
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
this : f ^ n ≠ 0
⊢ ↑z.num ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
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
g : 𝒜 →+*ᵍ ℬ
f : A
n : ℕ
⊢ (fun x ↦ g f ^ x) n = g ((fun x ↦ f ^ x) n)

Tactic:
by simp

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
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι =
    (basicOpenIsoSpec 𝒜 x ⋯ ⋯).inv ≫ (basicOpen 𝒜 x).ι

Tactic:
Iso.eq_inv_comp,

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
⊢ (basicOpenIsoSpec 𝒜 x ⋯ ⋯).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (basicOpen 𝒜 f).ι =
    (basicOpen 𝒜 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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm = awayι 𝒜 x ⋯ ⋯

Tactic:
rw [awayι, awayι, Iso.eq_inv_comp, basicOpenIsoSpec_hom, basicOpenToSpec_SpecMap_awayMap_assoc,
  ← basicOpenIsoSpec_hom _ _ f_deg hm, Iso.hom_inv_id_assoc, Scheme.homOfLE_ι]

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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : f t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
⊢ Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x) (X.basicOpen x') ⋯ ≫
      (basicOpenIsoSpecAway x).hom ≫
        Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen x') ⋯ ≫
      (basicOpenIsoSpecAway x').hom ≫
        Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'

Tactic:
have hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x := by
    aesop (add simp PrimeSpectrum.basicOpen_mul)

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : f t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
⊢ Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x) (X.basicOpen x') ⋯ ≫
      (basicOpenIsoSpecAway x).hom ≫
        Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen x') ⋯ ≫
      (basicOpenIsoSpecAway x').hom ≫
        Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e_a.e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x✝ : Away 𝒜 t
⊢ (IsLocalization.Away.awayToAwayRight x (f s)).comp (IsLocalization.map (Localization.Away x) f ⋯) =
    (IsLocalization.map (Localization.Away x') f ⋯).comp
      (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯)

Tactic:
apply IsLocalization.ringHom_ext (M := .powers t)

Goal state after:
case e_a.e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x✝ : Away 𝒜 t
⊢ ((IsLocalization.Away.awayToAwayRight x (f s)).comp (IsLocalization.map (Localization.Away x) f ⋯)).comp
      (algebraMap A (Localization.Away t)) =
    ((IsLocalization.map (Localization.Away x') f ⋯).comp
          (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯)).comp
      (algebraMap A (Localization.Away t))
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 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c ∈ DFinsupp.support ((DirectSum.decompose 𝒜) x)
this : c ≠ 0
⊢ (((DirectSum.decompose 𝒜) x) c).1 ∈ 𝒜 c

Tactic:
by simp

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 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (fun ir ↦ X.basicOpen (f ir.snd.fst)) x ⊓ (fun ir ↦ X.basicOpen (f ir.snd.fst)) y =
    X.basicOpen (f (x.snd.fst * y.snd.fst))

Tactic:
by simp

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
S : CommRingCat
f : R ⟶ S
inst✝ : IsOpenImmersion (Spec.map f)
U : (Spec S).Opens
r : ↑R
x : ↑Γ(M.restrict (Spec.map f), U)
⊢ (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) ((ConcreteCategory.hom f) r • x) =
    r • (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x

Tactic:
rw [smul_Spec_def, smul_Spec_def]
  simp_rw [smul_restrictAppIso_hom_apply, ← ConcreteCategory.comp_apply, Category.assoc]
  have :
      f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map U.leTop.op ≫ (Hom.appIso (Spec.map f) U).inv =
        (ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Spec.map f ''ᵁ U).leTop.op := by
    simp [Iso.cancel_iso_inv_left, Hom.app_eq_appLE]
    rfl
  rw [this]

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

Goal state before:
pp: R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ U ≤ PrimeSpectrum.basicOpen 1

Tactic:
by simp

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

Goal state before:
pp: R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
x : ↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤))
⊢ ∀ (x : ↥(Submonoid.powers 1)),
    IsUnit ((algebraMap (↑R) (Module.End ↑R ↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen 1))))) ↑x)

Tactic:
by simp

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 (𝒜₊)
s : A
⊢ (basicOpen ℬ (f s)).ι ≫ map f hf =
    Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ ≫ (basicOpen 𝒜 s).ι

Tactic:
by simp

Goal state after:
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 (ℬ₊)
⊢ 𝒜₊ ≤ HomogeneousIdeal.map (GradedRingHom.id 𝒜) (𝒜₊)

Tactic:
by simp

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
h₁ : IsColimit (CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯) :=
  ModuleCat.isColimitCokernelCofork (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) H₁ ⋯
⊢ (tildeFinsupp ↑t).hom ≫
      (tildeFinsupp ↑t).inv ≫
        tilde.map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ≫ (tildeFinsupp ↑s).hom =
    (tilde.functor R).map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ≫ (tildeFinsupp ↑s).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : K
hx : x ∈ A
⊢ (IsLocalization.lift ⋯) ((algebraMap (↥A) (Localization.AtPrime P)) ⟨x, hx⟩) = x

Tactic:
by simp

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
h₁ : IsColimit (CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯) :=
  ModuleCat.isColimitCokernelCofork (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) H₁ ⋯
⊢ (tildeFinsupp ↑s).hom ≫
      Cofork.π
        (CokernelCofork.ofπ
          ((tildeFinsupp ↑s).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))) ⋯) =
    Cofork.π
        ((CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯).map (tilde.functor R)) ≫
      (Iso.refl
          ((CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯).map
              (tilde.functor R)).pt).hom

Tactic:
by simp

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
⊢ Submodule.span (↑R) Set.univ = ⊤

Tactic:
by simp

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
a✝ : Nontrivial R
this : Nontrivial O
y : O
h : v ((algebraMap O R) y) ≤ 1
⊢ eval₂ (algebraMap O R) ((algebraMap O R) y) (X - C y) = 0

Tactic:
by simp

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

Goal state before:
pp: case refine_3
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
⊢ ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q

Tactic:
· simp_rw [add_smul]; exact fun _ _ => carrier.add_mem f_deg q

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

Goal state before:
pp: case inl
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ Away.mk 𝒜 hf a (∏ i, ↑i ^ ai i) ⋯ ∈ ↑(↥(𝒜 0))[f']

Tactic:
obtain rfl : ai = 0 := funext <| by simpa [hd, hdx] using hai

Goal state after:
case inl
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i, 0 i • dx i = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ Away.mk 𝒜 hf a (∏ i, ↑i ^ 0 i) ⋯ ∈ ↑(↥(𝒜 0))[f']
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ R ≤ fSₘ

Tactic:
refine ⟨hS.le.trans (LocalSubring.le_ofPrime ..), ((local_hom_TFAE _).out 2 0).mp ?_⟩

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ maximalIdeal ↥fSₘ.toSubring
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral ↥R.toSubring ↥S
⊢ RingHom.ker (algebraMap ↥R.toSubring ↥S) ≠ ⊤

Tactic:
by simp

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
H : IsUnit p.leadingCoeff
⊢ (Polynomial.C ↑H.unit⁻¹ * p).Monic

Tactic:
simp [Polynomial.Monic]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ Existence f ∧ Uniqueness f

Tactic:
change (∀ _, _) ↔ (∀ _, _) ∧ (∀ _, _)

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ValuativeCommSq f), Nonempty (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton ⋯.LiftStruct
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} = ⊤
p : (↥R.toSubring)[X]
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (aeval ⅟x⁻¹) p = 0
H : IsUnit p.leadingCoeff
⊢ (C ↑H.unit⁻¹ * p).Monic

Tactic:
simp [Polynomial.Monic]

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x ∈ ⊤

Tactic:
by simp

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x ∈ ⊤

Tactic:
by simp

Goal state after: