-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : E),
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          y⟫ =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          x⟫
simp_rw₁ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
simp_rw₂ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
simp_rw₃ :
  (∀ (x y : E), True) ∧
    ∀ (x : E),
      0 ≤
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)⟫
simp_rw₄ :
  (∀ (x y : E), True) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw₅ : (∀ (x y : E), True) ∧
  ∀ (x : E),
    0 ≤
      inner 𝕜 (E := E) ((U.starProjection : (a : E) → E) x : E)
        ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E)
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]