-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
inst_4 : DecidableEq ι
inst_5 : AddMonoid ι
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_8 : GradedRing 𝒜
inst_9 : GradedRing ℬ
F : Type u_10
inst_10 : FunLike F A B
inst_11 : GradedFunLike F 𝒜 ℬ
inst_12 : RingHomClass F A B
f : F
x : A
rw :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
rw₁ :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        (∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
          (f : (a : A) → B)
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A)) :
      ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
rw₂ :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
        (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
          ((f : (a : A) → B)
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) :
      ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))) :
      ⨁ (i : ι), ↥(ℬ i))
rw₃ :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
        (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
      (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
        (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
rw₄ rw₅ rw₆ :
  Eq (α := ⨁ (i : ι), ↥(ℬ i))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
      (map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A)))
e_f :
  Eq (α := ι → ⨁ (i : ι), ↥(ℬ i))
    (fun (i : ι) ↦
      (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i))
        ((f : (a : A) → B)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)))
    fun (x_1 : ι) ↦
    (map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
        (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x_1) : A))
⊢ Eq (α := ⨁ (i : ι), ↥(ℬ i)) ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) ((f : (a : A) → B) x) : ⨁ (i : ι), ↥(ℬ i))
    ((map (α := fun (i : ι) ↦ ↥(𝒜 i)) (β := fun (i : ι) ↦ ↥(ℬ i)) (GradedRingHom.gradedAddHom (↑f : 𝒜 →+*ᵍ ℬ)) :
          (a : ⨁ (i : ι), ↥(𝒜 i)) → ⨁ (i : ι), ↥(ℬ i))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) :
      ⨁ (i : ι), ↥(ℬ i))

Tactic:
classical
  rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]
  congr 1
  simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
    DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]

Premises used: DirectSum.decompose_of_mem, DirectSum.map_of, map_sum, Graded.map_mem, Subtype.prop, GradedRingHom.gradedAddHom, DirectSum.decompose_sum