case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ val (-Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) = -val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝)
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
y : HomogeneousLocalization 𝒜 x
⊢ val (-y) = -val y
induction y using Quotient.inductionOn
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ val (-Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) = -val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝)
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ val (-Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) = -val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝)
simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    -Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ val (-Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) = -val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝)
change Localization.mk _ _ = -Localization.mk _ _
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    -Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    -Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
dsimp only
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    Localization.mk (-↑a✝.num) { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    -Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
rw [Localization.neg_mk]
no goals
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-a✝).num { val := ↑(-a✝).den, property := (_ : ↑(-a✝).den ∈ x) } =
    Localization.mk (-↑a✝.num) { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) }
rfl