awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst_4 : Nontrivial E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
this_1 : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact.{u_2} (X := E) (sphere 0 ‖x‖)
H₂ : Set.Nonempty.{u_2} (α := E) (sphere 0 ‖x‖)
x₀ : E
hx₀' : Membership.mem (γ := Set E) (sphere 0 ‖x‖) x₀
hTx₀ : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T' : E →L[𝕜] E).reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀_ne : x₀ ≠ 0
⊢ HasEigenvalue T
    (↑(⨅ (x : { x : E // x ≠ 0 }),
          HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫_𝕜 : ℝ)
            (HPow.hPow (β := ℕ) ‖(↑x : E)‖ 2)) :
      𝕜)

Tactic:
exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMinOn hx₀_ne this)

Premises used: Module.End.hasEigenvalue_of_hasEigenvector, Subtype.prop, IsSelfAdjoint.hasEigenvector_of_isMinOn
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hT' : ∀ (μ : 𝕜), eigenspace T μ = ⊥
⊢ Subsingleton E

Tactic:
(subsingleton_or_nontrivial E).resolve_right fun _h =>
    absurd (hT' _) hT.hasEigenvalue_iSup_of_finiteDimensional

Premises used: Norm.norm, Inner.inner, iSup, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, HDiv.hDiv, subsingleton_or_nontrivial, RCLike.ofReal, absurd, HPow.hPow, RCLike.re, Or.resolve_right, OfNat.ofNat, Subtype.val, DFunLike.coe
-- 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
f g : H
h : ∀ (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((g : (a : X) → V) x : V)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- 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
f : H
⊢ Eq (α := X → V) ((coeCLM 𝕜 : (a : H) → X → V) f : X → V) ((⇑f : (a : X) → V) : (a : X) → V)

Tactic:
rfl

Premises used: 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
⊢ Eq (α := (a : X) → V) (⇑0 : (a : X) → V) 0

Tactic:
(coeCLM 𝕜).map_zero ..

Premises used: ContinuousLinearMap.map_zero, RKHS.coeCLM
-- 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
f g : H
⊢ (⇑(f + g) : (a : X) → V) = HAdd.hAdd (α := (a : X) → V) (⇑f : (a : X) → V) (⇑g : (a : X) → V)

Tactic:
(coeCLM 𝕜).map_add ..

Premises used: RKHS.coeCLM, ContinuousLinearMap.map_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
f g : H
⊢ (⇑(f - g) : (a : X) → V) = HSub.hSub (α := (a : X) → V) (⇑f : (a : X) → V) (⇑g : (a : X) → V)

Tactic:
(coeCLM 𝕜).map_sub (M₂ := X → V) ..

Premises used: ContinuousLinearMap.map_sub, RKHS.coeCLM
-- 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
f : H
⊢ Eq (α := (a : X) → V) (⇑(-f) : (a : X) → V) (-(⇑f : (a : X) → V))

Tactic:
(coeCLM 𝕜).map_neg (M₂ := X → V) ..

Premises used: RKHS.coeCLM, ContinuousLinearMap.map_neg
-- 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
f : H
c : 𝕜
⊢ (⇑(c • f) : (a : X) → V) = HSMul.hSMul (β := (a : X) → V) c (⇑f : (a : X) → V)

Tactic:
(coeCLM 𝕜).map_smul ..

Premises used: RKHS.coeCLM, ContinuousLinearMap.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
x : X
simp_rw : Continuous.{u_4, u_3} (Y := V) fun (f : H) ↦ (coeCLM 𝕜 : (a : H) → X → V) f x
⊢ Continuous.{u_4, u_3} (Y := V) fun (f : H) ↦ (f : (a : X) → V) x

Tactic:
simp_rw [← coeCLM_apply]

Premises used: RKHS.coeCLM_apply
-- 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
x : X
⊢ Continuous.{u_4, u_3} (Y := V) fun (f : H) ↦ (coeCLM 𝕜 : (a : H) → X → V) f x

Tactic:
fun_prop
-- 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
y : X
v : V
x : X
⊢ Eq.{u_3 + 1} (α := V) ((((kerFun H y : (a : V) → H) v : H) : (a : X) → V) x : V) ((kernel H x y : (a : V) → V) v : V)

Tactic:
simp [kernel, kerFun]

Premises used: RKHS.kerFun, RKHS.kernel
-- 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
x y : X
⊢ Eq (α := V →L[𝕜] V) (kernel H x y)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H y))

