-- 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)
b₁ : b = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id b + cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 (-c)
b₂ :
  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)
⊢ b = a⁺
have b₃ : 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 := sorry,
              map_zero' := sorry : C((↑(σₙ ℝ a) : Type), (↑s : Type))₀ }) :
        (a : (↑(σₙ ℝ a) : Type)) → ℝ)
      fun (x : ℝ) ↦ x⁺)
    a =
  a⁺
Tactic: calc
    b = cfcₙ (id : ℝ → ℝ) b + cfcₙ (0 : ℝ → ℝ) (-c) := by simp [cfcₙ_id ℝ b]
    _ = _ := by
      congr! 1
      all_goals
        refine cfcₙ_congr fun x hx ↦ Eq.symm ?_
        lift x to σₙ ℝ _ using hx
        simp only [Subtype.val_injective.extend_apply, comp_apply, coe_mk,
          ContinuousMap.coe_mk, Subtype.map_coe, id_eq, _root_.posPart_eq_self, f, Pi.zero_apply,
          posPart_eq_zero]
      · exact quasispectrum_nonneg_of_nonneg b hb x.val x.property
      · obtain ⟨x, hx⟩ := x
        simp only [← neg_nonneg]
        rw [Unitization.quasispectrum_eq_spectrum_inr ℝ (-c), Unitization.inr_neg,
          ← spectrum.neg_eq, Set.mem_neg, ← Unitization.quasispectrum_eq_spectrum_inr ℝ c]
          at hx
        exact quasispectrum_nonneg_of_nonneg c hc _ hx
    _ = _ := key.symm
    _ = a⁺ := by
      refine cfcₙ_congr fun x hx ↦ ?_
      lift x to σₙ ℝ a using hx
      simp [f]