awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_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 inr : ∀ (h₁ : ⟪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: rwa [smul_le_smul_iff_of_pos_left (pow_pos (CStarModule.norm_pos A h) _)] 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
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * ⟪y, x⟫_A‖
have rw : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * star ⟪x, y⟫_A‖
Tactic: rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
-- 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
rw : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * star ⟪x, y⟫_A‖
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * ⟪y, x⟫_A‖
have rw₁ : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
Tactic: rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
-- 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
rw : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * star ⟪x, y⟫_A‖
rw₁ : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * ⟪y, x⟫_A‖
have rw₂ : ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖ = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
Tactic: rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
-- 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 refine : 0 ≤ ⟪x, y⟫_A * ⟪y, x⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
-- 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
⊢ 0 ≤ ⟪x, y⟫_A * ⟪y, x⟫_A
have rw : 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A
Tactic: rw [← star_inner x]
-- 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
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖
have this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
Tactic: have := calc ‖⟪x, y⟫‖ ^ 2 = ‖⟪x, y⟫ * ⟪y, x⟫‖ := by
                rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
    _ ≤ ‖‖x‖ ^ 2 • ⟪y, y⟫‖ := by
                refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
                rw [← star_inner x]
                exact mul_star_self_nonneg ⟪x, y⟫_A
    _ = ‖x‖ ^ 2 * ‖⟪y, y⟫‖ := by simp [norm_smul]
    _ = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by
                simp only [norm_eq_sqrt_norm_inner_self (A := A), norm_nonneg, Real.sq_sqrt]
    _ = (‖x‖ * ‖y‖) ^ 2 := by simp only [mul_pow]
-- 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
this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖
have refine : 0 ≤ ‖x‖ * ‖y‖
Tactic: refine (pow_le_pow_iff_left₀ (norm_nonneg ⟪x, y⟫_A) ?_ (by simp)).mp this
-- 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
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
have simp : ‖⟪x, x⟫ + ⟪y, x⟫ + ⟪x, y⟫ + ⟪y, y⟫‖ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
Tactic: simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, 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
⊢ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
have bc : ‖⟪x, x⟫ + ⟪y, x⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖
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
⊢ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
have bc : ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖
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
bc : ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖
⊢ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
have bc₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
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
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have simp : HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ = HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖
Tactic: simp only [add_pow_two, add_left_inj]
-- 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
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
Tactic: calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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
calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have calc₁ : ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
Tactic: calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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
calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₁ : ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have calc₂ : ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
Tactic: calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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
calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₁ : ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₂ : ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have calc₃ : ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ =
  HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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
calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₁ : ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₂ : ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
calc₃ :
  ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
have calc₄ : HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
Tactic: calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖
have h : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
Tactic: have h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2 := by
    calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- 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 : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖
have refine : 0 ≤ ‖x‖ + ‖y‖
Tactic: refine (pow_le_pow_iff_left₀ (CStarModule.norm_nonneg A) ?_ (by simp)).mp 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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}
have refine_1 : ‖‖v‖⁻¹ •> v‖ ≤ 1
Tactic: refine Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩
-- 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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
refine_1 : ‖‖v‖⁻¹ •> v‖ ≤ 1
⊢ ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}
have refine_2 : ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖
Tactic: refine Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩
-- 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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
refine_1 : ‖‖v‖⁻¹ •> v‖ ≤ 1
refine_2 : ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖
⊢ ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}
have refine_3 : Membership.mem (γ := Set ℝ) (upperBounds {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}) ‖v‖
Tactic: refine Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩
-- 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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ ‖w‖ * ‖v‖ ≤ 1 * ‖v‖
have ha : 0 ≤ ‖v‖
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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ ‖⟪w, v⟫_A‖ ≤ ‖v‖
have calc : ‖w‖ * ‖v‖ ≤ 1 * ‖v‖
Tactic: calc _ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
      _ ≤ 1 * ‖v‖ := by gcongr
      _ = ‖v‖ := by simp
-- 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
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
calc : ‖w‖ * ‖v‖ ≤ 1 * ‖v‖
⊢ ‖⟪w, v⟫_A‖ ≤ ‖v‖
have calc₁ : 1 * ‖v‖ = ‖v‖
Tactic: calc _ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
      _ ≤ 1 * ‖v‖ := by gcongr
      _ = ‖v‖ := by simp
-- 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 : StarOrderedRing A
inst_3 : SMul A E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℂ E
inst_6 : CStarModule A E
⊢ Continuous.{u_2, u_1} (Y := A) fun (x : E × E) ↦ ⟪x.1, x.2⟫_A
have simp_rw : Continuous.{u_2, u_1} (Y := A) fun (x : E × E) ↦ (((innerSL : (a : E) → E →L[ℂ] A) x.1 : E →L[ℂ] A) : (a : E) → A) x.2
Tactic: simp_rw [← innerSL_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u
A : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
h : a.toProd = b.toProd
⊢ a = b
have mk : ∀ (toProd : (A →L[𝕜] A) × (A →L[𝕜] A))
  (central :
    ∀ (x y : A),
      HMul.hMul (α := A) ((toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd.1 : (a : A) → A) y : A))
  (h : DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } = b.toProd),
  { toProd := toProd, central := central } = b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u
A : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd : (A →L[𝕜] A) × (A →L[𝕜] A)
central :
  ∀ (x y : A),
    HMul.hMul (α := A) ((toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd.1 : (a : A) → A) y : A)
h : DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } = b.toProd
⊢ { toProd := toProd, central := central } = b
have mk : ∀ (toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A))
  (central_1 :
    ∀ (x y : A),
      HMul.hMul (α := A) ((toProd_1.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd_1.1 : (a : A) → A) y : A))
  (h :
    DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } =
      DoubleCentralizer.toProd { toProd := toProd_1, central := central_1 }),
  Eq (α := 𝓜(𝕜, A)) { toProd := toProd, central := central } { toProd := toProd_1, central := central_1 }
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ HMul.hMul (α := A) (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).1 : (a : A) → A) y : A)
have rw : HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
  HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)
Tactic: rw [Prod.snd_natCast, Prod.fst_natCast]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ HMul.hMul (α := A) (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).1 : (a : A) → A) y : A)
have rw : HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
  HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)
Tactic: rw [Prod.snd_intCast, Prod.fst_intCast]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk :
  ∀ (x y : A),
    HMul.hMul (α := A) (((a.toProd ^ k).2 : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x (((a.toProd ^ k).1 : (a : A) → A) y : A)
x y : A
⊢ HMul.hMul (α := A) (((a.toProd ^ (k + 1)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((a.toProd ^ (k + 1)).1 : (a : A) → A) y : A)
have succ : ∀
  (hk :
    ∀ (x y : A),
      HMul.hMul (α := A) ((a.toProd.2 ^ k : (a : A) → A) x : A) y =
        HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) y : A))
  (x y : A),
  HMul.hMul (α := A) ((a.toProd.2 ^ (k + 1) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
Tactic: rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
Cleared hypotheses: hk, x, y
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk :
  ∀ (x y : A),
    HMul.hMul (α := A) ((a.toProd.2 ^ k : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) y : A)
x y : A
⊢ HMul.hMul (α := A) ((a.toProd.2 ^ (k + 1) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
have succ : HMul.hMul (α := A) ((a.toProd.2 * a.toProd.2 ^ k : (a : A) → A) x : A) y =
  HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]