awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ instCStarModule = instCStarModuleComplex

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ instCStarModule = instCStarModuleComplex

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ Eq (α := Inner ℂ ℂ)
    (@toInner _ _ NonUnitalCommSemiring.toNonUnitalSemiring Complex.instStarRing Semiring.toModule
      NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.partialOrder
      (@SMulZeroClass.toSMul _ _ AddZero.toZero _) Complex.instNorm NormedAddCommGroup.toNorm _)
    (@toInner _ _ NonUnitalRing.toNonUnitalSemiring NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule
      NonUnitalNonAssocRing.toAddCommGroup NormedSpace.toModule Complex.partialOrder instSMulOfMul
      NonUnitalNormedRing.toNorm NonUnitalNormedRing.toNorm _)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
x y z : E
rw : star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
rw [← star_star (r := ⟪x + y, z⟫)]
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
x y z : E
⊢ star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
simp only [inner_add_right, star_add, star_inner]

Premises used: StarAddMonoid.star_add, CStarModule.star_inner, CStarModule.inner_add_right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
a : A
x y : E
rw : star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a
⊢ ⟪a •> x, y⟫ = ⟪x, y⟫ * star a

Tactic:
rw [← star_inner]

Premises used: CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
a : A
x y : E
⊢ star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℂ
x y : E
rw : star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫
⊢ ⟪z •> x, y⟫ = star z •> ⟪x, y⟫

Tactic:
rw [← star_inner]

Premises used: CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℂ
x y : E
⊢ star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> x = (↑z : ℂ) •> x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> x = (↑z : ℂ) •> x

