-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop} (htfae : h → [p1, p2, p3].TFAE), [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
refine_1 :
  ∀ (h : Subsingleton V),
    List.TFAE
      [∀ (x : Finsupp.{u_2, u_3} X (V →L[𝕜] V)) (x_1 : V),
          LE.le (α := ℝ) (0 : ℝ)
            ((RCLike.re : (a : 𝕜) → ℝ)
                (x.sum fun (i : X) (a : V →L[𝕜] V) ↦
                  x.sum fun (i_1 : X) (a_1 : V →L[𝕜] V) ↦
                    inner 𝕜 (E := V) ((K i i_1 : (a : V) → V) ((a_1 : (a : V) → V) x_1 : V) : V)
                      ((a : (a : V) → V) x_1 : V)) :
              ℝ),
        ∀ (f : X × V →₀ 𝕜),
          LE.le (α := ℝ) (0 : ℝ)
            ((RCLike.re : (a : 𝕜) → ℝ)
                (f.sum fun (xv : X × V) (z : 𝕜) ↦
                  f.sum fun (xv' : X × V) (w : 𝕜) ↦
                    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) w *
                      ⟪(K xv'.1 xv.1 : (a : V) → V) xv.2, xv'.2⟫_𝕜) :
              ℝ),
        ∀ (vv : X →₀ V),
          LE.le (α := ℝ) (0 : ℝ)
            ((RCLike.re : (a : 𝕜) → ℝ)
                (vv.sum fun (x : X) (w : V) ↦ vv.sum fun (x' : X) (w' : V) ↦ ⟪(K x' x : (a : V) → V) w, w'⟫_𝕜) :
              ℝ)]
⊢ List.TFAE
    [∀ (x : Finsupp.{u_2, u_3} X (V →L[𝕜] V)) (x_1 : V),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (x.sum fun (i : X) (a : V →L[𝕜] V) ↦
                x.sum fun (i_1 : X) (a_1 : V →L[𝕜] V) ↦
                  inner 𝕜 (E := V) ((K i i_1 : (a : V) → V) ((a_1 : (a : V) → V) x_1 : V) : V)
                    ((a : (a : V) → V) x_1 : V)) :
            ℝ),
      ∀ (f : X × V →₀ 𝕜),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (f.sum fun (xv : X × V) (z : 𝕜) ↦
                f.sum fun (xv' : X × V) (w : 𝕜) ↦
                  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) w *
                    ⟪(K xv'.1 xv.1 : (a : V) → V) xv.2, xv'.2⟫_𝕜) :
            ℝ),
      ∀ (vv : X →₀ V),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (vv.sum fun (x : X) (w : V) ↦ vv.sum fun (x' : X) (w' : V) ↦ ⟪(K x' x : (a : V) → V) w, w'⟫_𝕜) :
            ℝ)]
have refine_2 : Nontrivial V →
  List.TFAE
    [∀ (x : Finsupp.{u_2, u_3} X (V →L[𝕜] V)) (x_1 : V),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (x.sum fun (i : X) (a : V →L[𝕜] V) ↦
                x.sum fun (i_1 : X) (a_1 : V →L[𝕜] V) ↦
                  inner 𝕜 (E := V) ((K i i_1 : (a : V) → V) ((a_1 : (a : V) → V) x_1 : V) : V)
                    ((a : (a : V) → V) x_1 : V)) :
            ℝ),
      ∀ (f : X × V →₀ 𝕜),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (f.sum fun (xv : X × V) (z : 𝕜) ↦
                f.sum fun (xv' : X × V) (w : 𝕜) ↦
                  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) w *
                    ⟪(K xv'.1 xv.1 : (a : V) → V) xv.2, xv'.2⟫_𝕜) :
            ℝ),
      ∀ (vv : X →₀ V),
        LE.le (α := ℝ) (0 : ℝ)
          ((RCLike.re : (a : 𝕜) → ℝ)
              (vv.sum fun (x : X) (w : V) ↦ vv.sum fun (x' : X) (w' : V) ↦ ⟪(K x' x : (a : V) → V) w, w'⟫_𝕜) :
            ℝ)]
Tactic: refine (subsingleton_or_nontrivial V).elim (fun h ↦ ?_) fun _ ↦ ?_