mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ I)) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)

Tactic:
Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
this : Submodule.map ((mul R R) a) I = a • I
⊢ Submodule.map (Submodule.mkQ (a • I)) (a • I) = ⊥

Tactic:
Submodule.mkQ_map_self

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
this : Submodule.map ((mul R R) a) I = a • I
⊢ ⊥ = ⊥
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : {b} • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ b • span {a})

Tactic:
rw [this] at lem

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ b • span {a})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x * a}) = Module.length R (R ⧸ span {x})

Tactic:
Ideal.span_singleton_mul_right_unit h x

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x}) = Module.length R (R ⧸ span {x})
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: case hV'
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
⊢ IsCompact (Set.range ⇑g)

Tactic:
· exact isCompact_range g.continuous

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro V U i f ⟨j, r, s, h, w⟩; exact ⟨j, r, s, (h <| i ·), (w <| i ·)⟩

Goal state after:
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
h : I.IsPrime
⊢ (Ideal.homogeneousCore 𝒜 I).toIdeal.IsPrime

Tactic:
apply (Ideal.homogeneousCore 𝒜 I).isHomogeneous.isPrime_of_homogeneous_mem_or_mem
  · exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)
  rintro x y hx hy hxy
  have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy)
  refine H.imp ?_ ?_
  · exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx
  · exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy

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
⊢ (carrier x).IsPrime

Tactic:
refine Ideal.IsPrime.comap _ (hK := ?_)
  exact IsLocalization.isPrime_of_isPrime_disjoint
    (Submonoid.powers f) _ _ inferInstance
    ((disjoint_powers_iff_notMem_of_isPrime _).mpr x.2)

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))ᵒᵖ
⊢ ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
                TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                  sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                    (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).obj
            M).obj.obj
      U ≅
    ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
                TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                  sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                    (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).obj
            M).obj.obj
      U

Tactic:
refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp φ.hom ((Scheme.ΓSpecIso S).inv).hom).app _

Goal state after:
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)
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:
← CommRingCat.hom_comp,

Goal state after:
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) =
    (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } = x

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val 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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ = HomogeneousLocalization.val x

Tactic:
rw [← hx]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ (algebraMap (A⁰_ f) (Localization.Away f)) x = HomogeneousLocalization.val 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 g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : z ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ ∑ i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) z), ↑(((DirectSum.decompose 𝒜) z) i) ∈
    Ideal.span (Set.range fun i ↦ ↑i.snd)

