awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
i : Fin 4
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h : ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
      ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4))‖ ≤
  ‖x‖ / 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h_1 : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
i : Fin 4
h :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h₁ : ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
      ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4))‖ ≤
  ‖x‖ / 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h_1 : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
i : Fin 4
h :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
h₁ :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h₂ : ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
      ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4))‖ ≤
  ‖x‖ / 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
x_1 : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h_1 : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
i : Fin 4
h :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
h₁ :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
h₂ :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
have h₃ : ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
      ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4))‖ ≤
  ‖x‖ / 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ Eq (α := Submodule ℂ A) (span ℂ (↑(unitary A) : Set A)) ⊤
have rw : LE.le (α := Submodule ℂ A) ⊤ (span ℂ (↑(unitary A) : Set A))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitary.Span (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(unitary A) : Set A)) x
have obtain : ∀ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ)
  (h : ∀ (i : Fin 4), ‖c i‖ ≤ norm.{u_1} (E := A) (∑ i : Fin 4, c i • (↑(u i) : A)) / 2),
  Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(unitary A) : Set A)) (∑ i : Fin 4, c i • (↑(u i) : A))
Tactic: obtain ⟨u, c, rfl, h⟩ := CStarAlgebra.exists_sum_four_unitary x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
⊢ norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) = ‖a‖
have refine : ‖a‖ ≤ norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)
Tactic: refine le_antisymm
    (opNorm_le_bound _ (norm_nonneg _) fun b => by simpa only [mul_comm] using norm_mul_le b a) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖a‖ ≤ norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)
have suffices : norm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) ≤
  norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)
Tactic: suffices ‖mul 𝕜 E (star a)‖ ≤ ‖(mul 𝕜 E).flip a‖ by
    simpa only [ge_iff_le, opNorm_mul_apply, norm_star] using this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
⊢ norm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)
have refine : ∀ (b : E),
  norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
Tactic: refine opNorm_le_bound _ (norm_nonneg _) fun b => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a b : E
⊢ norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
have calc : norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) =
  norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E)
Tactic: calc ‖mul 𝕜 E (star a) b‖ = ‖(mul 𝕜 E).flip a (star b)‖ := by
        simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)
    _ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖ := by
        simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a b : E
calc :
  norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) =
    norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E)
⊢ norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
have calc₁ : norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E) ≤
  norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
Tactic: calc ‖mul 𝕜 E (star a) b‖ = ‖(mul 𝕜 E).flip a (star b)‖ := by
        simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)
    _ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖ := by
        simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
⊢ nnnorm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) = ‖a‖₊
have rw : sSup
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1) =
  ‖a‖₊
Tactic: rw [← sSup_unitClosedBall_eq_nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
⊢ sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊
have refine_1 : Set.Nonempty (α := NNReal)
  ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
    Metric.closedBall 0 1)
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
refine_1 :
  Set.Nonempty (α := NNReal)
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1)
⊢ sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊
have refine_2 : ∀ (a_1 : NNReal),
  Membership.mem (γ := Set NNReal)
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1)
      a_1 →
    a_1 ≤ ‖a‖₊
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
refine_1 :
  Set.Nonempty (α := NNReal)
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1)
refine_2 :
  ∀ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 →
      a_1 ≤ ‖a‖₊
⊢ sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊
have refine_3 : ∀ (r : NNReal) (hr : r < ‖a‖₊),
  ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
have ha : 0 < ‖a‖₊
Tactic: have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
have hr₁ : r * ‖a‖₊⁻¹ < 1
Tactic: rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr
Cleared hypotheses: hr, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
have refine_3 : ∀ (k : 𝕜) (hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊) (hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹),
  ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
Tactic: obtain ⟨k, hk₁, hk₂⟩ :=
        NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
have refine_3 : Membership.mem (γ := Set E) (Metric.closedBall 0 1) (k • a⋆)
Tactic: refine ⟨_, ⟨k • star a, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : Membership.mem (γ := Set E) (Metric.closedBall 0 1) (k • a⋆)
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1
have refine_3₁ : r < (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) (k • a⋆)
Tactic: refine ⟨_, ⟨k • star a, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) (k • a⋆)
have refine_3 : r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
Tactic: simp only [map_smul, nnnorm_smul, mul_apply', CStarRing.nnnorm_self_mul_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
have refine_3 : r / (‖a‖₊ * ‖a‖₊) < ‖k‖₊
Tactic: rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : r / (‖a‖₊ * ‖a‖₊) < ‖k‖₊
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
have refine_3₁ : r * (‖a‖₊ * ‖a‖₊)⁻¹ < ‖k‖₊
Tactic: rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : r / (‖a‖₊ * ‖a‖₊) < ‖k‖₊
refine_3₁ : r * (‖a‖₊ * ‖a‖₊)⁻¹ < ‖k‖₊
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
have refine_3₂ : r * (‖a‖₊⁻¹ * ‖a‖₊⁻¹) < ‖k‖₊
Tactic: rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2
have refine : norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
  √(norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2)
Tactic: refine (Real.le_sqrt (norm_nonneg _) (norm_nonneg _)).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    √(norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2)
have simp : ‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) x.toProd.1 : E →L[𝕜] E)
      ((mul 𝕜 E : (a : E) → E →L[𝕜] E) x.toProd.2 : E →L[𝕜] E)‖ ≤
  √‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
        ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
        ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E)‖
Tactic: simp only [Unitization.splitMul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) x.toProd.1 : E →L[𝕜] E)
        ((mul 𝕜 E : (a : E) → E →L[𝕜] E) x.toProd.2 : E →L[𝕜] E)‖ ≤
    √‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
          ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
          ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E)‖
have rw : sSup
    ((fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) x.toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) x.toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E)) ''
      Metric.closedBall 0 1) ≤
  √‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
        ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
        ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E)‖
Tactic: rw [← sSup_unitClosedBall_eq_norm]