-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, ⋯⟩ : Fin pb.dim) :
            A)
          ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
        ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
          HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
            ((pb.basis : (a : Fin pb.dim) → B) x : B)) =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
have inr : HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, sorry⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, sorry⟩ : Fin pb.dim) : B)))
    (Submodule.Quotient.mk
      (∑ x ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B))) =
  HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
    HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
        ((algebraMap A B : (a : A) → B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, sorry⟩ : Fin pb.dim) :
            A)) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
Tactic: rw [Quotient.mk_add]