mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R (↑α * ϖ ^ m) = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)

Tactic:
rw [ord_mul, ord_pow, ord_of_irreducible hϖ]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ord R ↑α + m • 1 = (IsDiscreteValuationRing.addVal R) (↑α * ϖ ^ m)

case neg.hx
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ∈ nonZeroDivisors R

case neg.hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬↑α * ϖ ^ m = 0
⊢ ϖ ^ m ∈ nonZeroDivisors R
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x = 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
inf_le_iff,

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x = 1
⊢ ord f x ≤ ord (f + g) x ∨ ord g x ≤ ord (f + g) x
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ⊤ ≤ Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ)

Tactic:
← hF,

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ Algebra.adjoin ↥(𝒜 0) ↑F ≤ Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ)
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ Algebra.adjoin ↥(𝒜 0) ↑F ≤ Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ)

Tactic:
Algebra.adjoin_le_iff

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ↑F ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ Algebra.adjoin ↥(𝒜 0) ↑s ≤ Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0})

Tactic:
Algebra.adjoin_le_iff

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ↑s ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0}))
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_2
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, ⊤))
⊢ ∀ {X Y : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ} (f : X ⟶ Y),
    ((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.map
          f ≫
        ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj Y))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj Y))).hom =
      ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj X))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj X))).hom ≫
        ((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.map
          f

Tactic:
· cat_disch

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

Goal state before:
pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (f : X ⟶ Y),
    (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))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom ≫
        (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 φ))).map
          f

Tactic:
· cat_disch

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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : IsLocalization.mk' (at 𝔭.primeCompl) (↑f.num * b) (⟨↑f.den, ⋯⟩ * s) = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
IsLocalization.mk'_eq_iff_eq_mul,

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 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : (algebraMap A (at 𝔭.primeCompl)) (↑f.num * b) = 1 * (algebraMap A (at 𝔭.primeCompl)) ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_3
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
⊢ ∀ {X_1 Y : TopologicalSpace.Opens ↥↑V} (f_1 : X_1 ⟶ Y),
    (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).map f_1 ≫ (Over.isoMk (eqToIso ⋯) ⋯).hom =
      (Over.isoMk (eqToIso ⋯) ⋯).hom ≫ ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).map f_1

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Goal state before:
pp: case smul
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a₁ a₂ : B
ha₂ : a₂ ∈ Submodule.span B (⇑f '' ↑I.toIdeal)
ih : ∀ (i : ι), ↑(((DirectSum.decompose ℬ) a₂) i) ∈ Ideal.map f I.toIdeal
i : ι
⊢ ∑ ij ∈ DFinsupp.support ((DirectSum.decompose ℬ) a₁) ×ˢ DFinsupp.support ((DirectSum.decompose ℬ) a₂) with
      ij.1 + ij.2 = i, ↑(((DirectSum.decompose ℬ) a₁) ij.1) * ↑(((DirectSum.decompose ℬ) a₂) ij.2) ∈
    Ideal.map f I.toIdeal

Tactic:
exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _

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

Goal state before:
pp: 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
⊢ Algebra.adjoin ↥(𝒜 0)
      {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:
by
  rw [← top_le_iff]
  change ⊤ ≤ (Algebra.adjoin (𝒜 0) _).toSubmodule
  rw [← HomogeneousLocalization.Away.span_mk_prod_pow_eq_top hf v hx dv hxd, Submodule.span_le]
  rintro _ ⟨a, ai, hai, rfl⟩
  have H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k := by
    rw [smul_eq_mul, tsub_mul, ← smul_eq_mul, ← hai]
    conv => enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
    simp_rw [smul_eq_mul, add_mul, Finset.sum_add_distrib,
      mul_assoc, ← Finset.mul_sum, mul_comm d, mul_comm (_ / _)]
    simp only [add_tsub_cancel_right]
  have H : Away.mk 𝒜 hf a (∏ i, v i ^ ai i)
      (hai ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) =
      Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i, v i ^ (ai i % d))
      (H₀ ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) *
      ∏ i, Away.isLocalizationElem hf (hxd i) ^ (ai i / d) := by
    apply (show Function.Injective (algebraMap (Away 𝒜 f) (Localization.Away f))
      from val_injective _)
    simp only [map_pow, map_prod, map_mul]
    simp only [HomogeneousLocalization.algebraMap_apply, val_mk,
      Localization.mk_pow, Localization.mk_prod, Localization.mk_mul,
      ← Finset.prod_mul_distrib, ← pow_add, ← pow_mul]
    congr
    · ext i
      congr
      exact Eq.symm (Nat.mod_add_div (ai i) d)
    · simp only [SubmonoidClass.coe_finsetProd, ← pow_add, ← pow_mul,
        Finset.prod_pow_eq_pow_sum, SubmonoidClass.coe_pow]
      rw [tsub_add_cancel_of_le]
      rcases d.eq_zero_or_pos with hd | hd
      · simp [hd]
      rw [← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul (a := a), ← hai, Finset.sum_mul]
      simp_rw [smul_eq_mul, mul_comm (ai _), mul_assoc]
      gcongr
      exact Nat.div_mul_le_self (ai _) d
  rw [H, SetLike.mem_coe]
  apply (Algebra.adjoin (𝒜 0) _).mul_mem
  · apply Algebra.subset_adjoin
    refine ⟨a - ∑ i : ι', dv i * (ai i / d), (ai · % d), H₀.symm, ?_, rfl⟩
    rcases d.eq_zero_or_pos with hd | hd
    · have : ∀ (x : ι'), ai x = 0 := by simpa [hd, fun i ↦ (hxd' i).ne'] using hai
      simp [this]
    exact fun i ↦ (Nat.mod_lt _ hd).le
  apply prod_mem
  · classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]

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

Goal state before:
pp: R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
f : ↑R
⊢ IsIso (φ.hom.app (op (basicOpen f)))

Tactic:
refine ModuleCat.isIso_of_isLocalizedModule_comp (hM f) ?_

Goal state after:
R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom (M.obj.map (basicOpen f).leTop.op ≫ φ.hom.app (op (basicOpen f))))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case refine_2.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)
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, (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i • dv i = a • d

Tactic:
simpa [Finset.sum_attach_eq_sum_dite] using hai

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

Goal state before:
pp: case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))

Tactic:
let u := X.homOfLE (U := i.2) (V := W i.1) (by simp [heq, le_sSup])

Goal state after:
case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
u : ↑↑i.snd ⟶ ↑(W i.fst) := X.homOfLE ⋯
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

Tactic:
Algebra.adjoin_le_iff

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
⊢ False

Tactic:
obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)

Goal state after:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ False
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
i : (𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f i)

Tactic:
induction i

Goal state after:
case inl
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : 𝒰.ulift.I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inl val✝))

case inr
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inr val✝))