mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝² : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝¹ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
this✝ : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away (φ e))
this : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away ((ofId R' (Localization.Away e)) f))
equiv : Localization.Away (φ e) ≃ₐ[R' ⊗[R] S] Localization.Away ((ofId R' (Localization.Away e)) f) :=
  IsLocalization.algEquiv (Submonoid.powers (e * f ⊗ₜ[R] 1)) (Localization.Away (φ e))
    (Localization.Away ((ofId R' (Localization.Away e)) f))
⊢ (algebraMap (Localization.Away f)
          (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))).comp
      (algebraMap R' (Localization.Away f)) =
    ((↑↑equiv.symm).comp ↑(Localization.awayMapₐ (ofId R' (Localization.Away e)) f)).comp
      (algebraMap R' (Localization.Away f))

Tactic:
simp only [← IsScalarTower.algebraMap_eq, RingHom.comp_assoc, AlgHom.comp_algebraMap_of_tower]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(↑R h1Cotangentι)

pp: case hg₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.baseChange.cotangentComplex)

pp: case hi₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Surjective ⇑0

pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

pp: case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
· rw [LinearMap.exact_zero_iff_injective]
    simp only [LinearMap.coe_restrictScalars]
    exact h1Cotangentι_injective

Goal state after:
case hg₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.baseChange.cotangentComplex)

case hi₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Surjective ⇑0

case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ≫ ((algSpec R).obj X ⊗ (algSpec R).obj Y).hom =
    ((algSpec R).obj (X ⊗ Y)).hom

Tactic:
by
      simpa using Over.w (prodComparison (algSpec R) X Y)

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

Goal state before:
pp: case h₁
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
⊢ (Over.Hom.left
          (η ≫
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left η ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
simp [Scheme.monObjAsOverPullback_one, ε_algSpec_left (R := CommRingCat.of _),
        pullbackSpecIso', specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
        AlgHom.toUnder, Under.homMk_right,
        ← AlgHom.coe_restrictScalars R (Bialgebra.counitAlgHom S _), -AlgHom.coe_restrictScalars,
        ← AlgHom.comp_toRingHom, Bialgebra.counitAlgHom_comp_includeRight]

Goal state after:
case h₁
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
⊢ Spec.map (ofHom ((algebraMap R S).comp ↑(Bialgebra.counitAlgHom R T))) =
    Spec.map (ofHom ↑((Algebra.ofId R S).comp (Bialgebra.counitAlgHom R T)))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : Adj B
α β : a ⟶ b
p : Hom₂ α β
⊢ (conjugateEquiv β.adj α.adj).symm p.τr = p.τl

Tactic:
rw [← Hom₂.conjugateEquiv_τl, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : Flat f
inst✝ : IsFinite f
R : CommRingCat
i : Spec R ⟶ Y
w✝ : IsOpenImmersion i
y' : ↥(Spec R)
⊢ finrank (pullback.snd f g) (i y') = finrank f (g (i y'))

Tactic:
rw [← Scheme.Hom.comp_apply, finrank_eq_finrank_snd_of_isAffine,
    finrank_eq_finrank_snd_of_isAffine, ← pullbackLeftPullbackSndIso_hom_snd f g i,
    ← finrank_eq_of_isAffine, ← finrank_eq_of_isAffine, finrank_comp_left_of_isIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ IsIso φ

Tactic:
ConcreteCategory.isIso_iff_bijective

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: 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)) ⊤

pp: 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✝

pp: 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)) ⊤

pp: 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✝

Tactic:
on_goal 4 =>
        simp only [← ENat.natCast_add, ENat.recTopCoe_natCast, Nat.cast_add (R := ℤ),
          ofAdd_add, WithZero.coe_mul]

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✝

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)) ⊤
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsNoetherianRing R
inst✝⁴ : KrullDimLE 1 R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
⊢ (ordFrac R) ((algebraMap R K) x) = (ordMonoidWithZeroHom R) x

Tactic:
have := (FaithfulSMul.algebraMap_injective R K).isDomain

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsNoetherianRing R
inst✝⁴ : KrullDimLE 1 R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
this : IsDomain R
⊢ (ordFrac R) ((algebraMap R K) x) = (ordMonoidWithZeroHom R) x
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ zeroLocus (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ∅

Tactic:
← preimage_comap_zeroLocus,

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i) ⁻¹' zeroLocus t = ∅
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)

Tactic:
· rw [(isClosed_zeroLocus _ _).closure_subset_iff]
    exact subset_zeroLocus_vanishingIdeal 𝒜 t

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (pullbackComp f (𝟙 Y)).inv ≫ Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (pullback f).leftUnitor.hom =
    eqToHom ⋯

Tactic:
by
  let e₁ := pullbackComp f (𝟙 _)
  let e₂ := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
  let e₃ := (pullback f).leftUnitor
  change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
  have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_id_comp.{u} f.toRingCatSheafHom)
  simp [← this]

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

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d))) (⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩) = 1

Tactic:
rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]

Goal state after:
case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ ∃ c,
    ↑c * (↑(1, 1).2 * (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).1) =
      ↑c * (↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).2 * (1, 1).1)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case pos.e_a.e_x
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 := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m - j) * ↑(((decompose 𝒜) b) i) ^ m

Tactic:
mul_assoc,

Goal state after:
case pos.e_a.e_x
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 := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * (↑(((decompose 𝒜) b) i) ^ (m - j) * ↑(((decompose 𝒜) b) i) ^ m)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ M : ModuleCat ↑R
⊢ IsIso (ModuleCat.ofHom (StructureSheaf.toOpenₗ ↑R ↑M ⊤))

Tactic:
ConcreteCategory.isIso_iff_bijective

Goal state after:
R : CommRingCat
M✝ M : ModuleCat ↑R
⊢ Function.Bijective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (StructureSheaf.toOpenₗ ↑R ↑M ⊤)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
⊢ ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
            (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj).map
        i ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop g))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) =
    ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
      ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).map i

Tactic:
let N := (modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)

Goal state after:
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 ⊤)
⊢ ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
            (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj).map
        i ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop g))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) =
    ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
      ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).map i
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
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
⊢ ∑ x, ai x % d * dv x + ∑ x, d * (ai x / d) * dv x - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv x

Tactic:
mul_assoc,

Goal state after:
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
⊢ ∑ x, ai x % d * dv x + ∑ x, d * (ai x / d * dv x) - (∑ i, dv i * (ai i / d)) * d = ∑ x, ai x % d * dv x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e_x.e_f.e_a
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
i : ι'
⊢ ai i = ai i % d + d * (ai i / d)

Tactic:
exact Eq.symm (Nat.mod_add_div (ai i) d)

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

Goal state before:
pp: case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
      (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

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

Goal state after: