awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ T.IsPositive ↔
    ∃ (m : ℕ) (u : Fin m → E),
      T =
        ∑ i : Fin m,
          (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)

Tactic:
⟨fun hT ↦ ?_, fun ⟨m, u, hT⟩ ↦ hT ▸ isPositive_sum _ fun _ _ ↦ isPositive_rankOne_self _⟩

Premises used: InnerProductSpace.isPositive_rankOne_self, Finset.univ, ContinuousLinearMap.IsPositive, Eq.rec, Iff.intro, _private.0.ContinuousLinearMap.isPositive_iff_eq_sum_rankOne.match_1, Eq.symm, ContinuousLinearMap.isPositive_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
refine :
  ∀ (hT : T.IsPositive),
    ∃ (m : ℕ) (u : Fin m → E),
      T =
        ∑ i : Fin m,
          (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)
⊢ T.IsPositive ↔
    ∃ (m : ℕ) (u : Fin m → E),
      T =
        ∑ i : Fin m,
          (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)

Tactic:
refine ⟨fun hT ↦ ?_, fun ⟨m, u, hT⟩ ↦ hT ▸ isPositive_sum _ fun _ _ ↦ isPositive_rankOne_self _⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
⊢ ∃ (m : ℕ) (u : Fin m → E),
    T =
      ∑ i : Fin m, (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)

Tactic:
⟨Module.finrank 𝕜 E, a, ext fun _ ↦ ?_⟩

