Maximal-domain composition of a partial operator with its adjoint

import Mathlib.Analysis.InnerProductSpace.LinearPMap

noncomputable section
open scoped LinearPMap
namespace FunctionalInequalities
namespace Analysis
namespace Semigroup
variable {H₀ H₁ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℝ H₀] [CompleteSpace H₀]
  [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁]
/-- The domain of `T†T`, as a submodule of `H₀`: those `x ∈ D(T)` with `T x ∈ D(T†)`. -/
def adjointCompDomain (T : H₀ →ₗ.[ℝ] H₁) : Submodule ℝ H₀ :=
  (Submodule.comap T.toFun T†.domain).map T.domain.subtype
/-- Membership in the domain of `T†T`. -/
theorem mem_adjointCompDomain {T : H₀ →ₗ.[ℝ] H₁} {x : H₀} :
    x ∈ adjointCompDomain T ↔ ∃ hx : x ∈ T.domain, T ⟨x, hx⟩ ∈ T†.domain := by
  constructor
  · rintro ⟨⟨y, hy⟩, h, rfl⟩
    exact ⟨hy, h⟩
  · rintro ⟨hx, h⟩
    exact ⟨⟨x, hx⟩, h, rfl⟩
/-- On the restricted domain, `T` takes values in `D(T†)`; this is the side condition that
`LinearPMap.comp` demands. -/
theorem domRestrict_mem_adjoint_domain (T : H₀ →ₗ.[ℝ] H₁)
    (x : ↥(adjointCompDomain T ⊓ T.domain)) :
    T.domRestrict (adjointCompDomain T) x ∈ T†.domain := by
  obtain ⟨hx, h⟩ := mem_adjointCompDomain.mp x.2.1
  rw [T.domRestrict_apply (y := ⟨x, hx⟩) rfl]
  exact h
/-- `T†T` with its maximal domain `{x ∈ D(T) | T x ∈ D(T†)}`. -/
def adjointComp (T : H₀ →ₗ.[ℝ] H₁) : H₀ →ₗ.[ℝ] H₀ :=
  T†.comp (T.domRestrict (adjointCompDomain T)) (domRestrict_mem_adjoint_domain T)
/-- `adjointComp T x = T† (T x)`. -/
theorem adjointComp_apply (T : H₀ →ₗ.[ℝ] H₁) (x : (adjointComp T).domain) :
    adjointComp T x = T† ⟨T ⟨x, x.2.2⟩,
      by simpa [T.domRestrict_apply (y := ⟨x, x.2.2⟩) rfl] using domRestrict_mem_adjoint_domain T x⟩ := by
  change T† ⟨T.domRestrict (adjointCompDomain T) x, _⟩ = _
  congr 1
end Semigroup
end Analysis
end FunctionalInequalities