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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ ^ n) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) ^ n
ι : 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
n : ℕ
⊢ val (y ^ n) = val y ^ n
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ ^ n) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) ^ n
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ ^ n) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) ^ n
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑((fun x_1 => x_1 ^ n) a✝).num
      { val := ↑((fun x_1 => x_1 ^ n) a✝).den, property := (_ : ↑((fun x_1 => x_1 ^ n) a✝).den ∈ x) } =
    Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ ^ n) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) ^ n
change Localization.mk _ _ = Localization.mk _ _ ^ n
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑((fun x_1 => x_1 ^ n) a✝).num
      { val := ↑((fun x_1 => x_1 ^ n) a✝).den, property := (_ : ↑((fun x_1 => x_1 ^ n) a✝).den ∈ x) } =
    Localization.mk (↑a✝.num ^ n) ({ val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n)
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑((fun x_1 => x_1 ^ n) a✝).num
      { val := ↑((fun x_1 => x_1 ^ n) a✝).den, property := (_ : ↑((fun x_1 => x_1 ^ n) a✝).den ∈ x) } =
    Localization.mk ↑a✝.num { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n
rw [Localization.mk_pow]
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(a✝ ^ n).num { val := ↑(a✝ ^ n).den, property := (_ : ↑(a✝ ^ n).den ∈ x) } =
    Localization.mk (↑a✝.num ^ n) ({ val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n)
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑((fun x_1 => x_1 ^ n) a✝).num
      { val := ↑((fun x_1 => x_1 ^ n) a✝).den, property := (_ : ↑((fun x_1 => x_1 ^ n) a✝).den ∈ x) } =
    Localization.mk (↑a✝.num ^ n) ({ val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n)
dsimp only
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
n : ℕ
a✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(a✝ ^ n).num { val := ↑(a✝ ^ n).den, property := (_ : ↑(a✝ ^ n).den ∈ x) } =
    Localization.mk (↑a✝.num ^ n) ({ val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) } ^ n)
congr 1