Tactic:
have h₁ : z • x = (z : ℂ) • x := by simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = (↑z : ℂ) •> x
rw : star ((↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫
⊢ ⟪z •> x, y⟫ = z •> ⟪x, y⟫

Tactic:
rw [h₁, ← star_inner, inner_smul_right_complex]

Premises used: CStarModule.inner_smul_right_complex, CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = (↑z : ℂ) •> x
⊢ star ((↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> y = (↑z : ℂ) •> y

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> y = (↑z : ℂ) •> y

Tactic:
have h₁ : z • y = (z : ℂ) • y := by simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = (↑z : ℂ) •> y
rw : star (star (↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫
⊢ ⟪x, z •> y⟫ = z •> ⟪x, y⟫

Tactic:
rw [h₁, ← star_inner, inner_smul_left_complex]

Premises used: CStarModule.inner_smul_left_complex, CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = (↑z : ℂ) •> y
⊢ star (star (↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x z y : E
⊢ ⟪x, z + y⟫ = ⟪x, z⟫ + ⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x : E
z : ℂ
y : E
⊢ ⟪x, z •> y⟫ = ((RingHom.id ℂ : (a : ℂ) → ℂ) z : ℂ) •> ⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z y : E
h :
  ∀ (x : E),
    Eq.{u_1 + 1} (α := A)
      (({ toFun := fun (y_1 : E) ↦ ⟪z + y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } : (a : E) → A) x : A)
      ((HAdd.hAdd (α := E →ₗ[ℂ] A) { toFun := fun (y : E) ↦ ⟪z, y⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A }
              { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A } :
            (a : E) → A)
          x :
        A)
⊢ { toFun := fun (y_1 : E) ↦ ⟪z + y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := E →ₗ[ℂ] A) { toFun := fun (y : E) ↦ ⟪z, y⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A }
      { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A }

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z y x : E
⊢ Eq.{u_1 + 1} (α := A) (({ toFun := fun (y_1 : E) ↦ ⟪z + y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } : (a : E) → A) x : A)
    ((HAdd.hAdd (α := E →ₗ[ℂ] A) { toFun := fun (y : E) ↦ ⟪z, y⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A }
            { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A } :
          (a : E) → A)
        x :
      A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℂ
y : E
h :
  ∀ (x : E),
    Eq.{u_1 + 1} (α := A)
      (({ toFun := fun (y_1 : E) ↦ ⟪z •> y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } : (a : E) → A) x : A)
      ((((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) •>
              { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A } :
            (a : E) → A)
          x :
        A)
⊢ { toFun := fun (y_1 : E) ↦ ⟪z •> y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } =
    ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) •>
      { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A }

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
z : ℂ
y x : E
⊢ Eq.{u_1 + 1} (α := A)
    (({ toFun := fun (y_1 : E) ↦ ⟪z •> y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ } : (a : E) → A) x : A)
    ((((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) •>
            { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := ⋯, map_smul' := ⋯ : E →ₗ[ℂ] A } :
          (a : E) → A)
        x :
      A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x y : E
⊢ (((innerₛₗ : (a : E) → E →ₗ[ℂ] A) x : E →ₗ[ℂ] A) : (a : E) → A) y = ⟪x, y⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x : E
⊢ ⟪x, 0⟫ = 0

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x : E
⊢ ⟪0, x⟫ = 0

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x y : E
⊢ ⟪x, -y⟫ = -⟪x, y⟫

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x y : E
⊢ ⟪-x, y⟫ = -⟪x, y⟫

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x y z : E
⊢ ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
x y z : E
⊢ ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Tactic:
simp [← innerₛₗ_apply]

Premises used: CStarModule.innerₛₗ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
ι : Type u_3
s : Finset ι
x : E
y : ι → E
⊢ ⟪x, ∑ i ∈ s, y i⟫ = ∑ i ∈ s, ⟪x, y i⟫

Tactic:
map_sum (innerₛₗ x) ..

Premises used: CStarModule.innerₛₗ, map_sum, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
inst_10 : StarModule ℂ A
ι : Type u_3
s : Finset ι
x : ι → E
y : E
⊢ ⟪∑ i ∈ s, x i, y⟫ = ∑ i ∈ s, ⟪x i, y⟫

Tactic:
map_sum (innerₛₗ.flip y) ..

Premises used: CStarModule.innerₛₗ, map_sum, LinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : AddCommGroup E
inst_3 : Module ℂ A
inst_4 : Module ℂ E
inst_5 : PartialOrder A
inst_6 : SMul A E
inst_7 : Norm A
inst_8 : Norm E
inst_9 : CStarModule A E
x : E
⊢ IsSelfAdjoint ⟪x, x⟫

Tactic:
star_inner _ _

Premises used: IsSelfAdjoint, CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self (A := A)]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
⊢ 0 ≤ ‖x‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self (A := A)]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
hx : x ≠ 0
simp : ⟪x, x⟫ ≠ 0
⊢ 0 < ‖x‖

Tactic:
simp only [norm_eq_sqrt_norm_inner_self (A := A), Real.sqrt_pos, norm_pos_iff]

Premises used: norm_pos_iff, CStarModule.norm_eq_sqrt_norm_inner_self, Real.sqrt_pos
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
hx : x ≠ 0
H : ⟪x, x⟫ = 0
⊢ x = 0

Tactic:
rw [inner_self] at H

Premises used: CStarModule.inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False

Tactic:
hx H
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False

Tactic:
exact hx H
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
⊢ Norm.norm.{u_2} (E := E) 0 = 0

Tactic:
simp [norm_eq_sqrt_norm_inner_self (A := A)]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
h : ‖x‖ = 0
⊢ x = 0

Tactic:
simpa [norm_eq_sqrt_norm_inner_self (A := A), inner_self] using h

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self, CStarModule.inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
x : E
h : x = 0
⊢ ‖x‖ = 0

Tactic:
simp [h, norm_eq_sqrt_norm_inner_self (A := A)]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
inl : ∀ (h : x = 0), ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
inr : ∀ (h : x ≠ 0), ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
rcases eq_or_ne x 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x = 0
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
simp [h, CStarModule.norm_zero A (E := E)]

Premises used: CStarModule.norm_zero
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A

Tactic:
inner_self_nonneg

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A

Tactic:
exact inner_self_nonneg

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
simp :
  a * (⟪x, x⟫_A * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
      (HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A) =
    a * (⟪x, x⟫_A * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A =
    a * ⟪x, x⟫_A * star a - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
simp only [inner_sub_right, inner_op_smul_right, inner_sub_left,
                        inner_op_smul_left, inner_smul_left_real, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]

Premises used: CStarModule.inner_sub_left, mul_sub, CStarModule.inner_smul_right_real, mul_assoc, CStarModule.inner_sub_right, CStarModule.inner_op_smul_left, smul_sub, CStarModule.inner_smul_left_real, CStarModule.inner_op_smul_right, mul_smul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ a * (⟪x, x⟫_A * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
      (HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A) =
    a * (⟪x, x⟫_A * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
abel
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
bc : a * ⟪x, x⟫_A * star a ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
⊢ a * ⟪x, x⟫_A * star a - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
gcongr