mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
apply hφ

Goal state after:
case inr.inr.injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) =
    φ (r ^ (f.natDegree * g.natDegree) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Tactic:
apply hφ

Goal state after:
case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ φ (((taylor r) f).resultant ((taylor r) g)) = φ (f.resultant g)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
X G : C
f : X ⟶ G
inst✝ : GrpObj G
⊢ F.map (f⁻¹ * f) = 1

Tactic:
inv_mul_cancel,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
X G : C
f : X ⟶ G
inst✝ : GrpObj G
⊢ F.map 1 = 1
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
⊢ False

Tactic:
let fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 _) (Over.homMk c hc ≫ snd G G)

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 (𝟙_ (Over S))) (Over.homMk c hc ≫ snd G G)
⊢ False
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective (⇑hₐ.toLinearMap ∘ ⇑g)

Tactic:
apply hₐ.injective.comp

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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := ⋯
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := ⋯
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑g
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
⊢ IsOpenImmersion (colimit.ι F j).left

Tactic:
rw [← MorphismProperty.Over.forget_comp_forget_map]

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j))
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map (f ≫ 𝟙 b) = map f ≫ 𝟙 (obj b)

Tactic:
by rw [map_comp f (𝟙 b), map_id b]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
hf : Surjective f
hhomeo : IsHomeomorph ⇑f
this : QuasiCompact f
⊢ IsOpenImmersion f

Tactic:
have := Flat.isIso_of_surjective_of_mono f

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
hf : Surjective f
hhomeo : IsHomeomorph ⇑f
this✝ : QuasiCompact f
this : IsIso f
⊢ IsOpenImmersion f
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : R
ha : a ∈ R⁰
⊢ (ordMonoidWithZeroHom R) a ≠ 0

Tactic:
lift a to R⁰ using ha
  simp [← ordMonoidWithZeroHom_eq_ordMonoidHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
⊢ (ordHom x hx) ((ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

Tactic:
by
  have : Ring.KrullDimLE 1 (X.presheaf.stalk x) := krullDimLE_of_coheight_le hx.le
  rw [← algebraMap_germ_eq_germToFunctionField _ hx']
  exact Ring.ordFrac_of_isUnit (hf.map (X.presheaf.germ U x hx').hom)

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ Multiplicative.toAdd (Multiplicative.ofAdd n) ≤ Multiplicative.toAdd (unzero ⋯) ↔
    ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

Tactic:
Multiplicative.toAdd_le,

Goal state after:
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ Multiplicative.ofAdd n ≤ unzero ⋯ ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ R x) i) '' s) = ⊤
⊢ Ideal.span s = ⊤

Tactic:
by
  simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
    Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢
  choose f hf using hs'
  have : Fintype s := hs.fintype
  refine ⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩
  ext i
  simpa [Finsupp.sum_fintype] using hf i

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
f g : 𝒜 →+*ᵍ ℬ
h : (fun f ↦ (↑↑f.toRingHom).toFun) f = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ f = g

Tactic:
cases f
    cases g
    congr
    apply DFunLike.coe_injective
    exact h

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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ (mk (n • x✝)).val = n • val (Quotient.mk'' x✝)

Tactic:
val_mk,

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = n • val (Quotient.mk'' x✝)
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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = n • val (Quotient.mk'' x✝)

Tactic:
val_mk,

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = n • Localization.mk ↑x✝.num ⟨↑x✝.den, ⋯⟩
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ (mk (-y)).val = -val (Quotient.mk'' y)

Tactic:
val_mk,

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = -val (Quotient.mk'' y)
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = -val (Quotient.mk'' y)

Tactic:
val_mk,

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = -Localization.mk ↑y.num ⟨↑y.den, ⋯⟩
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (mk (y1 + y2)).val = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ = Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ + val (Quotient.mk'' y2)
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ = Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ + val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ + Localization.mk ↑y2.num ⟨↑y2.den, ⋯⟩
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (mk (y1 * y2)).val = val (Quotient.mk'' y1) * val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = val (Quotient.mk'' y1) * val (Quotient.mk'' y2)
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = val (Quotient.mk'' y1) * val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ * val (Quotient.mk'' y2)
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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ * val (Quotient.mk'' y2)

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ =
    Localization.mk ↑y1.num ⟨↑y1.den, ⋯⟩ * Localization.mk ↑y2.num ⟨↑y2.den, ⋯⟩
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
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (mk (y ^ n)).val = val (Quotient.mk'' y) ^ n

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = val (Quotient.mk'' y) ^ n
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
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = val (Quotient.mk'' y) ^ n

Tactic:
val_mk,

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 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk ↑y.num ⟨↑y.den, ⋯⟩ ^ n
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 : (mk f).val * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
val_mk,

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 : Localization.mk ↑f.num ⟨↑f.den, ⋯⟩ * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m), (algebraMap A (at Submonoid.powers f)) x = (f ^ (k' - k) * f ^ k) • val z

Tactic:
mul_smul,

Goal state after:
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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m), (algebraMap A (at Submonoid.powers f)) x = f ^ (k' - k) • f ^ k • val z