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
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 : H₀ K
x_2 : 𝕜
⊢ (Finsupp.sum (x_2 • x) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 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 : (Finsupp.sum x fun (i : X × V) (a : 𝕜) ↦
    match (motive := X × V → 𝕜) i with
    | (y, u) =>
      Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (x, v) => star (x_2 * a) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
  HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
    (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_1 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_smul_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 : H₀ K
x_2 : 𝕜
rw :
  (Finsupp.sum x fun (i : X × V) (a : 𝕜) ↦
      match (motive := X × V → 𝕜) i with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star (x_2 * a) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 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_2 • x) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 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₁ : ∀ (i : X × V),
  Eq.{u_1 + 1} (α := 𝕜)
    (match (motive := X × V → 𝕜) i with
      | (y, u) =>
        Finsupp.sum x_1 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_smul_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
x_1 x_2 : V
⊢ (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))
have refine : ∀ (f : H₀ K),
  inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K))
      (↑f : UniformSpace.Completion (H₀ K)) =
    ⟪HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
        (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
      (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜
Tactic: refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_
-- 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
x_1 : 𝕜
x_2 : V
⊢ (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))
have refine : ∀ (f : H₀ K),
  inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K))
      (↑f : UniformSpace.Completion (H₀ K)) =
    ⟪HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
        (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
      (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜
Tactic: refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_
-- 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
v : V
⊢ norm (E := UniformSpace.Completion (H₀ K))
      ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)) ≤
    √‖K x x‖ * ‖v‖
have refine : HPow.hPow (β := ℕ)
    (norm (E := UniformSpace.Completion (H₀ K))
      ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)))
    2 ≤
  HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
Tactic: refine (sq_le_sq₀ (by simp) (by simp [mul_nonneg])).mp ?_
-- 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
v : V
⊢ HPow.hPow (β := ℕ)
      (norm (E := UniformSpace.Completion (H₀ K))
        ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)))
      2 ≤
    HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
have simp : ‖inner 𝕜 (E := H₀ K) (Finsupp.single (x, v) 1) (Finsupp.single (x, v) 1)‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
Tactic: simp only [LinearMap.coe_mk, AddHom.coe_mk, UniformSpace.Completion.norm_coe,
    ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_self_re_eq_norm]
-- 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
v : V
⊢ ‖inner 𝕜 (E := H₀ K) (Finsupp.single (x, v) 1) (Finsupp.single (x, v) 1)‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
have simp : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
Tactic: simp only [inner_H₀_def, RCLike.star_def, mul_zero, zero_mul,
    Finsupp.sum_single_index, mul_one, map_zero, map_one, one_mul]
-- 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
v : V
⊢ ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
have _ : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖
Tactic: calc
    _ ≤ ‖K x x v‖ * ‖v‖ := by simp [norm_inner_le_norm]
    _ ≤ ‖K x x‖ * ‖v‖ * ‖v‖ := by simp [mul_le_mul_of_nonneg_right, le_opNorm]
    _ ≤ _ := by simp [mul_pow, mul_assoc, ← sq]
-- 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
v : V
_ : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖
⊢ ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
have _₁ : norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖ ≤ ‖K x x‖ * ‖v‖ * ‖v‖
Tactic: calc
    _ ≤ ‖K x x v‖ * ‖v‖ := by simp [norm_inner_le_norm]
    _ ≤ ‖K x x‖ * ‖v‖ * ‖v‖ := by simp [mul_le_mul_of_nonneg_right, le_opNorm]
    _ ≤ _ := by simp [mul_pow, mul_assoc, ← sq]
-- 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
v : V
_ : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖
_₁ : norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖ ≤ ‖K x x‖ * ‖v‖ * ‖v‖
⊢ ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
have _₂ : ‖K x x‖ * ‖v‖ * ‖v‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
Tactic: calc
    _ ≤ ‖K x x v‖ * ‖v‖ := by simp [norm_inner_le_norm]
    _ ≤ ‖K x x‖ * ‖v‖ * ‖v‖ := by simp [mul_le_mul_of_nonneg_right, le_opNorm]
    _ ≤ _ := by simp [mul_pow, mul_assoc, ← sq]
