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
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'⟫_𝕜) :
        ℝ)
⊢ ∀ (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:
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)
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'⟫_𝕜) :
        ℝ)
⊢ ∀ (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:
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)
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'⟫_𝕜) :
        ℝ)
⊢ ∀
    (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:
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)
this : ∀ {h p1 p2 p3 : Prop} (htfae : h → [p1, p2, p3].TFAE), [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
h_1 : Nontrivial V
v_1 : V
hv : v_1 ≠ 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'⟫_𝕜) :
        ℝ)
h :
  ∀ (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'⟫_𝕜) :
        ℝ)
ff : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
v : V
rw :
  LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (ff.sum fun (x' : X) (v' : V →L[𝕜] V) ↦
          ff.sum fun (x : X) (v_2 : V →L[𝕜] V) ↦
            inner 𝕜 (E := V) ((K x x' : (a : V) → V) ((v' : (a : V) → V) v : V) : V) ((v_2 : (a : V) → V) v : V)) :
      ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (ff.sum fun (i : X) (a : V →L[𝕜] V) ↦
          ff.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) v : V) : V) ((a : (a : V) → V) v : V)) :
      ℝ)

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)
this : ∀ {h p1 p2 p3 : Prop} (htfae : h → [p1, p2, p3].TFAE), [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
h_1 : Nontrivial V
v_1 : V
hv : v_1 ≠ 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'⟫_𝕜) :
        ℝ)
h :
  ∀ (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'⟫_𝕜) :
        ℝ)
ff : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
v : V
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (ff.sum fun (x' : X) (v' : V →L[𝕜] V) ↦
          ff.sum fun (x : X) (v_2 : V →L[𝕜] V) ↦
            inner 𝕜 (E := V) ((K x x' : (a : V) → V) ((v' : (a : V) → V) v : V) : V) ((v_2 : (a : V) → V) v : V)) :
      ℝ)

Tactic:
simpa [Finsupp.sum_sum_index, inner_add_right, inner_add_left] using
      h (ff.sum fun x T ↦ .single x (T v))

Premises used: Finsupp.sum, inner_add_left, inner_add_right, DFunLike.coe, Finsupp.sum_sum_index, Finsupp.single
-- 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 : 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'⟫_𝕜) :
        ℝ)
⊢ ∀
    (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))
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
rw :
  Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        (Finsupp.sum f fun (x' : X × V) (v' : 𝕜) ↦
          Finsupp.sum g fun (x : X × V) (v : 𝕜) ↦
            match (motive := X × V → 𝕜) x' with
            | (x_1, v_1) => star v * v' * ⟪(K x_1 x.1 : (a : V) → V) x.2, v_1⟫_𝕜) :
      𝕜)
    (Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum g fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
      𝕜)
⊢ Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        (Finsupp.sum g fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum f fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) :
      𝕜)
    (Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum g fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
      𝕜)

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
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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
simp :
  Eq (α := 𝕜)
    (Finsupp.sum f fun (a : X × V) (b : 𝕜) ↦
      Finsupp.sum g fun (a_1 : X × V) (b_1 : 𝕜) ↦
        (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star b_1 * b * ⟪(K a.1 a_1.1 : (a : V) → V) a_1.2, a.2⟫_𝕜))
    (Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
      Finsupp.sum g fun (x_1 : X × V) (w : 𝕜) ↦ star z * w * ⟪(K x_1.1 x.1 : (a : V) → V) x.2, x_1.2⟫_𝕜)
⊢ Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
        (Finsupp.sum f fun (x' : X × V) (v' : 𝕜) ↦
          Finsupp.sum g fun (x : X × V) (v : 𝕜) ↦
            match (motive := X × V → 𝕜) x' with
            | (x_1, v_1) => star v * v' * ⟪(K x_1 x.1 : (a : V) → V) x.2, v_1⟫_𝕜) :
      𝕜)
    (Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum g fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
      𝕜)

Tactic:
simp only [map_finsuppSum]

Premises used: map_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
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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
h :
  ∀ (x : X × V) (x_1 : 𝕜) (x_2 : X × V) (x_3 : 𝕜),
    (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star x_3 * x_1 * ⟪(K x.1 x_2.1 : (a : V) → V) x_2.2, x.2⟫_𝕜) =
      star x_1 * x_3 * ⟪(K x_2.1 x.1 : (a : V) → V) x.2, x_2.2⟫_𝕜
⊢ Eq (α := 𝕜)
    (Finsupp.sum f fun (a : X × V) (b : 𝕜) ↦
      Finsupp.sum g fun (a_1 : X × V) (b_1 : 𝕜) ↦
        (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star b_1 * b * ⟪(K a.1 a_1.1 : (a : V) → V) a_1.2, a.2⟫_𝕜))
    (Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
      Finsupp.sum g fun (x_1 : X × V) (w : 𝕜) ↦ star z * w * ⟪(K x_1.1 x.1 : (a : V) → V) x.2, x_1.2⟫_𝕜)

Tactic:
congr! 6
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
x : X × V
x_1 : 𝕜
x_2 : X × V
x_3 : 𝕜
h :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star x_3 * x_1 * ⟪(star (K x_2.1 x.1) : (a : V) → V) x_2.2, x.2⟫_𝕜) =
    star x_1 * x_3 * ⟪(K x_2.1 x.1 : (a : V) → V) x.2, x_2.2⟫_𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star x_3 * x_1 * ⟪(K x.1 x_2.1 : (a : V) → V) x_2.2, x.2⟫_𝕜) =
    star x_1 * x_3 * ⟪(K x_2.1 x.1 : (a : V) → V) x.2, x_2.2⟫_𝕜

Tactic:
rw [← (Fact.out : K.PosSemidef).isHermitian.apply]

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.apply, Fact.out
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
x : X × V
x_1 : 𝕜
x_2 : X × V
x_3 : 𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star x_3 * x_1 * ⟪(star (K x_2.1 x.1) : (a : V) → V) x_2.2, x.2⟫_𝕜) =
    star x_1 * x_3 * ⟪(K x_2.1 x.1 : (a : V) → V) x.2, x_2.2⟫_𝕜

Tactic:
simp [star, adjoint_inner_right, mul_comm]

Premises used: mul_comm, ContinuousLinearMap.adjoint_inner_right, 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact 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⟫_𝕜) :
          ℝ)

Tactic:
have := (posSemidef_tfae.out 0 1).mp (Fact.out : K.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
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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
this :
  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⟫_𝕜) :
          ℝ)
⊢ ∀ (x : H₀ K),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ)
          (Finsupp.sum x fun (x_1 : X × V) (z : 𝕜) ↦
            match (motive := X × V → 𝕜) x_1 with
            | (y, u) =>
              Finsupp.sum x fun (x : X × V) (w : 𝕜) ↦
                match (motive := X × V → 𝕜) x with
                | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) :
        ℝ)

Tactic:
this.2

Premises used: And.right
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
this :
  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⟫_𝕜) :
          ℝ)
⊢ ∀ (x : H₀ K),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ)
          (Finsupp.sum x fun (x_1 : X × V) (z : 𝕜) ↦
            match (motive := X × V → 𝕜) x_1 with
            | (y, u) =>
              Finsupp.sum x fun (x : X × V) (w : 𝕜) ↦
                match (motive := X × V → 𝕜) x with
                | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) :
        ℝ)

Tactic:
exact this.2

Premises used: And.right