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
g : HomogeneousLocalization 𝒜 x
a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝) = val g
⊢ Quotient.mk'' a✝ = g
ι : 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
f g : HomogeneousLocalization 𝒜 x
h : val f = val g
⊢ f = g
induction f using Quotient.inductionOn'
case h.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✝¹ a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝¹) = val (Quotient.mk'' a✝)
⊢ Quotient.mk'' a✝¹ = Quotient.mk'' 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
g : HomogeneousLocalization 𝒜 x
a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝) = val g
⊢ Quotient.mk'' a✝ = g
induction g using Quotient.inductionOn'
case h.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✝¹ a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝¹) = val (Quotient.mk'' a✝)
⊢ Setoid.r a✝¹ a✝
case h.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✝¹ a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝¹) = val (Quotient.mk'' a✝)
⊢ Quotient.mk'' a✝¹ = Quotient.mk'' a✝
rw [Quotient.eq'']
no goals
case h.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✝¹ a✝ : NumDenSameDeg 𝒜 x
h : val (Quotient.mk'' a✝¹) = val (Quotient.mk'' a✝)
⊢ Setoid.r a✝¹ a✝
simpa only [Quotient.liftOn'_mk] using h