-- 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
⊢ Function.Injective (α := OfKernel K) (β := X → V)
    (⇑(ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
          (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
            (kerFun K x)) :
      (a : OfKernel K) → X → V)
have refine : ∀ (f : OfKernel K)
  (h :
    Eq (α := X → V)
      ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
              (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
                (kerFun K x) :
            (a : OfKernel K) → X → V)
          f :
        X → V)
      (0 : X → V)),
  f = 0
Tactic: refine (injective_iff_map_eq_zero _).mpr fun f h ↦ ?_
-- 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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
⊢ f = 0
have refine : ∀ (ff : H₀ K), ⟪(↑ff : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
Tactic: refine UniformSpace.Completion.denseRange_coe.eq_zero_of_inner_right 𝕜 fun ff ↦ ?_
-- 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
f : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
⊢ ⟪(↑0 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
have this : Eq (α := UniformSpace.Completion (H₀ K)) (↑0 : UniformSpace.Completion (H₀ K)) 0
Tactic: have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
-- 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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(↑(Finsupp.single i a + f_1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
have single_add : ⟪(↑(Finsupp.single i a) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
Tactic: simp only [UniformSpace.Completion.coe_add, inner_add_left, *, add_zero]
-- 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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(↑(Finsupp.single i a) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
have single_add : ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0
Tactic: rw [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜)]
-- 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
f : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0
have this : ⟪i.2,
    (ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
          (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
            (kerFun K x) :
        (a : OfKernel K) → X → V)
      f i.1⟫_𝕜 =
  ⟪i.2, 0 i.1⟫_𝕜
Tactic: have := (ext_iff_inner_left 𝕜).mp (congrFun h i.1) i.2
-- 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
f : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
this :
  ⟪i.2,
      (ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f i.1⟫_𝕜 =
    ⟪i.2, 0 i.1⟫_𝕜
⊢ ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0
have this₁ : ⟪(↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
Tactic: have := by simpa [OfKernel.kerFun, adjoint_inner_right] using this
-- 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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
this_1 :
  ⟪i.2,
      (ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f i.1⟫_𝕜 =
    ⟪i.2, 0 i.1⟫_𝕜
this : ⟪(↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0
have single_add : ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 =
  ⟪HSMul.hSMul (β := OfKernel K) a (↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜
Tactic: rw [← mul_zero (conj a), ← this, ← inner_smul_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
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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
i : X × V
a : 𝕜
f_1 : X × V →₀ 𝕜
h_1 : i ∉ f_1.support
h_2 : a ≠ 0
h_3 : ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
this_1 :
  ⟪i.2,
      (ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f i.1⟫_𝕜 =
    ⟪i.2, 0 i.1⟫_𝕜
this : ⟪(↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 =
    ⟪HSMul.hSMul (β := OfKernel K) a (↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜
have single_add : (UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a) =
  HSMul.hSMul (β := OfKernel K) a (↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K))
Tactic: refine (ext_iff_inner_right 𝕜).mp ?_ f
-- 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 : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
ff : H₀ K
⊢ ⟪(↑ff : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
have zero : ⟪(↑0 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
Tactic: induction ff using Finsupp.induction with
    | zero =>
      have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
      simp [this]
    | single_add i a =>
    simp only [UniformSpace.Completion.coe_add, inner_add_left, *, add_zero]
    rw [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜)]
    have := (ext_iff_inner_left 𝕜).mp (congrFun h i.1) i.2
    have := by simpa [OfKernel.kerFun, adjoint_inner_right] using this
    rw [← mul_zero (conj a), ← this, ← inner_smul_left]
    refine (ext_iff_inner_right 𝕜).mp ?_ f
    simp [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜),
      ← map_smul, -SeparationQuotient.mkCLM_apply, -UniformSpace.Completion.coe_toComplL]
Cleared hypotheses: ff