-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
s t : A
hs : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) s
ht : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) t
hs' :
  Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) s : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
ht' :
  Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) t : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
⊢ mk
      { deg := n,
        num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (s + t) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ } =
    HAdd.hAdd (α := Away 𝒜 f)
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) s : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) t : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
have h : val
    (mk
      { deg := n,
        num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (s + t) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }) =
  val
    (HAdd.hAdd (α := Away 𝒜 f)
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) s : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) t : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
Tactic: ext