mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, Function.Surjective ⇑f

Tactic:
by
  classical
  obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
    have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
  clear hs
  induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

Tactic:
by
  by_cases hr' : Ideal.span {r} = ⊤
  · rw [hr', ringKrullDim_eq_bot_of_subsingleton]
    simp
  have : Nonempty (PrimeSpectrum.zeroLocus (R := R) (Ideal.span {r})) := by
    rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
  have := Ideal.Quotient.nontrivial_iff.mpr hr'
  have := (Ideal.Quotient.mk (Ideal.span {r})).domain_nontrivial
  rw [ringKrullDim_quotient, Order.krullDim_eq_iSup_length, ringKrullDim,
    Order.krullDim_eq_iSup_length, ← WithBot.coe_one, ← WithBot.coe_add,
    ENat.iSup_add, WithBot.coe_le_coe, iSup_le_iff]
  intro l
  obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le (J := l.head.1.asIdeal) bot_le
  let p' : PrimeSpectrum R := ⟨p, hp.1.1⟩
  have hp' : p' < l.head := lt_of_le_of_ne hp' fun h ↦ Set.disjoint_iff.mp
    (Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes hp)
    ⟨show r ∈ p by simpa [← h] using l.head.2, hr⟩
  refine le_trans ?_ (le_iSup _ ((l.map Subtype.val (fun _ _ ↦ id)).cons p' hp'))
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)

Tactic:
simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.vcomp]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      (𝟙 (r₁ ≫ g ≫ 𝟙 c) ⊗≫
          r₁ ◁ (g ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ g (𝟙 c) l₃).hom ≫
                    g ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ g l₂ (𝟙 d)).inv ≫ α ▷ 𝟙 d ≫ (α_ l₁ h (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (h ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((h ≫ 𝟙 d) ≫ r₃)) ⊗≫
        𝟙 (h ≫ r₃) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (g ◁ β ≫ α) ▷ r₃ ⊗≫ adj₁.counit ▷ h ▷ r₃ ⊗≫ 𝟙 (h ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst✝ : IsIso φ
⊢ Hom.app (inv φ) U = inv (Hom.app φ U)

Tactic:
by
  apply IsIso.eq_inv_of_hom_inv_id
  simp [← Hom.comp_app]

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
⊢ restrictFunctor f ⊣ pushforward f

Tactic:
refine pushforwardPushforwardAdj (by exact f.isOpenEmbedding.isOpenMap.adjunction) _ _ ?_ ?_

Goal state after:
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
⊢ Functor.whiskerRight (NatTrans.op ⋯.adjunction.counit) Y.ringCatSheaf.obj =
    (Hom.toRingCatSheafHom f).hom ≫
      (Opens.map f.base).op.whiskerLeft
        {
            hom :=
              Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                (forget₂ CommRingCat RingCat) }.hom

case refine_2
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
⊢ {
          hom :=
            Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
              (forget₂ CommRingCat RingCat) }.hom ≫
      (Hom.opensFunctor f).op.whiskerLeft (Hom.toRingCatSheafHom f).hom ≫
        Functor.whiskerRight (NatTrans.op ⋯.adjunction.unit) X.ringCatSheaf.obj =
    𝟙 X.ringCatSheaf.obj
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.num * ↑c3.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ * Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩

Tactic:
rw [Localization.mk_mul]

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.num * ↑c3.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk (↑c1.num * ↑c3.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.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩ * Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩

Tactic:
rw [Localization.mk_mul]

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.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑c2.num * ↑c4.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.den, ⋯⟩)
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
this :
  ((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom =
    awayToSection 𝒜 f
⊢ IsIso
    (((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom)

Tactic:
← basicOpenIsoSpec_hom 𝒜 f f_deg hm

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
this :
  ((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom =
    awayToSection 𝒜 f
⊢ IsIso
    (((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenIsoSpec 𝒜 f f_deg hm).hom ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_1
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
⊢ 0 ∈ carrier f_deg q

Tactic:
exact carrier.zero_mem f_deg hm _

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
⊢ Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ i, ⋯⟩ =
    Localization.mk (a ^ m) ⟨f ^ n, ⋯⟩ * Localization.mk (↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ (i - n), ⋯⟩

Tactic:
rw [Localization.mk_mul]

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
⊢ Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ i, ⋯⟩ =
    Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) (⟨f ^ n, ⋯⟩ * ⟨f ^ (i - n), ⋯⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
⊢ j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e

Tactic:
cases d

Goal state after:
case e'_4.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
⊢ j * (0 * (e + 1)) = j * (0 + e) + (j * (0 - 1)) • e

case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * d), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d))) =
    x ^ (j * (e + 1)) * x ^ (j * d) * a

Tactic:
cases d

Goal state after:
case h.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (0 * (e + 1)), num := ⟨a * g ^ (j * (0 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (0 * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * 0), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (0 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
    x ^ (j * (e + 1)) * x ^ (j * 0) * a

case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) := ⋯
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅
  Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) := ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) := ⋯
this : Function.Surjective ⇑F
⊢ ((e₂.inv ≫
          ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1)
                  ((affineOpenCover 𝒜).openCover.f (i, j).2) (toSpecZero 𝒜)).inv ≫
              snd (diagonal (toSpecZero 𝒜))
                ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover
                      (toSpecZero 𝒜) (toSpecZero 𝒜)).f
                  (i, j))) ≫
            e₁.hom) ≫
        (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv) ≫
      fst (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))) =
    (Spec.map (CommRingCat.ofHom F) ≫ (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv) ≫
      fst (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd))))

Tactic:
simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id,
      limit.lift_π, PullbackCone.mk_π_app, e₂, e₁,
      pullbackSpecIso_inv_fst, ← Spec.map_comp]
    erw [pullbackDiagonalMapIdIso_inv_snd_fst]
    erw [pullbackAwayιIso_inv_fst]
    congr 1
    ext x : 2
    exact DFunLike.congr_fun (Algebra.TensorProduct.lift_comp_includeLeft
      (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) (fun _ _ ↦ .all _ _)).symm x

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

Goal state before:
pp: case h
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 : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom)
        ((ConcreteCategory.hom a) f ^ n •
          (AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op)) t))) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) 0
⊢ f ^ n • t = 0

Tactic:
← map_pow,

Goal state after:
case h
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 : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom)
        ((ConcreteCategory.hom a) (f ^ n) •
          (AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op)) t))) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) 0
⊢ f ^ n • t = 0
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
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
refine Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_
    rintro ⟨X₀, a, ha⟩
    dsimp
    simp only [assoc, ← Functor.map_comp]
    exact h ⟨_, _, ha⟩

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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve p₁ ⊓ F.imageSieve p₂, ⋯⟩),
    (presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫ G₀.obj.map I.f.op =
      (presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫ G₀.obj.map I.f.op

Tactic:
intro ⟨W₀, a, ⟨b₁, h₁⟩, ⟨b₂, h₂⟩⟩

Goal state after:
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
⊢ (presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op =
    (presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op