Tactic:
simp [kerFun, kernel]

Premises used: RKHS.kerFun, RKHS.kernel
-- 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
x : X
v : V
f : H
⊢ ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = ⟪v, (f : (a : X) → V) x⟫_𝕜

Tactic:
simp [kerFun, ← adjoint_inner_right]

Premises used: RKHS.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
x : X
v : V
f : H
⊢ ⟪f, (kerFun H x : (a : V) → H) v⟫_𝕜 = ⟪(f : (a : X) → V) x, v⟫_𝕜

Tactic:
simp [kerFun, ← adjoint_inner_left]

Premises used: ContinuousLinearMap.adjoint_inner_left, RKHS.kerFun
-- 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
x y : X
v w : V
⊢ ⟪(kernel H x y : (a : V) → V) v, w⟫_𝕜 =
    inner.{u_1, u_4} 𝕜 (E := H) ((kerFun H y : (a : V) → H) v : H) ((kerFun H x : (a : V) → H) w : H)

Tactic:
simp [← adjoint_inner_left, kernel]

Premises used: ContinuousLinearMap.adjoint_inner_left, RKHS.kernel
-- 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
x : X
rw : norm (E := V →L[𝕜] V) (kernel H x x) = norm (E := V →L[𝕜] H) (kerFun H x) * norm (E := V →L[𝕜] H) (kerFun H x)
rw₁ :
  norm (E := V →L[𝕜] V) (kernel H x x) =
    norm (E := V →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x))
rw₂ rw₃ :
  norm (E := V →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x)) =
    norm (E := V →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x)) (kerFun H x))
⊢ norm (E := V →L[𝕜] V) (kernel H x x) = HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2

Tactic:
rw [sq, ← ContinuousLinearMap.norm_adjoint_comp_self, kernel_apply]

Premises used: RKHS.kernel_apply, sq, ContinuousLinearMap.norm_adjoint_comp_self
-- 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
x : X
rw : norm (E := V →L[𝕜] H) (kerFun H x) = √(HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] H) (kerFun H x)) 2)
rw₁ rw₂ : norm (E := V →L[𝕜] H) (kerFun H x) = norm (E := V →L[𝕜] H) (kerFun H x)
⊢ norm (E := V →L[𝕜] H) (kerFun H x) = √(norm (E := V →L[𝕜] V) (kernel H x x))

Tactic:
rw [norm_kernel_eq_norm_kerFun_sq, Real.sqrt_sq (norm_nonneg _)]

Premises used: Real.sqrt_sq, norm_nonneg, RKHS.norm_kernel_eq_norm_kerFun_sq
-- 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
x y : X
grw :
  norm (E := H →L[𝕜] V) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x) : H →L[𝕜] V) *
      norm (E := V →L[𝕜] H) (kerFun H y) ≤
    √(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))
⊢ norm (E := V →L[𝕜] V) (kernel H x y) ≤
    √(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))

Tactic:
grw [kernel_apply, opNorm_comp_le]

Premises used: RKHS.kernel_apply, ContinuousLinearMap.opNorm_comp_le
-- 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
x y : X
⊢ norm (E := H →L[𝕜] V) ((adjoint : (a : V →L[𝕜] H) → H →L[𝕜] V) (kerFun H x) : H →L[𝕜] V) *
      norm (E := V →L[𝕜] H) (kerFun H y) ≤
    √(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))

Tactic:
simp [norm_kerFun_eq_sqrt_norm_kernel]

Premises used: RKHS.norm_kerFun_eq_sqrt_norm_kernel
-- 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
x y : X
grw :
  HPow.hPow (β := ℕ) (√(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))) 2 ≤
    norm (E := V →L[𝕜] V) (kernel H x x) * norm (E := V →L[𝕜] V) (kernel H y y)
