mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
⊢ IsCommMonObj X

Tactic:
have : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) := rfl

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ IsCommMonObj X
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) :=
  (pullbackSpecIso (↑Γ(S, U)) R ↑Γ(X, V)).symm ≪≫
    pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)))
      (Spec.map (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↑Γ(X, V))))
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) :=
  e₁.hom ≫
    pullback.map (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)
      (IsAffineOpen.fromSpec hV) (𝟙 (Spec (CommRingCat.of R))) (IsAffineOpen.fromSpec hU) ⋯ ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := g ''ᵁ PrimeSpectrum.basicOpen e
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
W₂ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := { carrier := (↑W₁)ᶜ, is_open' := ⋯ }
⊢ g { asIdeal := P', isPrime := w✝¹ } ∈ W₁

Tactic:
exact ⟨⟨P', ‹_›⟩, heP', rfl⟩

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

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
⊢ IsCommMonObj G

Tactic:
by
  let f := Spec.map (CommRingCat.ofHom <| algebraMap K (AlgebraicClosure K))
  let G' := (Over.pullback f).obj G
  have : IsProper G'.hom := by dsimp [G']; infer_instance
  have : IsIntegral (G' ⊗ G').left := by dsimp [G']; infer_instance
  let : GrpObj G' := Functor.grpObjObj
  have := isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed G'
  rw [isCommMonObj_iff_commutator_eq_toUnit_η] at this ⊢
  apply (Over.pullback f).map_injective
  rw [← cancel_epi (Functor.Monoidal.μIso (Over.pullback f) G G).hom]
  dsimp [GrpObj.commutator] at this ⊢
  simpa only [Functor.map_mul, one_eq_one, comp_one, Functor.map_one, Functor.map_inv',
    comp_mul, GrpObj.comp_inv, Functor.Monoidal.μ_fst, Functor.Monoidal.μ_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ IsOpen {x | QuasiFiniteAt f x}

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ ∀ x ∈ {x | QuasiFiniteAt f x}, ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
⊢ Smooth f

Tactic:
have := LocallyOfFiniteType.jacobsonSpace f

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this : JacobsonSpace ↥G
⊢ Smooth f
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b : B
f : a ⟶ b
g : b ⟶ a
F : B ⥤ᵖ C
adj : f ⊣ g
⊢ rightZigzag ((F.mapId a).inv ≫ F.map₂ adj.unit ≫ (F.mapComp f g).hom)
      ((F.mapComp g f).inv ≫ F.map₂ adj.counit ≫ (F.mapId b).hom) =
    F.map g ◁ (F.mapId a).inv ⊗≫
      (F.mapComp g (𝟙 a)).inv ≫
        F.map₂ (rightZigzag adj.unit adj.counit) ≫ (F.mapComp (𝟙 b) g).hom ⊗≫ (F.mapId b).hom ▷ F.map g

Tactic:
simp [rightZigzag, bicategoricalComp, F.map₂_iso_inv]

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
⊢ (if 1 ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R 1) else 0) = 1

Tactic:
by simp [nonZeroDivisors]

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(Multiplicative.toAdd (ordMonoidHom x))) = (ordMonoidWithZeroHom R) ↑x

Tactic:
simp only [SetLike.coe_mem, ordMonoidWithZeroHom_eq_ord, ordMonoidHom, MonoidHom.coe_mk,
    OneHom.coe_mk, toAdd_ofAdd]
  rw [← ENat.natCast_lift (ord R x.1) (ord_lt_top x.2), ENat.recTopCoe_natCast,
    ENat.natCast_lift, ENat.lift_eq_toNat_of_lt_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
by_cases! hx : coheight x ≠ 1
  · simp [hx]
  rw [ord_eq_iff hx <| (mul_ne_zero_iff_right hg).mpr hf]
  simp [hf, hg, ord_eq_ordHom_of_coheight_eq_one hx, unzeroD_eq_unzero]

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 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ z ∈ ↑(⨆ i, basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f))

Tactic:
mem_coe,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ z ∈ ⨆ i, basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f)
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
z : ι × ι
H : z ∈ antidiag.erase (max₁, max₂)
⊢ (proj 𝒜 z.1) x * (proj 𝒜 z.2) y ∈ I

