Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x✝² x✝¹ x✝ : H₀ K
⊢ (Finsupp.sum (x✝² + x✝¹) fun x z ↦
      match x with
      | (y, u) =>
        Finsupp.sum x✝ fun x w ↦
          match x with
          | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) =
    (Finsupp.sum x✝² fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) +
      Finsupp.sum x✝¹ fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜

Tactic:
Finsupp.sum_add_index'

Goal state after:
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x✝² x✝¹ x✝ : H₀ K
⊢ ((Finsupp.sum x✝² fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) +
      Finsupp.sum x✝¹ fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) =
    (Finsupp.sum x✝² fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜) +
      Finsupp.sum x✝¹ fun x z ↦
        match x with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜

case h_zero
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x✝² x✝¹ x✝ : H₀ K
⊢ ∀ (a : X × V),
    (match a with
      | (y, u) =>
        Finsupp.sum x✝ fun x w ↦
          match x with
          | (x, v) => star 0 * w * ⟪(K x y) u, v⟫_𝕜) =
      0

case h_add
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x✝² x✝¹ x✝ : H₀ K
⊢ ∀ (a : X × V) (b₁ b₂ : 𝕜),
    (match a with
      | (y, u) =>
        Finsupp.sum x✝ fun x w ↦
          match x with
          | (x, v) => star (b₁ + b₂) * w * ⟪(K x y) u, v⟫_𝕜) =
      (match a with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star b₁ * w * ⟪(K x y) u, v⟫_𝕜) +
        match a with
        | (y, u) =>
          Finsupp.sum x✝ fun x w ↦
            match x with
            | (x, v) => star b₂ * w * ⟪(K x y) u, v⟫_𝕜