⊢ HPow.hPow (β := ℕ) (norm (E := V →L[𝕜] V) (kernel H x y)) 2 ≤
    norm (E := V →L[𝕜] V) (kernel H x x) * norm (E := V →L[𝕜] V) (kernel H y y)

Tactic:
grw [norm_kernel_le]

Premises used: RKHS.norm_kernel_le
-- 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
x y : X
⊢ HPow.hPow (β := ℕ) (√(norm (E := V →L[𝕜] V) (kernel H x x)) * √(norm (E := V →L[𝕜] V) (kernel H y y))) 2 ≤
    norm (E := V →L[𝕜] V) (kernel H x x) * norm (E := V →L[𝕜] V) (kernel H y y)

Tactic:
simp [mul_pow]

Premises used: mul_pow
-- 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
⊢ Eq.{u_4 + 1} (α := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) ⊤

Tactic:
(orthogonal_eq_bot_iff.mp ((Submodule.eq_bot_iff _).mpr fun f fin ↦ DFunLike.ext f 0 ?_))

Premises used: Iff.mpr, Submodule.orthogonal_eq_bot_iff, DFunLike.ext, Iff.mp, Submodule.eq_bot_iff, OfNat.ofNat
-- 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
refine :
  ∀ (f : H)
    (fin :
      Membership.mem (γ := Submodule 𝕜 H)
        (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f)
    (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((0 : (a : X) → V) x : V)
⊢ Eq.{u_4 + 1} (α := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) ⊤

Tactic:
refine (orthogonal_eq_bot_iff.mp ((Submodule.eq_bot_iff _).mpr fun f fin ↦ DFunLike.ext f 0 ?_))

Premises used: Iff.mpr, Submodule.orthogonal_eq_bot_iff, DFunLike.ext, Iff.mp, Submodule.eq_bot_iff, OfNat.ofNat
-- 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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
⊢ ∀ (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((0 : (a : X) → V) x : V)

Tactic:
fun x ↦ ext_inner_left 𝕜 fun v ↦ ?_

Premises used: ext_inner_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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
refine : ∀ (x : X) (v : V), ⟪v, (f : (a : X) → V) x⟫_𝕜 = ⟪v, (0 : (a : X) → V) x⟫_𝕜
⊢ ∀ (x : X), Eq.{u_3 + 1} (α := V) ((f : (a : X) → V) x : V) ((0 : (a : X) → V) x : V)

Tactic:
refine fun x ↦ ext_inner_left 𝕜 fun v ↦ ?_

Premises used: ext_inner_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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
simp : ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = 0
⊢ ⟪v, (f : (a : X) → V) x⟫_𝕜 = ⟪v, (0 : (a : X) → V) x⟫_𝕜

Tactic:
simp only [← kerFun_inner, coe_zero, Pi.zero_apply, inner_zero_right]

Premises used: Pi.zero_apply, inner_zero_right, RKHS.kerFun_inner, RKHS.coe_zero
-- 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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
⊢ ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = 0

Tactic:
inner_right_of_mem_orthogonal (subset_closure ?_) fin

Premises used: Submodule.inner_right_of_mem_orthogonal
-- 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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
refine :
  Membership.mem (α := H)
    (↑(toAddSubmonoid (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) : Set H)
    ((kerFun H x : (a : V) → H) v : H)
⊢ ⟪(kerFun H x : (a : V) → H) v, f⟫_𝕜 = 0

Tactic:
refine inner_right_of_mem_orthogonal (subset_closure ?_) fin

Premises used: Submodule.inner_right_of_mem_orthogonal
-- 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
f : H
fin :
  Membership.mem (γ := Submodule 𝕜 H)
    (topologicalClosure (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x}))ᗮ f
x : X
v : V
⊢ Membership.mem (α := H)
    (↑(toAddSubmonoid (span 𝕜 {x : H | ∃ (x_1 : X) (v : V), (kerFun H x_1 : (a : V) → H) v = x})) : Set H)
    ((kerFun H x : (a : V) → H) v : H)

Tactic:
simp [mem_span_of_mem]

Premises used: Submodule.mem_span_of_mem
-- 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
a :
  ∀ (i j : X) (x : V),
    Eq (α := V) ((Matrix.conjTranspose (kernel H) i j : (a : V) → V) x : V) ((kernel H i j : (a : V) → V) x : V)
⊢ Matrix.IsHermitian (α := V →L[𝕜] V) (kernel H)

Tactic:
ext
-- 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
i j : X
x : V
⊢ Eq (α := V) ((Matrix.conjTranspose (kernel H) i j : (a : V) → V) x : V) ((kernel H i j : (a : V) → V) x : 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
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
i j : X
x : V
a : ∀ (w : V), ⟪(Matrix.conjTranspose (kernel H) i j : (a : V) → V) x, w⟫_𝕜 = ⟪(kernel H i j : (a : V) → V) x, w⟫_𝕜
⊢ Eq (α := V) ((Matrix.conjTranspose (kernel H) i j : (a : V) → V) x : V) ((kernel H i j : (a : V) → V) x : 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
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
i j : X
x w : V
⊢ ⟪(Matrix.conjTranspose (kernel H) i j : (a : V) → V) x, w⟫_𝕜 = ⟪(kernel H i j : (a : V) → V) x, w⟫_𝕜

Tactic:
simp only [Matrix.conjTranspose_apply, star, adjoint_inner_left,
    ← inner_conj_symm _ (kernel H _ _ _), kernel_inner, inner_conj_symm]

Premises used: ContinuousLinearMap.adjoint_inner_left, RKHS.kernel, Matrix.conjTranspose_apply, RKHS.kernel_inner, DFunLike.coe, inner_conj_symm, 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
⊢ Matrix.PosSemidef (R := V →L[𝕜] V) (kernel H)

Tactic:
⟨isHermitian_kernel H, fun s ↦ (ContinuousLinearMap.isPositive_iff' _).2 ⟨?_, fun v ↦ ?_⟩⟩

Premises used: Iff.mpr, HMul.hMul, RKHS.isHermitian_kernel, HSub.hSub, Finsupp.sum, Matrix.PosSemidef, And.intro, RKHS.kernel, ContinuousLinearMap.isPositive_iff', OfNat.ofNat, 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
refine_1 :
  ∀ (s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)),
    IsSelfAdjoint
      (HSub.hSub (α := V →L[𝕜] V)
        (s.sum fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj) 0)
refine_2 :
  ∀ (s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)) (v : V),
    0 ≤
      ⟪(HSub.hSub (α := V →L[𝕜] V)
              (s.sum fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj)
              0 :
            (a : V) → V)
          v,
        v⟫_𝕜
⊢ Matrix.PosSemidef (R := V →L[𝕜] V) (kernel H)

Tactic:
refine ⟨isHermitian_kernel H, fun s ↦ (ContinuousLinearMap.isPositive_iff' _).2 ⟨?_, fun 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
s : Finsupp.{u_2, u_3} X (V →L[𝕜] V)
refine_1 :
  Eq (α := V →L[𝕜] V)
    (s.sum fun (i : X) (m : V →L[𝕜] V) ↦
      star (fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj) i m)
    (s.sum fun (x' : X) (v' : V →L[𝕜] V) ↦ s.sum fun (x : X) (v : V →L[𝕜] V) ↦ star v * kernel H x x' * v')
⊢ IsSelfAdjoint
    (HSub.hSub (α := V →L[𝕜] V)
      (s.sum fun (i : X) (xi : V →L[𝕜] V) ↦ s.sum fun (j : X) (xj : V →L[𝕜] V) ↦ star xi * kernel H i j * xj) 0)

Tactic:
rw [IsSelfAdjoint, sub_zero, star_finsuppSum, Finsupp.sum_comm]

Premises used: IsSelfAdjoint, Finsupp.sum_comm, sub_zero, star_finsuppSum