Tactic:
refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : z ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c ∈ DFinsupp.support ((DirectSum.decompose 𝒜) z)
hc0 : c = 0
⊢ ↑(((DirectSum.decompose 𝒜) z) c) ∈ Ideal.span (Set.range fun i ↦ ↑i.snd)
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
⊢ HomogeneousLocalization.mk
      { deg := m * i + m * i,
        num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩,
        den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } =
    ∑ i ∈ range (m + m + 1), g i

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
⊢ Localization.mk
      ↑{ deg := m * i + m * i,
            num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩,
            den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i + m * i,
              num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩,
              den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.den,
        ⋯⟩ =
    HomogeneousLocalization.val (∑ i ∈ range (m + m + 1), g i)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ M : ModuleCat ↑R
⊢ (tilde.functor R).map (toTildeΓNatIso.hom.app M) ≫ fromTildeΓNatTrans.app ((tilde.functor R).obj M) =
    𝟙 ((tilde.functor R).obj M)

Tactic:
by
    apply SpecModulesToSheafFullyFaithful.map_injective
    apply CategoryTheory.Sheaf.hom_ext
    apply (TopCat.Sheaf.restrictHomEquivHom _ _ PrimeSpectrum.isBasis_basic_opens).symm.injective
    ext r : 3
    apply IsLocalizedModule.ext (.powers (M := R) r.unop)
      (toOpen _ (PrimeSpectrum.basicOpen (R := R) r.unop)).hom
    · rw [Subtype.forall]
      change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
      simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
      exact Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen r.unop le_rfl
    dsimp [toTildeΓNatIso, isoTop,
      TopCat.Sheaf.restrictHomEquivHom, Functor.IsCoverDense.restrictHomEquivHom,
      fromTildeΓNatTrans, moduleSpecΓFunctor, Sheaf.forget, sheafToPresheaf]
    simp only [← ModuleCat.hom_comp, Functor.map_comp]
    congr 1
    rw [ObjectProperty.FullSubcategory.comp_hom]
    dsimp
    rw [toOpen_map_app_assoc, toOpen_fromTildeΓ_app]
    rfl

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

Goal state before:
pp: case hy
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
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ isLocalizationElem hf ⋯ ∈
    {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩

Goal state after:
case hy.refine_1
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
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ ∑ i, Pi.single j d i • dv i = dv j • d

case hy.refine_2
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
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ ∀ (i : ι'), Pi.single j d i ≤ d

case hy.refine_3
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
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯ = isLocalizationElem hf ⋯
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
⊢ IsIso M.fromTildeΓ

Tactic:
isIso_fromTildeΓ_iff

Goal state after:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
⊢ (tilde.functor R).essImage M
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case refine_2.refine_3.e_x
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∏ i, v i ^ (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i = ∏ i, (v ∘ Subtype.val) i ^ ai i

Tactic:
change _ = ∏ x ∈ s.attach, _

Goal state after:
case refine_2.refine_3.e_x
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∏ i, v i ^ (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i = ∏ x ∈ s.attach, (v ∘ Subtype.val) x ^ ai 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
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (↑(((decompose 𝒜) f) m) ^ m) ⟨f ^ m, ⋯⟩

Tactic:
decompose_of_mem_same _ f_deg

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (f ^ m) ⟨f ^ m, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
⊢ ∃ n, f ^ n • t = 0

Tactic:
· obtain ⟨n, hn⟩ := h.uniqueness (a f) le_top (iso.inv t) <| by
      simpa [M', iso, ← M.presheaf.map_comp_apply, homOfLE_op_comp_eqToHom, e] using
        congr((e _ hf).inv $ht)
    use n
    have := congr(iso.hom $hn)
    dsimp [iso, ψ] at this
    rw [eqToHom_op, map_zero, ← map_pow, Scheme.Modules.restrictAppIso_smul_Spec,
      M.map_smul_Spec, Iso.inv_hom_id_apply] at this
    simpa using this

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

Goal state before:
pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows

Tactic:
have (w : W.left) : ∃ (i : ι), w ∈ Set.range (f i).left := by
      have := Set.mem_univ w
      simpa [← hf]

Goal state after:
case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
this : ∀ (w : ↥W.left), ∃ i, w ∈ Set.range ⇑(f i).left
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows

Tactic:
· have (w : W.left) : ∃ (i : ι), w ∈ Set.range (f i).left := by
      have := Set.mem_univ w
      simpa [← hf]
    choose i z hz using this
    let V : Cover (precoverage @Etale) W.left :=
      Cover.mkOfCovers W.left (fun w ↦ (Z (i w)).left)
        (fun w ↦ (f (i w)).left) (fun w ↦ ⟨_, _, hz w⟩) inferInstance
    let : Cover.Over X V :=
      { over w := ⟨(Z (i w)).hom⟩
        isOver_map w := by cat_disch }
    have (w : W.left) : Etale (V.X w ↘ X) := (Z (i w)).prop
    refine ⟨V, inferInstance, inferInstance, ?_⟩
    rintro _ _ ⟨w⟩
    refine ⟨_, 𝟙 _, _, ⟨i w⟩, by cat_disch⟩

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

Goal state before:
pp: R : CommRingCat
⊢ (tilde.functor R).essImage = SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
R : CommRingCat
⊢ (tilde.functor R).essImage ≤ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf

case refine_2
R : CommRingCat
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf ≤ (tilde.functor R).essImage
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
⊢ ∀ ⦃X Y : Cᵒᵖ ⥤ D⦄ (f : X ⟶ Y),
    ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f ≫
        {
          app := fun x ↦
            match x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := ⋯ } =
      {
          app := fun x ↦
            match x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := ⋯ } ≫
        (𝟭 (Cᵒᵖ ⥤ D)).map f

Tactic:
intros; ext; simp

Goal state after: