awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
⊢ Eq (α := V →L[𝕜] V)
    (s.sum fun (i : X) (m : V →L[𝕜] V) ↦
      star (fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj) i m)
    (s.sum fun (x' : X) (v' : V →L[𝕜] V) ↦ s.sum fun (x : X) (v : V →L[𝕜] V) ↦ star v * kernel H x x' * v')

Tactic:
simp [← mul_assoc, (isHermitian_kernel H).apply]

Premises used: Matrix.IsHermitian.apply, mul_assoc, RKHS.isHermitian_kernel
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
v : V
refine_2 :
  LE.le.{u_1} (α := 𝕜) 0
    (s.sum fun (i : X) (a : V →L[𝕜] V) ↦
      s.sum fun (i_1 : X) (a_1 : V →L[𝕜] V) ↦
        inner.{u_1, u_4} 𝕜 (E := H) ((kerFun H i_1 : (a : V) → H) ((a_1 : (a : V) → V) v : V) : H)
          ((kerFun H i : (a : V) → H) ((a : (a : V) → V) v : V) : H))
⊢ 0 ≤
    ⟪(HSub.hSub (α := V →L[𝕜] V)
            (s.sum fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj) 0 :
          (a : V) → V)
        v,
      v⟫_𝕜

Tactic:
simp [Finsupp.sum_apply'', Finsupp.sum_inner, star, adjoint_inner_left,
      kernel_inner, -inner_kerFun, -kerFun_inner]

Premises used: Finsupp.sum_inner, ContinuousLinearMap.adjoint_inner_left, Finsupp.sum_apply'', RKHS.inner_kerFun, RKHS.kerFun_inner, RKHS.kernel_inner, Star.star
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
v : V
⊢ LE.le.{u_1} (α := 𝕜) 0
    (s.sum fun (i : X) (a : V →L[𝕜] V) ↦
      s.sum fun (i_1 : X) (a_1 : V →L[𝕜] V) ↦
        inner.{u_1, u_4} 𝕜 (E := H) ((kerFun H i_1 : (a : V) → H) ((a_1 : (a : V) → V) v : V) : H)
          ((kerFun H i : (a : V) → H) ((a : (a : V) → V) v : V) : H))

Tactic:
simp [← Finsupp.sum_inner, ← Finsupp.inner_sum, -kerFun_inner, -inner_kerFun]

Premises used: Finsupp.sum_inner, Finsupp.inner_sum, RKHS.inner_kerFun, RKHS.kerFun_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h : K.IsHermitian
f : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
simp :
  Eq (α := V →L[𝕜] V)
    (f.sum fun (i : X) (m : V →L[𝕜] V) ↦ f.sum fun (i_1 : X) (m_1 : V →L[𝕜] V) ↦ star m_1 * (K i_1 i * m))
    (f.sum fun (i : X) (xi : V →L[𝕜] V) ↦ f.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * (K i j * xj))
⊢ IsSelfAdjoint (R := V →L[𝕜] V)
    (f.sum fun (i : X) (xi : V →L[𝕜] V) ↦ f.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * K i j * xj)

Tactic:
simp only [mul_assoc, isSelfAdjoint_iff, star_finsuppSum, Pi.star_apply, star_mul, h.apply,
    star_star]

Premises used: star_star, Matrix.IsHermitian.apply, mul_assoc, Pi.star_apply, StarMul.star_mul, isSelfAdjoint_iff, star_finsuppSum
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h : K.IsHermitian
f : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
rw rw₁ :
  Eq (α := V →L[𝕜] V) (f.sum fun (x' : X) (v' : V →L[𝕜] V) ↦ f.sum fun (x : X) (v : V →L[𝕜] V) ↦ star v' * (K x' x * v))
    (f.sum fun (i : X) (xi : V →L[𝕜] V) ↦ f.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * (K i j * xj))
⊢ Eq (α := V →L[𝕜] V)
    (f.sum fun (i : X) (m : V →L[𝕜] V) ↦ f.sum fun (i_1 : X) (m_1 : V →L[𝕜] V) ↦ star m_1 * (K i_1 i * m))
    (f.sum fun (i : X) (xi : V →L[𝕜] V) ↦ f.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * (K i j * xj))

Tactic:
rw [Finsupp.sum_comm]

Premises used: Finsupp.sum_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
⊢ h ∧ p1

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
⊢ h ∧ p2

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
⊢ ∀ (a : h ∧ p1), h ∧ p2

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
⊢ ∀ (a : h ∧ p1), h ∧ p2

