-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ :
  ∀ (f g : C((↑s : Type), ℝ)₀),
    HMul.hMul (α := A) (β := A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            g :
          A) =
      0
mul₂ :
  ∀ (f g : C((↑s : Type), ℝ)₀),
    HMul.hMul (α := A) (β := A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            g :
          A) =
      0
ψ : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src :=
    HAdd.hAdd (α := C((↑s : Type), ℝ)₀ →ₗ[ℝ] A)
      (↑(cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
        [inst_12 : FunLike (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) C((↑s : Type), ℝ)₀ A] →
          [SemilinearMapClass (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) (RingHom.id ℝ) C((↑s : Type), ℝ)₀ A] →
            C((↑s : Type), ℝ)₀ →ₗ[ℝ] A)
      (↑(cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
        [inst_12 : FunLike (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) C((↑s : Type), ℝ)₀ A] →
          [SemilinearMapClass (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) (RingHom.id ℝ) C((↑s : Type), ℝ)₀ A] →
            C((↑s : Type), ℝ)₀ →ₗ[ℝ] A);
  {
    toFun :=
      HAdd.hAdd (α := (a : C((↑s : Type), ℝ)₀) → A)
        (⇑(cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
          (a : C((↑s : Type), ℝ)₀) → A)
        (⇑(cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
          (a : C((↑s : Type), ℝ)₀) → A),
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
f : C((↑s : Type), ℝ)₀ := { toFun := fun (x : (↑s : Type)) ↦ (↑x : ℝ)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ (R := ℝ) (p := IsSelfAdjoint)
      (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ a }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ a))
        (⇑(f.comp
              { toFun := Subtype.map (p := Membership.mem (σₙ ℝ a)) (q := Membership.mem s) id has,
                continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(σₙ ℝ a) : Type), (↑s : Type))₀ }) :
          (a : (↑(σₙ ℝ a) : Type)) → ℝ)
        fun (x : ℝ) ↦ x⁺)
      a =
    cfcₙ (R := ℝ) (p := IsSelfAdjoint)
        (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ b))
          (⇑(f.comp
                { toFun := Subtype.map (p := Membership.mem (σₙ ℝ b)) (q := Membership.mem s) id hbs,
                  continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(σₙ ℝ b) : Type), (↑s : Type))₀ }) :
            (a : (↑(σₙ ℝ b) : Type)) → ℝ)
          fun (x : ℝ) ↦ x⁺)
        b +
      cfcₙ (R := ℝ) (p := IsSelfAdjoint)
        (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ (-c) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ (-c)))
          (⇑(f.comp
                { toFun := Subtype.map (p := Membership.mem (σₙ ℝ (-c))) (q := Membership.mem s) id hcs,
                  continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(σₙ ℝ (-c)) : Type), (↑s : Type))₀ }) :
            (a : (↑(σₙ ℝ (-c)) : Type)) → ℝ)
          fun (x : ℝ) ↦ x⁺)
        (-c)
⊢ cfcₙ (R := ℝ) (p := IsSelfAdjoint) id b + cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 (-c) =
    cfcₙ (R := ℝ) (p := IsSelfAdjoint)
        (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ b))
          (⇑(f.comp
                { toFun := Subtype.map (p := Membership.mem (σₙ ℝ b)) (q := Membership.mem s) id hbs,
                  continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(σₙ ℝ b) : Type), (↑s : Type))₀ }) :
            (a : (↑(σₙ ℝ b) : Type)) → ℝ)
          fun (x : ℝ) ↦ x⁺)
        b +
      cfcₙ (R := ℝ) (p := IsSelfAdjoint)
        (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ (-c) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ (-c)))
          (⇑(f.comp
                { toFun := Subtype.map (p := Membership.mem (σₙ ℝ (-c))) (q := Membership.mem s) id hcs,
                  continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(σₙ ℝ (-c)) : Type), (↑s : Type))₀ }) :
            (a : (↑(σₙ ℝ (-c)) : Type)) → ℝ)
          fun (x : ℝ) ↦ x⁺)
        (-c)
have h : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id b =
  cfcₙ (R := ℝ) (p := IsSelfAdjoint)
    (Function.extend (α := { x : ℝ // x ∈ σₙ ℝ b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ σₙ ℝ b))
      (⇑(f.comp
            { toFun := Subtype.map (p := Membership.mem (σₙ ℝ b)) (q := Membership.mem s) id hbs, continuous_toFun := sorry,
              map_zero' := sorry }) :
        (a : (↑(σₙ ℝ b) : Type)) → ℝ)
      fun (x : ℝ) ↦ x⁺)
    b
Tactic: congr! 1