Tactic:
rcases z with ⟨i, j⟩

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H : (i, j) ∈ antidiag.erase (max₁, max₂)
⊢ (proj 𝒜 (i, j).1) x * (proj 𝒜 (i, j).2) y ∈ I
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1
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
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).obj U ≅
    ((SheafOfModules.forget X.ringCatSheaf).obj (unit X.ringCatSheaf)).obj U

Tactic:
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

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

Goal state before:
pp: case e'_2
ι : 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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.den * ↑c3.num + ↑c3.den * ↑c1.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ + Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩

Tactic:
Localization.add_mk

Goal state after:
case e'_2
ι : 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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.den * ↑c3.num + ↑c3.den * ↑c1.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk (↑⟨↑c1.den, ⋯⟩ * ↑c3.num + ↑⟨↑c3.den, ⋯⟩ * ↑c1.num) (⟨↑c1.den, ⋯⟩ * ⟨↑c3.den, ⋯⟩)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e'_3
ι : 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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.den * ↑c4.num + ↑c4.den * ↑c2.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩ + Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩

Tactic:
Localization.add_mk

Goal state after:
case e'_3
ι : 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
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.den * ↑c4.num + ↑c4.den * ↑c2.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑⟨↑c2.den, ⋯⟩ * ↑c4.num + ↑⟨↑c4.den, ⋯⟩ * ↑c2.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ + Localization.mk ↑y2.num ⟨↑y2.den, ⋯⟩

Tactic:
Localization.add_mk

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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m), (algebraMap A (at Submonoid.powers f)) x = f ^ (k' - k) • f ^ k • val z

Tactic:
hk,

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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m), (algebraMap A (at Submonoid.powers f)) x = f ^ (k' - k) • den z • val z
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, ⊤)
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)
⊢ ↑(((DirectSum.decompose 𝒜) x) c) ∈ Ideal.span (Set.range fun x ↦ x.snd.fst)

Tactic:
have : c ≠ 0 := by contrapose hc; simpa [hc] using hx

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, ⊤)
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) ∈ Ideal.span (Set.range fun x ↦ x.snd.fst)
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
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)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ a ∈ Submodule.span ↥(𝒜 0) ↑(Submonoid.closure (Set.range v))

Tactic:
rw [← Algebra.adjoin_eq_span, hx]

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
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)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ a ∈ Subalgebra.toSubmodule ⊤
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e'_5
ι : 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)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ¬∑ i, ai i • dv i = n
this : ↑(((decompose 𝒜) (∏ i, v i ^ ai i)) n) = 0
⊢ (mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ }).val = val 0

Tactic:
simp [this, Localization.mk_zero]

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

Goal state before:
pp: case inr
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
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
      (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

Tactic:
rw [← tilde.toOpen_res _ (PrimeSpectrum.basicOpen 1) _ (homOfLE (by simp)), Category.assoc,
      NatTrans.naturality, ← Category.assoc, this, ← Functor.map_comp, ← op_comp, homOfLE_comp]

Goal state after:
case inr.hU
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
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1
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 ℬ
⊢ (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom ≫
      CommRingCat.ofHom
          (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal
            ⋯) ≫
        (stalkIso ℬ p).inv =
    PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p

Tactic:
rw [← Iso.eq_inv_comp, Iso.comp_inv_eq]
  ext : 1
  simp only [CommRingCat.hom_ofHom, stalkIso, RingEquiv.toCommRingCatIso_inv,
    RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp]
  ext x : 2
  obtain ⟨c, rfl⟩ := x.mk_surjective
  simp only [val_localRingHom, val_mk, RingHom.comp_apply]
  simp only [GradedRingHom.toRingHom_eq_toRingHom, Localization.localRingHom_mk,
    GradedRingHom.coe_toRingHom]
  -- I sincerely apologise for your eyes.
  erw [stalkIso'_symm_mk]
  erw [PresheafedSpace.stalkMap_germ_apply]
  erw [germ_map_sectionInBasicOpen]
  erw [stalkIso'_germ]
  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
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 : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } =
    product

Tactic:
dsimp [product]

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 : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } =
    HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
      HomogeneousLocalization.mk
        { deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
          den_mem := ⋯ }