-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
simp :
  Quotient.mk''
      { deg := (x + y).deg,
        num :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.num : A) : B) +
              HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑y.den : A) : B) ((g : (a : A) → B) (↑x.num : A) : B))
            ⋯,
        den :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) ⋯,
        den_mem := ⋯ } =
    mk
      (HAdd.hAdd (α := NumDenSameDeg ℬ Q)
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q }
        { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) ⋯,
          den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q })
⊢ Quotient.map'
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ (HAdd.hAdd (α := HomogeneousLocalization 𝒜 P) (Quotient.mk'' x) (Quotient.mk'' y)) =
    HAdd.hAdd (α := HomogeneousLocalization ℬ Q)
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' y))

Tactic:
simp only [← mk_add, Quotient.map'_mk'', num_add, map_add, map_mul, den_add]

Premises used: HomogeneousLocalization.NumDenSameDeg.den_add, map_add, map_mul, Quotient.map'_mk'', HomogeneousLocalization.NumDenSameDeg.num_add, HomogeneousLocalization.mk_add