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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FinitePresentation T (T ⊗[R] S)
this : FiniteType R S
⊢ FinitePresentation R S

Tactic:
rw [Algebra.FiniteType.iff_quotient_mvPolynomial''] at this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FinitePresentation T (T ⊗[R] S)
this : ∃ n f, Function.Surjective ⇑f
⊢ FinitePresentation R S
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
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
⊢ False

Tactic:
rw! [

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
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
⊢ False
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b : B
f g h i : a ⟶ b
inst✝ : BicategoricalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
simp [ih_η, ih_θ, bicategoricalIsoComp, bicategoricalComp]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p p (ofId R R) ⋯)

Tactic:
rw! [

Goal state after:
case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p p (ofId R R) ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun γ ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun β ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    β

Tactic:
by
    calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := by
        rw [adj.right_triangle]
        bicategory

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_cases hr' : Ideal.span {r} = ⊤

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R
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
⊢ I ≤ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker

pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I

Tactic:
· have : Submodule.map (mul R R a) I = a • I := rfl
    rw [le_ker_iff_map, Submodule.map_comp, this, 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
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

Tactic:
cases y'

Goal state after:
case pos.top.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

case pos.top.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

Tactic:
cases y'

Goal state after:
case pos.coe.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

case pos.coe.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝¹ a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝¹ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝¹ *
      ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

Tactic:
by_cases hx : x = 0
  · simp only [ord, hx, AddValuation.map_zero]
    subst hx
    by_contra!
    rw [Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at this
    have art := this.2
    rw [Ideal.span_singleton_zero] at art
    have : IsArtinianRing R :=
      (LinearEquiv.isArtinian_iff (Submodule.quotEquivOfEqBot ⊥ rfl).symm).mpr art
    exact IsDiscreteValuationRing.not_krullDimLE_zero R inferInstance
  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible R
  obtain ⟨m, α, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx hϖ
  rw [ord_mul, ord_pow, ord_of_irreducible hϖ]
  · simp [IsDiscreteValuationRing.addVal_uniformizer hϖ]
  all_goals simp_all [Irreducible.ne_zero hϖ]

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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa only [Equiv.apply_symm_apply] using this
  infer_instance

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 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑(vanishingIdeal {x}) ⊆ ↑y.asHomogeneousIdeal

Tactic:
vanishingIdeal_singleton

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
⊢ f = g

Tactic:
apply SheafOfModules.hom_ext
  ext U x
  exact congr($(H U.unop) x)

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
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
by
  rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one,
    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_under,
    IsLocalization.under_map_of_isPrime_disjoint (.powers f)]
  · rfl
  · infer_instance
  · exact (disjoint_powers_iff_notMem_of_isPrime _).mpr x.2
  · exact isUnit_of_invertible _

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
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
        X.ringCatSheaf =
    𝟙 X.ringCatSheaf

Tactic:
ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]

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
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (f ≫ g) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Z)).app
        Z.ringCatSheaf =
    {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
            (Opens.grothendieckTopology ↥Y)).map
        {
          hom :=
            Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
              (forget₂ CommRingCat RingCat) }

Tactic:
ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ mk { deg := 0, num := f * g, den := 1, den_mem := ⋯ } =
    mk { deg := 0, num := f, den := 1, den_mem := ⋯ } * mk { deg := 0, num := g, den := 1, den_mem := ⋯ }

Tactic:
ext; simp [Localization.mk_mul]

Goal state after:
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
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
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
convert! zero_mem (Submodule.span (𝒜 0) _)
      ext
      have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
      simp [this, Localization.mk_zero]

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

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
        ↑x)

Tactic:
rw [Subtype.forall]

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop f)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

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

Tactic:
rw [Subtype.forall]

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop f)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop r))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑x)

Tactic:
rw [Subtype.forall]

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop r))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑x)

Tactic:
rw [Subtype.forall]

Goal state after:
case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ ∃ n t, f ^ n • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t

Tactic:
use n, ψ t'

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := ⋯
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ f ^ n • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (ψ t')
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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } *
      HomogeneousLocalization.mk { deg := m * ny, num := ⟨y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } =
    HomogeneousLocalization.mk
      { deg := m * (nx + ny), num := ⟨x ^ m * y ^ m, ⋯⟩, den := ⟨f ^ nx * f ^ ny, ⋯⟩, den_mem := ⋯ }

Tactic:
simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_mul, 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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ Localization.mk (x ^ m * y ^ m) (⟨f ^ nx, ⋯⟩ * ⟨f ^ ny, ⋯⟩) = Localization.mk (x ^ m * y ^ m) ⟨f ^ nx * f ^ ny, ⋯⟩
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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ Localization.mk (x ^ m * y ^ m) (⟨f ^ nx, ⋯⟩ * ⟨f ^ ny, ⋯⟩) = Localization.mk (x ^ m * y ^ m) ⟨f ^ nx * f ^ ny, ⋯⟩

Tactic:
simp only [Submonoid.mk_mul_mk, mk_eq_monoidOf_mk']

Goal state after: