ι : 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 : HomogeneousLocalization 𝒜 x
this : Quotient.mk'' (Quotient.out' f) = f
⊢ val f = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
ι : 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 : HomogeneousLocalization 𝒜 x
⊢ val f = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
have := Quotient.out_eq' f
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val f = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
ι : 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 : HomogeneousLocalization 𝒜 x
this : Quotient.mk'' (Quotient.out' f) = f
⊢ val f = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
apply_fun HomogeneousLocalization.val at this
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val (Quotient.mk'' (Quotient.out' f)) = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val f = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
rw [← this]
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val (Quotient.mk'' (Quotient.out' f)) = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val (Quotient.mk'' (Quotient.out' f)) = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
simp only [Quotient.liftOn'_mk'']
no goals
ι : 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 : HomogeneousLocalization 𝒜 x
this : val (Quotient.mk'' (Quotient.out' f)) = val f
⊢ val (Quotient.mk'' (Quotient.out' f)) = Localization.mk (num f) { val := den f, property := (_ : den f ∈ x) }
rfl