Premises used: Exists.intro, ContinuousLinearMap.ext, Module.finrank
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
refine :
  ∀ (x : E),
    Eq (α := E) ((T : (a : E) → E) x : E)
      ((∑ i : Fin (Module.finrank 𝕜 E),
              (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
            (a : E) → E)
          x :
        E)
⊢ ∃ (m : ℕ) (u : Fin m → E),
    T =
      ∑ i : Fin m, (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)

Tactic:
refine ⟨Module.finrank 𝕜 E, a, ext fun _ ↦ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
have : ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
rw :
  (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
      Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
            ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (∑ i : Fin m,
            (((rankOne 𝕜 :
                      (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                    (u i) :
                  EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              (u i) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]

Premises used: ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, LinearMap.isPositive_toContinuousLinearMap_iff, Matrix.isPositive_toEuclideanLin_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
simp_rw :
  (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
      Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
            ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (∑ i : Fin m,
            (((rankOne 𝕜 :
                      (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                    (u i) :
                  EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              (u i) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]

Premises used: LinearEquiv.symm_apply_eq, map_sum, eq_comm, ContinuousLinearMap.coe_sum, LinearMap.coe_toContinuousLinearMap_symm, InnerProductSpace.symm_toEuclideanLin_rankOne
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩

Premises used: Finset.univ, _private.0.Matrix.posSemidef_iff_eq_sum_vecMulVec.match_3, Exists, WithLp.toLp, Iff.intro, Exists.intro, _private.0.Matrix.posSemidef_iff_eq_sum_vecMulVec.match_2, OfNat.ofNat, Eq, WithLp.ofLp, Finset.sum, Matrix.vecMulVec, Star.star
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
have have₁ have₂ :
  ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have₃ :
  ∀ (this : Fintype n),
    (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
        Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (((toContinuousLinearMap :
                  (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (∑ i : Fin m,
              (((rankOne 𝕜 :
                        (a : EuclideanSpace 𝕜 n) →
                          EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                      (u i) :
                    EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                  (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                (u i) :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
      ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have₄ :
  ∀ (this : Fintype n),
    (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
      ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))

Tactic:
classical
  have := Fintype.ofFinite n
  rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
  simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
  exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩

Premises used: ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, LinearEquiv.symm_apply_eq, LinearMap.isPositive_toContinuousLinearMap_iff, Matrix.isPositive_toEuclideanLin_iff, map_sum, eq_comm, ContinuousLinearMap.coe_sum, LinearMap.coe_toContinuousLinearMap_symm, InnerProductSpace.symm_toEuclideanLin_rankOne
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : WithLp 2 (E × F)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (RCLike.re : (a : 𝕜) → ℝ) (⟪x.fst, x.fst⟫_𝕜 + ⟪x.snd, x.snd⟫_𝕜)

Tactic:
simp [prod_norm_sq_eq_of_L2]

Premises used: WithLp.prod_norm_sq_eq_of_L2
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (⟪y.fst, x.fst⟫_𝕜 + ⟪y.snd, x.snd⟫_𝕜) = ⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y z : WithLp 2 (E × F)
simp :
  ⟪x.fst, z.fst⟫_𝕜 + ⟪y.fst, z.fst⟫_𝕜 + (⟪x.snd, z.snd⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜) =
    ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)
⊢ ⟪(x + y).fst, z.fst⟫_𝕜 + ⟪(x + y).snd, z.snd⟫_𝕜 =
    ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)

Tactic:
simp only [add_fst, add_snd, inner_add_left]

Premises used: WithLp.add_snd, inner_add_left, WithLp.add_fst
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y z : WithLp 2 (E × F)
⊢ ⟪x.fst, z.fst⟫_𝕜 + ⟪y.fst, z.fst⟫_𝕜 + (⟪x.snd, z.snd⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜) =
    ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
r : 𝕜
simp :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.fst, y.fst⟫_𝕜 +
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.snd, y.snd⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)
⊢ ⟪(r • x).fst, y.fst⟫_𝕜 + ⟪(r • x).snd, y.snd⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)

Tactic:
simp only [smul_fst, inner_smul_left, smul_snd]

Premises used: WithLp.smul_snd, WithLp.smul_fst, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
r : 𝕜
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.fst, y.fst⟫_𝕜 +
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.snd, y.snd⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
⊢ ⟪x, y⟫_𝕜 = ⟪x.ofLp.1, y.ofLp.1⟫_𝕜 + ⟪x.ofLp.2, y.ofLp.2⟫_𝕜

Tactic:
rfl

Premises used: WithLp.snd, WithLp.fst, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
left :
  ∀ (i : ι₁ ⊕ ι₂),
    norm (E := WithLp 2 (E × F))
        (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            i :
          WithLp 2 (E × F)) =
      1
right :
  Pairwise fun (i j : ι₁ ⊕ ι₂) ↦
    inner 𝕜 (E := WithLp 2 (E × F))
        (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            i :
          WithLp 2 (E × F))
        (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            j :
          WithLp 2 (E × F)) =
      0
⊢ Orthonormal 𝕜 (E := WithLp 2 (E × F)) (ι := ι₁ ⊕ ι₂)
    (⇑((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F)))) :
      (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ ∀ (i : ι₁ ⊕ ι₂),
    norm (E := WithLp 2 (E × F))
        (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            i :
          WithLp 2 (E × F)) =
      1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
right :
  (∀ (a a_1 : ι₁), ¬a = a_1 → inner.{u_1, u_4} 𝕜 (E := E) ((v : (a : ι₁) → E) a : E) ((v : (a : ι₁) → E) a_1 : E) = 0) ∧
    ∀ (b b_1 : ι₂), ¬b = b_1 → inner.{u_1, u_5} 𝕜 (E := F) ((w : (a : ι₂) → F) b : F) ((w : (a : ι₂) → F) b_1 : F) = 0
⊢ ∀ ⦃i j : ι₁ ⊕ ι₂⦄,
    i ≠ j →
      (fun (i j : ι₁ ⊕ ι₂) ↦
          inner 𝕜 (E := WithLp 2 (E × F))
              (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
                    (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
                  i :
                WithLp 2 (E × F))
              (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
                    (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
                  j :
                WithLp 2 (E × F)) =
            0)
        i j

Tactic:
simp only [ne_eq, Basis.map_apply, Basis.prod_apply, LinearMap.coe_inl,
        OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.coe_symm_linearEquiv,
        WithLp.prod_inner_apply, Sum.forall, Sum.elim_inl, Function.comp_apply, inner_zero_right,
        add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq, reduceCtorEq, not_false_eq_true,
        inner_zero_left, imp_self, implies_true, and_true, Sum.inr.injEq, true_and]

Premises used: WithLp.prod_inner_apply, reduceCtorEq, and_true, LinearMap.coe_inr, Sum.inr.injEq, Module.Basis.prod_apply, inner_zero_left, Sum.inl.injEq, zero_add, OrthonormalBasis.coe_toBasis, ne_eq, inner_zero_right, Sum.elim_inr, Module.Basis.map_apply, LinearMap.coe_inl, imp_self, Sum.elim_inl, Function.comp_apply, implies_true, Sum.forall, add_zero, not_false_eq_true, WithLp.coe_symm_linearEquiv, true_and
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a a_1 : ι₁), ¬a = a_1 → inner.{u_1, u_4} 𝕜 (E := E) ((v : (a : ι₁) → E) a : E) ((v : (a : ι₁) → E) a_1 : E) = 0) ∧
    ∀ (b b_1 : ι₂), ¬b = b_1 → inner.{u_1, u_5} 𝕜 (E := F) ((w : (a : ι₂) → F) b : F) ((w : (a : ι₂) → F) b_1 : F) = 0

Tactic:
⟨v.orthonormal.2, w.orthonormal.2⟩

Premises used: And.right, OrthonormalBasis.orthonormal, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a a_1 : ι₁), ¬a = a_1 → inner.{u_1, u_4} 𝕜 (E := E) ((v : (a : ι₁) → E) a : E) ((v : (a : ι₁) → E) a_1 : E) = 0) ∧
    ∀ (b b_1 : ι₂), ¬b = b_1 → inner.{u_1, u_5} 𝕜 (E := F) ((w : (a : ι₂) → F) b : F) ((w : (a : ι₂) → F) b_1 : F) = 0

Tactic:
exact ⟨v.orthonormal.2, w.orthonormal.2⟩
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
rw :
  (∀ (a : ι₁),
      Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) (Sum.inl a) : WithLp 2 (E × F))
        (Sum.elim (β := ι₂)
            (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
            (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
            (Sum.inl a) :
          WithLp 2 (E × F))) ∧
    ∀ (b : ι₂),
      Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) (Sum.inr b) : WithLp 2 (E × F))
        (Sum.elim (α := ι₁)
            (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
            (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
            (Sum.inr b) :
          WithLp 2 (E × F))
⊢ ∀ (i : ι₁ ⊕ ι₂),
    Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) i : WithLp 2 (E × F))
      (Sum.elim (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
          (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F)) i :
        WithLp 2 (E × F))

Tactic:
rw [Sum.forall]

Premises used: Sum.forall
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      Eq (α := WithLp 2 (E × F))
        ((Basis.toOrthonormalBasis ((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))))
                ⋯ :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            (Sum.inl a) :
          WithLp 2 (E × F))
        (Sum.elim (β := ι₂)
            (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
            (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
            (Sum.inl a) :
          WithLp 2 (E × F))) ∧
    ∀ (b : ι₂),
      Eq (α := WithLp 2 (E × F))
        ((Basis.toOrthonormalBasis ((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))))
                ⋯ :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            (Sum.inr b) :
          WithLp 2 (E × F))
        (Sum.elim (α := ι₁)
            (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
            (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
            (Sum.inr b) :
          WithLp 2 (E × F))

Tactic:
aesop
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x x_1 : E
⊢ 0 ≤
    norm (E := WithLp 2 (↥K × ↥Kᗮ))
      (((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)) :
            (a : E) → WithLp 2 (↥K × ↥Kᗮ))
          x_1 :
        WithLp 2 (↥K × ↥Kᗮ))

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x x_1 : E
⊢ 0 ≤ ‖x_1‖

Tactic:
positivity