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
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 : V
hv : v ≠ 0
h :
  ∀ (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)) :
        ℝ)
ff : X × V →₀ 𝕜
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (ff.sum fun (xv : X × V) (z : 𝕜) ↦
          ff.sum fun (xv' : X × V) (w : 𝕜) ↦
            HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) w * ⟪(K xv'.1 xv.1 : (a : V) → V) xv.2, xv'.2⟫_𝕜) :
      ℝ)
have rw : LE.le (α := ℝ) (0 : ℝ)
  ((RCLike.re : (a : 𝕜) → ℝ)
      (ff.sum fun (x' : X × V) (v' : 𝕜) ↦
        ff.sum fun (x : X × V) (v : 𝕜) ↦
          HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) v : 𝕜) v' * ⟪(K x'.1 x.1 : (a : V) → V) x.2, x'.2⟫_𝕜) :
    ℝ)
Tactic: rw [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
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 : V
hv : v ≠ 0
h :
  ∀ (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)) :
        ℝ)
ff : X × V →₀ 𝕜
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (ff.sum fun (x' : X × V) (v' : 𝕜) ↦
          ff.sum fun (x : X × V) (v : 𝕜) ↦
            HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) v : 𝕜) v' * ⟪(K x'.1 x.1 : (a : V) → V) x.2, x'.2⟫_𝕜) :
      ℝ)
have h₁ : Eq (α := 𝕜)
  (ff.sum fun (x' : X × V) (v' : 𝕜) ↦
    ff.sum fun (x : X × V) (v : 𝕜) ↦
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) v : 𝕜) v' * ⟪(K x'.1 x.1 : (a : V) → V) x.2, x'.2⟫_𝕜)
  (Finsupp.sum
    (ff.sum fun (xv : X × V) (z : 𝕜) ↦
      Finsupp.single xv.1
        (HSMul.hSMul (β := V →L[𝕜] V) (z / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)
          (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : V) → V →L[𝕜] 𝕜) v) xv.2)))
    fun (i : X) (a : V →L[𝕜] V) ↦
    Finsupp.sum
      (ff.sum fun (xv : X × V) (z : 𝕜) ↦
        Finsupp.single xv.1
          (HSMul.hSMul (β := V →L[𝕜] V) (z / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)
            (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : V) → V →L[𝕜] 𝕜) v) xv.2)))
      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: convert! h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) 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
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 : V
hv : v ≠ 0
h :
  ∀ (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)) :
        ℝ)
ff : X × V →₀ 𝕜
⊢ Eq (α := 𝕜)
    (ff.sum fun (x' : X × V) (v' : 𝕜) ↦
      ff.sum fun (x : X × V) (v : 𝕜) ↦
        HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) v : 𝕜) v' * ⟪(K x'.1 x.1 : (a : V) → V) x.2, x'.2⟫_𝕜)
    (Finsupp.sum
      (ff.sum fun (xv : X × V) (z : 𝕜) ↦
        Finsupp.single xv.1
          (HSMul.hSMul (β := V →L[𝕜] V) (z / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)
            (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : V) → V →L[𝕜] 𝕜) v) xv.2)))
      fun (i : X) (a : V →L[𝕜] V) ↦
      Finsupp.sum
        (ff.sum fun (xv : X × V) (z : 𝕜) ↦
          Finsupp.single xv.1
            (HSMul.hSMul (β := V →L[𝕜] V) (z / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)
              (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : V) → V →L[𝕜] 𝕜) v) xv.2)))
        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))
have h₁ : Eq (α := 𝕜)
  (ff.sum fun (x' : X × V) (v' : 𝕜) ↦
    ff.sum fun (x : X × V) (v : 𝕜) ↦
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) v : 𝕜) v' * ⟪(K x'.1 x.1 : (a : V) → V) x.2, x'.2⟫_𝕜)
  (ff.sum fun (a : X × V) (b : 𝕜) ↦
    ff.sum fun (a_1 : X × V) (b_1 : 𝕜) ↦ ⟪HSMul.hSMul (β := V) b_1 ((K a.1 a_1.1 : (a : V) → V) a_1.2 : V), b • a.2⟫_𝕜)
Tactic: simp [Finsupp.sum_sum_index, inner_add_right, inner_add_left, ← smul_assoc, hv]
-- 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
⊢ 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_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⟫_𝕜) :
      ℝ)
Tactic: tfae_have 1 → 2 := fun h ff ↦ by
    rw [Finsupp.sum_comm]
    convert! h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) v
    simp [Finsupp.sum_sum_index, inner_add_right, inner_add_left, ← smul_assoc, hv]
    simp [inner_smul_left, inner_smul_right, ← mul_assoc, mul_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)
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⟫_𝕜) :
        ℝ)
⊢ 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_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'⟫_𝕜) :
      ℝ)
Tactic: tfae_have 2 → 3 := fun h vv ↦ by
    simpa [add_mul, Finsupp.sum_sum_index] using (h (vv.sum fun x v ↦ .single ⟨x, v⟩ 1))
-- 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_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 (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)) :
      ℝ)
have 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)) :
    ℝ)
Tactic: rw [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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
⊢ 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⟫_𝕜 :
      𝕜)
have 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⟫_𝕜 :
    𝕜)
Tactic: rw [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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
⊢ 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⟫_𝕜 :
      𝕜)
have 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⟫_𝕜)
Tactic: simp only [map_finsuppSum]
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f g : H₀ K
⊢ 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⟫_𝕜)
have 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⟫_𝕜
Tactic: congr! 6
-- 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
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 * ⟪(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⟫_𝕜
have 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⟫_𝕜
Tactic: rw [← (Fact.out : K.PosSemidef).isHermitian.apply]
-- 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
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
⊢ ∀ (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⟫_𝕜) :
        ℝ)
have 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⟫_𝕜) :
        ℝ)
Tactic: have := (posSemidef_tfae.out 0 1).mp (Fact.out : K.PosSemidef)
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 x_2 : H₀ K
⊢ (Finsupp.sum (x + x_1) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HAdd.hAdd (α := 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 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 x_1 fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜)
have h_zero : ∀ (a : X × V),
  Eq.{u_1 + 1} (α := 𝕜)
    (match (motive := X × V → 𝕜) a with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
      𝕜)
    (0 : 𝕜)
Tactic: rw [Finsupp.sum_add_index']
-- 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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 x_2 : H₀ K
h_zero :
  ∀ (a : X × V),
    Eq.{u_1 + 1} (α := 𝕜)
      (match (motive := X × V → 𝕜) a with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (0 : 𝕜)
⊢ (Finsupp.sum (x + x_1) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HAdd.hAdd (α := 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 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 x_1 fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜)
have h_add : ∀ (a : X × V) (b₁ b₂ : 𝕜),
  (match (motive := X × V → 𝕜) a with
    | (y, u) =>
      Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (x, v) => star (b₁ + b₂) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜)
      (match (motive := X × V → 𝕜) a with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star b₁ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (match (motive := X × V → 𝕜) a with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star b₂ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
Tactic: rw [Finsupp.sum_add_index']