-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (hypothesis)
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
h : Nontrivial V
v : V
hv : v ≠ 0
tfae_1_to_2 :
  ∀
    (a :
      ∀ (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⟫_𝕜) :
        ℝ)
tfae_2_to_3 :
  ∀
    (a :
      ∀ (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 tfae_3_to_1 : ∀
  (a :
    ∀ (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'⟫_𝕜) :
          ℝ))
  (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)) :
      ℝ)
Tactic: tfae_have 3 → 1 := fun h ff v ↦ by
    rw [Finsupp.sum_comm]
    simpa [Finsupp.sum_sum_index, inner_add_right, inner_add_left] using
      h (ff.sum fun x T ↦ .single x (T v))