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
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
refine_2 :
  ∀ (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'⟫_𝕜) :
              ℝ)]
⊢ 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'⟫_𝕜) :
            ℝ)]

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)

Premises used: exists_ne, 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
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
⊢ ∀ (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)) :
        ℝ)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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
⊢ ∀ (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:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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
⊢ ∀
    (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:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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 →₀ 𝕜
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⟫_𝕜) :
      ℝ)
⊢ 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⟫_𝕜) :
      ℝ)

Tactic:
rw [Finsupp.sum_comm]

Premises used: Finsupp.sum_comm
-- 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)
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 : 𝕜) → ℝ)
        (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:
h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) v

Premises used: Norm.norm, ContinuousLinearMap.smulRight, innerSL, Finsupp.sum, HDiv.hDiv, RCLike.ofReal, Prod.fst, HPow.hPow, HSMul.hSMul, OfNat.ofNat, Prod.snd, DFunLike.coe, Finsupp.single
-- 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)
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 →₀ 𝕜
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))
⊢ 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:
convert! h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) v

Premises used: Norm.norm, ContinuousLinearMap.smulRight, innerSL, Finsupp.sum, HDiv.hDiv, RCLike.ofReal, Prod.fst, HPow.hPow, HSMul.hSMul, OfNat.ofNat, Prod.snd, DFunLike.coe, Finsupp.single
-- 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)
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 →₀ 𝕜
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⟫_𝕜)
⊢ 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:
simp [Finsupp.sum_sum_index, inner_add_right, inner_add_left, ← smul_assoc, hv]

Premises used: smul_assoc, inner_add_left, inner_add_right, Finsupp.sum_sum_index
-- 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)
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⟫_𝕜)
    (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 [inner_smul_left, inner_smul_right, ← mul_assoc, mul_comm]

Premises used: mul_assoc, inner_smul_right, mul_comm, 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)
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
⊢ ∀
    (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]
-- 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)
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⟫_𝕜) :
        ℝ)
⊢ ∀ (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:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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⟫_𝕜) :
        ℝ)
⊢ ∀ (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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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⟫_𝕜) :
        ℝ)
⊢ ∀
    (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:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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)
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
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⟫_𝕜) :
        ℝ)
h :
  ∀ (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:
simpa [add_mul, Finsupp.sum_sum_index] using (h (vv.sum fun x v ↦ .single ⟨x, v⟩ 1))

Premises used: add_mul, Finsupp.sum, Prod.mk, OfNat.ofNat, Finsupp.sum_sum_index, Finsupp.single
-- 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)
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⟫_𝕜) :
        ℝ)
⊢ ∀
    (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))