awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ≤
    (↑(↑(Fintype.card ι) : NNReal) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        (((linearEquiv ℂ A ((i : ι) → E i) : C⋆ᵐᵒᵈ(A, (i : ι) → E i) ≃ₗ[ℂ] (i : ι) → E i) :
              (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i)
            x :
          (i : ι) → E i)
have simp : ‖x‖ ≤
  (↑(Fintype.card ι) : ℝ) *
    Norm.norm (E := (i : ι) → E i)
      ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)
Tactic: simp only [NNReal.coe_natCast, linearEquiv_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ≤
    (↑(Fintype.card ι) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)
have calc : ∑ x_1 : ι,
    Norm.norm (E := (i : ι) → E i)
      ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i) ≤
  (↑(Fintype.card ι) : ℝ) *
    Norm.norm (E := (i : ι) → E i)
      ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)
Tactic: calc ‖x‖ ≤ ∑ i, ‖x i‖ := pi_norm_le_sum_norm x
      _ ≤ ∑ _, ‖⇑x‖ := Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..
      _ ≤ Fintype.card ι * ‖⇑x‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x : E
⊢ 0 ≤ ⟪x, x⟫_ℂ
have rw : LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) ⟪x, x⟫_ℂ : ℝ)
Tactic: rw [← inner_self_ofReal_re, RCLike.ofReal_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫
have rw : star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫
Tactic: rw [← star_star (r := ⟪x + y, z⟫)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪a •> x, y⟫ = ⟪x, y⟫ * star a
have rw : star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a
Tactic: rw [← star_inner]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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, y⟫ = star z •> ⟪x, y⟫
have rw : star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫
Tactic: rw [← star_inner]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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, y⟫ = z •> ⟪x, y⟫
have h₁ : z •> x = (↑z : ℂ) •> x
Tactic: have h₁ : z • x = (z : ℂ) • x := by simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪z •> x, y⟫ = z •> ⟪x, y⟫
have rw : star ((↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫
Tactic: rw [h₁, ← star_inner, inner_smul_right_complex]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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
⊢ ⟪x, z •> y⟫ = z •> ⟪x, y⟫
have h₁ : z •> y = (↑z : ℂ) •> y
Tactic: have h₁ : z • y = (z : ℂ) • y := by simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪x, z •> y⟫ = z •> ⟪x, y⟫
have rw : star (star (↑z : ℂ) •> ⟪y, x⟫) = z •> ⟪x, y⟫
Tactic: rw [h₁, ← star_inner, inner_smul_left_complex]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ { 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 }
have h : ∀ (x : E),
  Eq.{u_1 + 1} (α := A) (({ toFun := fun (y_1 : E) ↦ ⟪z + y, y_1⟫, map_add' := sorry, map_smul' := sorry } : (a : E) → A) x : A)
    ((HAdd.hAdd (α := E →ₗ[ℂ] A) { toFun := fun (y : E) ↦ ⟪z, y⟫, map_add' := sorry, map_smul' := sorry : E →ₗ[ℂ] A }
            { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := sorry, map_smul' := sorry : E →ₗ[ℂ] A } :
          (a : E) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ { 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 }
have h : ∀ (x : E),
  Eq.{u_1 + 1} (α := A)
    (({ toFun := fun (y_1 : E) ↦ ⟪z •> y, y_1⟫, map_add' := sorry, map_smul' := sorry } : (a : E) → A) x : A)
    ((((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) •>
            { toFun := fun (y_1 : E) ↦ ⟪y, y_1⟫, map_add' := sorry, map_smul' := sorry : E →ₗ[ℂ] A } :
          (a : E) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ 0 < ‖x‖
have simp : ⟪x, x⟫ ≠ 0
Tactic: simp only [norm_eq_sqrt_norm_inner_self (A := A), Real.sqrt_pos, norm_pos_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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
⊢ False
have H₁ : x = 0
Tactic: rw [inner_self] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
have inl : ∀ (h : x = 0), ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
Tactic: rcases eq_or_ne x 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
have inr : ∀ (h : x ≠ 0), ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
Tactic: rcases eq_or_ne x 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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 - 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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 ≤
    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
have bc : a * ⟪x, x⟫_A * star a ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ ‖⟪x, x⟫_A‖ •> (a * star a) = HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a)
have rw : 0 ≤ ‖⟪x, x⟫_A‖
Tactic: rw [Real.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
⊢ HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
Tactic: rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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 * star a)
have calc : ‖⟪x, x⟫_A‖ •> (a * star a) = HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a)
Tactic: calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
calc : ‖⟪x, x⟫_A‖ •> (a * star a) = HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a)
⊢ a * ⟪x, x⟫_A * star a ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
have calc₁ : HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
Tactic: calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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 ≤
    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
have calc : 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A
Tactic: calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      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]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
calc : 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A
⊢ 0 ≤
    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
have calc₁ : ⟪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: calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      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]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (goal)
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
calc : 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A
calc₁ :
  ⟪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
⊢ 0 ≤
    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
have calc₂ : 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: calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      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]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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
have h₁ : ∀ (a : A),
  0 ≤
    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: have h₁ : ∀ (a : A),
        (0 : A) ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := fun a => by
      calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      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]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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
h₁ :
  ∀ (a : A),
    0 ≤
      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
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
have h₂ : 0 ≤
  HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) -
      HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) +
    HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
Tactic: specialize h₁ ⟪x, y⟫
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Defs (hypothesis)
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
h₁ :
  0 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
have h₂ : HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
Tactic: simp only [star_inner, sub_self, zero_sub, le_neg_add_iff_add_le, add_zero] at h₁
Cleared hypotheses: h₁