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
y2 : HomogeneousLocalization 𝒜 x
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ * y2) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) * val y2
ι : 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
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ val (y1 * y2) = val y1 * val y2
induction y1 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
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹ * Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) =
    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
y2 : HomogeneousLocalization 𝒜 x
a✝ : NumDenSameDeg 𝒜 x
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝ * y2) = val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) * val y2
induction y2 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
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹ * Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) =
    val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹) * val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) 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
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹ * Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) =
    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.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
⊢ Localization.mk ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).num
      { val := ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).den,
        property := (_ : ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).den ∈ 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.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
⊢ val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹ * Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝) =
    val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝¹) * val (Quotient.mk (Setoid.ker (embedding 𝒜 x)) a✝)
change Localization.mk _ _ = Localization.mk _ _ * Localization.mk _ _
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
⊢ Localization.mk ↑(a✝¹ * a✝).num { val := ↑(a✝¹ * a✝).den, property := (_ : ↑(a✝¹ * a✝).den ∈ 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.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
⊢ Localization.mk ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).num
      { val := ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).den,
        property := (_ : ↑((fun x_1 x_2 => x_1 * x_2) a✝¹ a✝).den ∈ 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.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
⊢ Localization.mk ↑(a✝¹ * a✝).num { val := ↑(a✝¹ * a✝).den, property := (_ : ↑(a✝¹ * a✝).den ∈ x) } =
    Localization.mk (↑a✝¹.num * ↑a✝.num)
      ({ val := ↑a✝¹.den, property := (_ : ↑a✝¹.den ∈ x) } * { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) })
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
⊢ Localization.mk ↑(a✝¹ * a✝).num { val := ↑(a✝¹ * a✝).den, property := (_ : ↑(a✝¹ * a✝).den ∈ 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.mk_mul]
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
⊢ Localization.mk ↑(a✝¹ * a✝).num { val := ↑(a✝¹ * a✝).den, property := (_ : ↑(a✝¹ * a✝).den ∈ x) } =
    Localization.mk (↑a✝¹.num * ↑a✝.num)
      ({ val := ↑a✝¹.den, property := (_ : ↑a✝¹.den ∈ x) } * { val := ↑a✝.den, property := (_ : ↑a✝.den ∈ x) })
rfl