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
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

Tactic:
UniformSpace.Completion.denseRange_coe.eq_zero_of_inner_right 𝕜 fun ff ↦ ?_

Premises used: DenseRange.eq_zero_of_inner_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
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)
refine : ∀ (ff : H₀ K), ⟪(↑ff : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ f = 0

Tactic:
refine UniformSpace.Completion.denseRange_coe.eq_zero_of_inner_right 𝕜 fun ff ↦ ?_

Premises used: DenseRange.eq_zero_of_inner_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
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)
⊢ Eq (α := UniformSpace.Completion (H₀ K)) (↑0 : UniformSpace.Completion (H₀ K)) 0

Tactic:
have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
-- 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 : 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)
this : Eq (α := UniformSpace.Completion (H₀ K)) (↑0 : UniformSpace.Completion (H₀ K)) 0
⊢ ⟪(↑0 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0

Tactic:
simp [this]
-- 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 : 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
single_add : ⟪(↑(Finsupp.single i a) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(↑(Finsupp.single i a + f_1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0

Tactic:
simp only [UniformSpace.Completion.coe_add, inner_add_left, *, add_zero]

Premises used: inner_add_left, add_zero, UniformSpace.Completion.coe_add
-- 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 : 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
single_add :
  ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0
⊢ ⟪(↑(Finsupp.single i a) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0

Tactic:
rw [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜)]

Premises used: UniformSpace.Completion.coe_toComplL
-- 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 : 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
⊢ ⟪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
-- 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 : 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⟫_𝕜
⊢ ⟪(↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0

Tactic:
simpa [OfKernel.kerFun, adjoint_inner_right] using this

Premises used: _private.0.RKHS.OfKernel.kerFun, ContinuousLinearMap.adjoint_inner_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
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⟫_𝕜
⊢ ⟪(↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0

Tactic:
have := by simpa [OfKernel.kerFun, adjoint_inner_right] using this
-- 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 : 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
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⟫_𝕜
⊢ ⟪(UniformSpace.Completion.toComplL : (a : H₀ K) → UniformSpace.Completion (H₀ K)) (Finsupp.single i a), f⟫_𝕜 = 0

Tactic:
rw [← mul_zero (conj a), ← this, ← inner_smul_left]

Premises used: MulZeroClass.mul_zero, starRingEnd, DFunLike.coe, inner_smul_left
-- 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 : 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⟫_𝕜

Tactic:
(ext_iff_inner_right 𝕜).mp ?_ f

Premises used: ext_iff_inner_right, Iff.mp
-- 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 : 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
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))
⊢ ⟪(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:
refine (ext_iff_inner_right 𝕜).mp ?_ f

Premises used: ext_iff_inner_right, Iff.mp
-- 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 : 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) =
    HSMul.hSMul (β := OfKernel K) a (↑(Finsupp.single i 1) : UniformSpace.Completion (H₀ K))

Tactic:
simp [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜),
      ← map_smul, -SeparationQuotient.mkCLM_apply, -UniformSpace.Completion.coe_toComplL]

Premises used: UniformSpace.Completion.coe_toComplL, SeparationQuotient.mkCLM_apply, map_smul
-- 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 : 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
zero : ⟪(↑0 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
single_add :
  ∀ (i : X × V) (a : 𝕜) (f_1 : X × V →₀ 𝕜),
    i ∉ f_1.support →
      a ≠ 0 →
        ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0 →
          ⟪(↑(Finsupp.single i a + f_1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(↑ff : 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]

Premises used: inner_add_left, ext_iff_inner_right, Iff.mp, UniformSpace.Completion.coe_toComplL, add_zero, SeparationQuotient.mkCLM_apply, UniformSpace.Completion.coe_add, map_smul, inner_smul_left
-- 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)
inst_4 : Fact K.PosSemidef
a : ∀ (x y : X) (v : V), Eq (α := V) ((kernel (OfKernel K) x y : (a : V) → V) v : V) ((K x y : (a : V) → V) v : V)
⊢ kernel (OfKernel K) = K

Tactic:
ext x y 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
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
x y : X
v : V
⊢ Eq (α := V) ((kernel (OfKernel K) x y : (a : V) → V) v : V) ((K x y : (a : V) → V) v : V)

Tactic:
ext_inner_right 𝕜 fun w ↦ ?_

Premises used: ext_inner_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
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
x y : X
v : V
a : ∀ (w : V), ⟪(kernel (OfKernel K) x y : (a : V) → V) v, w⟫_𝕜 = ⟪(K x y : (a : V) → V) v, w⟫_𝕜
⊢ Eq (α := V) ((kernel (OfKernel K) x y : (a : V) → V) v : V) ((K x y : (a : V) → V) v : V)

Tactic:
refine ext_inner_right 𝕜 fun w ↦ ?_

Premises used: ext_inner_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
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
x y : X
v w : V
⊢ ⟪(kernel (OfKernel K) x y : (a : V) → V) v, w⟫_𝕜 = ⟪(K x y : (a : V) → V) v, w⟫_𝕜

Tactic:
simp [kernel, adjoint_inner_left, -inner_kerFun, -kerFun_inner,
    coeCLM, OfKernel.kerFun, inner_H₀_def, RKHS.kerFun]

Premises used: RKHS.coeCLM, ContinuousLinearMap.adjoint_inner_left, RKHS.inner_kerFun, RKHS.kerFun, RKHS.kerFun_inner, _private.0.RKHS.OfKernel.kerFun, RKHS.kernel, _private.0.RKHS.inner_H₀_def
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
p : Submodule 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hp : p ∈ T.invtSubmodule
⊢ pᗮ ∈ T.invtSubmodule

Tactic:
fun x hx y hy ↦ hT y x ▸ hx (T y) (hp hy)

Premises used: Set.Mem, setOf, Eq.rec, Set.preimage, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ T.IsFinitelySemisimple

Tactic:
Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩

Premises used: Iff.mpr, inf_le_right, Module.End.isFinitelySemisimple_iff, Submodule.orthogonal, Module.End.invtSubmodule.inf_mem, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
refine_1 :
  ∀ (p : Submodule 𝕜 E) (hp₁ : p ∈ T.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p) (q : Submodule 𝕜 E)
    (hq₁ : q ∈ T.invtSubmodule) (hq₂ : q ≤ p), qᗮ ∈ T.invtSubmodule
refine_2 :
  ∀ (p : Submodule 𝕜 E) (hp₁ : p ∈ T.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p) (q : Submodule 𝕜 E)
    (hq₁ : q ∈ T.invtSubmodule) (hq₂ : q ≤ p), Disjoint q (qᗮ ⊓ p)
refine_3 :
  ∀ (p : Submodule 𝕜 E) (hp₁ : p ∈ T.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p) (q : Submodule 𝕜 E)
    (hq₁ : q ∈ T.invtSubmodule) (hq₂ : q ≤ p), q ⊔ qᗮ ⊓ p = p
⊢ T.IsFinitelySemisimple

Tactic:
refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩

Premises used: Iff.mpr, inf_le_right, Module.End.isFinitelySemisimple_iff, Submodule.orthogonal, Module.End.invtSubmodule.inf_mem, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

Tactic:
orthogonalComplement_mem_invtSubmodule hT hq₁

Premises used: Set.Mem, setOf, LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

Tactic:
exact orthogonalComplement_mem_invtSubmodule hT hq₁

Premises used: LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)

Tactic:
simp [disjoint_iff, ← inf_assoc, Submodule.inf_orthogonal_eq_bot q]

Premises used: disjoint_iff, Submodule.inf_orthogonal_eq_bot, inf_assoc