Tactic:
tfae_have 1 → 2 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 0 1).mp t⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
⊢ h ∧ p2

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
⊢ h ∧ p3

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
⊢ ∀ (a : h ∧ p2), h ∧ p3

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
⊢ ∀ (a : h ∧ p2), h ∧ p3

Tactic:
tfae_have 2 → 3 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 1 2).mp t⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
⊢ h ∧ p3

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
⊢ h ∧ p1

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
⊢ ∀ (a : h ∧ p3), h ∧ p1

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
⊢ ∀ (a : h ∧ p3), h ∧ p1

Tactic:
tfae_have 3 → 1 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 2 0).mp t⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
tfae_3_to_1 : ∀ (a : h ∧ p3), h ∧ p1
⊢ [h ∧ p1, h ∧ p2, h ∧ p3].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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)
⊢ ∀ {h p1 p2 p3 : Prop} (htfae : h → [p1, p2, p3].TFAE), [h ∧ p1, h ∧ p2, h ∧ p3].TFAE

Tactic:
have {h p1 p2 p3 : Prop} (htfae : h → List.TFAE [p1, p2, p3]) :
      List.TFAE [h ∧ p1, h ∧ p2, h ∧ p3] := by
    tfae_have 1 → 2 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 0 1).mp t⟩
    tfae_have 2 → 3 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 1 2).mp t⟩
    tfae_have 3 → 1 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 2 0).mp t⟩
    tfae_finish
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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
⊢ [K.PosSemidef,
      K.IsHermitian ∧
        ∀ (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⟫_𝕜) :
              ℝ),
      K.IsHermitian ∧
        ∀ (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'⟫_𝕜) :
              ℝ)].TFAE

Tactic:
this fun hHerm ↦ ?_

Premises used: Matrix.PosSemidef
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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
refine :
  ∀ (hHerm : K.IsHermitian),
    List.TFAE
      [∀ (x : Finsupp.{u_2, u_3} X (V →L[𝕜] V)),
          LE.le (α := V →L[𝕜] V) 0
            (x.sum fun (i : X) (xi : V →L[𝕜] V) ↦ x.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * K i j * xj),
        ∀ (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'⟫_𝕜) :
              ℝ)]
⊢ [K.PosSemidef,
      K.IsHermitian ∧
        ∀ (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⟫_𝕜) :
              ℝ),
      K.IsHermitian ∧
        ∀ (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'⟫_𝕜) :
              ℝ)].TFAE

Tactic:
refine this fun hHerm ↦ ?_
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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
simp :
  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) (xi : V →L[𝕜] V) ↦ x.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * K i j * xj :
                    (a : V) → V)
                  x_1,
                x_1⟫_𝕜 :
            ℝ),
      ∀ (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)),
        LE.le (α := V →L[𝕜] V) 0
          (x.sum fun (i : X) (xi : V →L[𝕜] V) ↦ x.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * K i j * xj),
      ∀ (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:
simp only [nonneg_iff_isPositive, isPositive_def', isSelfAdjoint_finsuppSum hHerm,
    reApplyInnerSelf_apply, true_and]

Premises used: _private.0.RKHS.isSelfAdjoint_finsuppSum, ContinuousLinearMap.nonneg_iff_isPositive, ContinuousLinearMap.reApplyInnerSelf_apply, ContinuousLinearMap.isPositive_def', true_and
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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
simp :
  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) (xi : V →L[𝕜] V) ↦ x.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * K i j * xj :
                    (a : V) → V)
                  x_1,
                x_1⟫_𝕜 :
            ℝ),
      ∀ (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:
simp only [star_eq_adjoint, zero_apply, add_apply, implies_true, Finsupp.sum_apply'', coe_mul',
    Function.comp_apply, Finsupp.sum_inner, adjoint_inner_left]

Premises used: Finsupp.sum_inner, ContinuousLinearMap.coe_mul', ContinuousLinearMap.adjoint_inner_left, Finsupp.sum_apply'', ContinuousLinearMap.add_apply, ContinuousLinearMap.star_eq_adjoint, Function.comp_apply, implies_true, ContinuousLinearMap.zero_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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
⊢ 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:
(subsingleton_or_nontrivial V).elim (fun h ↦ ?_) fun _ ↦ ?_

Premises used: subsingleton_or_nontrivial, Or.elim
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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 : Subsingleton V
⊢ ∀ (v : V), v = 0

Tactic:
have : ∀ v : V, v = 0 := fun v ↦ Subsingleton.elim v 0
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
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_1 : ∀ {h p1 p2 p3 : Prop} (htfae : h → [p1, p2, p3].TFAE), [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
h : Subsingleton V
this : ∀ (v : V), v = 0
⊢ 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:
simp [this]