awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
⊢ ∀ (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((0 : (a : X) → V) x : V)
have refine : ∀ (x : X) (v : V), ⟪v, (f : (a : X) → V) x⟫_𝕜 = ⟪v, (0 : (a : X) → V) x⟫_𝕜
Tactic: refine fun x ↦ ext_inner_left 𝕜 fun v ↦ ?_
-- 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
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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
⊢ ⟪v, (f : (a : X) → V) x⟫_𝕜 = ⟪v, (0 : (a : X) → V) x⟫_𝕜
have simp : ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = 0
Tactic: simp only [← kerFun_inner, coe_zero, Pi.zero_apply, inner_zero_right]
-- 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
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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
⊢ ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = 0
have refine : Membership.mem (α := H)
  (↑(toAddSubmonoid (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) : Set H)
  ((kerFun H x : (a : V) → H) v : H)
Tactic: refine inner_right_of_mem_orthogonal (subset_closure ?_) fin
-- 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
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
⊢ Matrix.IsHermitian (α := V →L[𝕜] V) (kernel H)
have a : ∀ (i j : X) (x : V),
  Eq (α := V) ((Matrix.conjTranspose (kernel H) i j : (a : V) → V) x : V) ((kernel H i j : (a : V) → V) x : V)
Tactic: ext
-- 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
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
i j : X
x : V
⊢ Eq (α := V) ((Matrix.conjTranspose (kernel H) i j : (a : V) → V) x : V) ((kernel H i j : (a : V) → V) x : V)
have a : ∀ (w : V), ⟪(Matrix.conjTranspose (kernel H) i j : (a : V) → V) x, w⟫_𝕜 = ⟪(kernel H i j : (a : V) → V) x, w⟫_𝕜
Tactic: refine ext_inner_right 𝕜 fun w ↦ ?_
-- 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
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
⊢ Matrix.PosSemidef (R := V →L[𝕜] V) (kernel H)
have refine_1 : ∀ (s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)),
  IsSelfAdjoint
    (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)
Tactic: refine ⟨isHermitian_kernel H, fun s ↦ (ContinuousLinearMap.isPositive_iff' _).2 ⟨?_, fun v ↦ ?_⟩⟩
-- 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
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
refine_1 :
  ∀ (s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)),
    IsSelfAdjoint
      (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)
⊢ Matrix.PosSemidef (R := V →L[𝕜] V) (kernel H)
have refine_2 : ∀ (s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)) (v : V),
  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: refine ⟨isHermitian_kernel H, fun s ↦ (ContinuousLinearMap.isPositive_iff' _).2 ⟨?_, fun v ↦ ?_⟩⟩
-- 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
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)
⊢ IsSelfAdjoint
    (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)
have refine_1 : 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: rw [IsSelfAdjoint, sub_zero, star_finsuppSum, Finsupp.sum_comm]
-- 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
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
⊢ 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⟫_𝕜
have 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))
Tactic: simp [Finsupp.sum_apply'', Finsupp.sum_inner, star, adjoint_inner_left,
      kernel_inner, -inner_kerFun, -kerFun_inner]
-- 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)
h : K.IsHermitian
f : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
⊢ 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)
have 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))
Tactic: simp only [mul_assoc, isSelfAdjoint_iff, star_finsuppSum, Pi.star_apply, star_mul, h.apply,
    star_star]
-- 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)
h : K.IsHermitian
f : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
⊢ 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))
have 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))
Tactic: rw [Finsupp.sum_comm]
-- 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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
⊢ [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
have tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
Tactic: tfae_have 1 → 2 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 0 1).mp t⟩
-- 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)
h p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : ∀ (a : h ∧ p1), h ∧ p2
⊢ [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
have tfae_2_to_3 : ∀ (a : h ∧ p2), h ∧ p3
Tactic: tfae_have 2 → 3 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 1 2).mp t⟩
-- 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)
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, h ∧ p2, h ∧ p3].TFAE
have tfae_3_to_1 : ∀ (a : h ∧ p3), h ∧ p1
Tactic: tfae_have 3 → 1 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 2 0).mp t⟩
-- 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)
⊢ [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
have this : ∀ {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
-- 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
⊢ [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
have 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'⟫_𝕜) :
            ℝ)]
Tactic: refine this fun hHerm ↦ ?_
-- 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
⊢ 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'⟫_𝕜) :
            ℝ)]
have 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'⟫_𝕜) :
          ℝ)]
Tactic: simp only [nonneg_iff_isPositive, isPositive_def', isSelfAdjoint_finsuppSum hHerm,
    reApplyInnerSelf_apply, true_and]
-- 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
⊢ 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'⟫_𝕜) :
            ℝ)]
have 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'⟫_𝕜) :
          ℝ)]
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]
-- 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
⊢ 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_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'⟫_𝕜) :
            ℝ)]
Tactic: refine (subsingleton_or_nontrivial V).elim (fun h ↦ ?_) fun _ ↦ ?_
-- 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 : 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'⟫_𝕜) :
            ℝ)]
have this₁ : ∀ (v : V), v = 0
Tactic: have : ∀ v : V, v = 0 := fun v ↦ Subsingleton.elim v 0
-- 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
h : 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'⟫_𝕜) :
            ℝ)]
have refine_2 : ∀ (v : V) (hv : 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: obtain ⟨v, hv⟩ := exists_ne (0 : V)