awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ star (↑(unitarySelfAddISMul a ha_norm) : A) = (↑a : A) - I • CFC.sqrt (1 - HPow.hPow (β := ℕ) (↑a : A) 2)

Tactic:
simp [IsSelfAdjoint.star_eq, ← sub_eq_add_neg, (CFC.sqrt_nonneg (1 - a ^ 2 : A)).isSelfAdjoint]

Premises used: LE.le.isSelfAdjoint, sub_eq_add_neg, HSub.hSub, HPow.hPow, CFC.sqrt_nonneg, OfNat.ofNat, Subtype.val, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ IsSelfAdjoint (CFC.sqrt (1 - HPow.hPow (β := ℕ) (↑a : A) 2))

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ ((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑(unitarySelfAddISMul a ha_norm) : A) = a

Tactic:
simp [IsSelfAdjoint.imaginaryPart (x := CFC.sqrt (1 - a ^ 2 : A)) (by cfc_tac)]

Premises used: IsSelfAdjoint.imaginaryPart
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
hx : x ≠ 0
⊢ norm (E := ↥(selfAdjoint A))
      (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x) : ↥(selfAdjoint A)) ≤
    1

Tactic:
simpa [norm_smul, inv_mul_le_one₀ (norm_pos_iff.2 hx)] using realPart.norm_le x

Premises used: Iff.mpr, norm_pos_iff, norm_smul, inv_mul_le_one₀, realPart.norm_le
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) :=
  selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯
⊢ norm (E := ↥(selfAdjoint A))
      (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x) : ↥(selfAdjoint A)) ≤
    1

Tactic:
simpa [norm_smul, inv_mul_le_one₀ (norm_pos_iff.2 hx)] using imaginaryPart.norm_le x

Premises used: Iff.mpr, norm_pos_iff, norm_smul, inv_mul_le_one₀, imaginaryPart.norm_le
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
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)) ⋯
rw :
  x =
    ‖x‖ •
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₁ : A)) : A) +
        HSMul.hSMul (β := A) I (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₂ : A)) : A))
⊢ x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))

Tactic:
rw [smul_add, smul_comm _ I, Unitary.coe_star, Unitary.coe_star,
    ← realPart_apply_coe (u₁ : A), ← realPart_apply_coe (u₂ : A)]

Premises used: realPart_apply_coe, SMulCommClass.smul_comm, Subtype.val, Unitary.coe_star, smul_add, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
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)) ⋯
⊢ x =
    ‖x‖ •
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₁ : A)) : A) +
        HSMul.hSMul (β := A) I (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (↑u₂ : A)) : A))

Tactic:
simpa only [u₁, u₂, selfAdjoint.realPart_unitarySelfAddISMul, realPart_add_I_smul_imaginaryPart]
    using Eq.symm <| NormedSpace.norm_smul_normalize x

Premises used: realPart_add_I_smul_imaginaryPart, selfAdjoint.realPart_unitarySelfAddISMul, NormedSpace.norm_smul_normalize, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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
inl :
  ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ),
    Eq.{u_1 + 1} (α := A) 0 (∑ i : Fin 4, c i • (↑(u i) : A)) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ norm.{u_1} (E := A) 0 / 2
inr :
  ∀ (hx : x ≠ 0),
    ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Tactic:
obtain (rfl | hx) := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
x : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
⊢ Eq.{u_1 + 1} (α := A) 0 (∑ i : Fin 4, HSMul.hSMul (α := ℂ) (β := A) (0 i) (↑(![1, -1, 1, -1] i) : A)) ∧
    ∀ (i : Fin 4), norm (E := ℂ) (0 i) ≤ norm.{u_1} (E := A) 0 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
x : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
h : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ),
    Eq.{u_1 + 1} (α := A) 0 (∑ i : Fin 4, c i • (↑(u i) : A)) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ norm.{u_1} (E := A) 0 / 2

Tactic:
exact ⟨![1, -1, 1, -1], 0, by simp⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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
⊢ have u₁ :=
    selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  have u₂ :=
    selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))

Tactic:
have := norm_smul_two_inv_smul_add_four_unitary x hx
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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
this :
  have u₁ :=
    selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  have u₂ :=
    selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
⊢ let u₁ :=
    selfAdjoint.unitarySelfAddISMul (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  let u₂ :=
    selfAdjoint.unitarySelfAddISMul (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))

Tactic:
extract_lets u₁ u₂ at this
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
h :
  x =
      ∑ i : Fin 4,
        ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
          (↑(![u₁, star u₁, u₂, star u₂] i) : A) ∧
    ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
⊢ ∃ (u : Fin 4 → ↥(unitary A)) (c : Fin 4 → ℂ), x = ∑ i : Fin 4, c i • (↑(u i) : A) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Tactic:
use ![u₁, star u₁, u₂, star u₂], ![‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹ * I, ‖x‖ * 2⁻¹ * I]

Premises used: Star.star, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
h :
  x =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)
h₁ : ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
⊢ x =
      ∑ i : Fin 4,
        ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
          (↑(![u₁, star u₁, u₂, star u₂] i) : A) ∧
    ∀ (i : Fin 4), ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
rw : ‖x‖ • HSMul.hSMul (α := ℝ) 2⁻¹ ((↑u₁ : A) + (↑(star u₁) : A) + I • ((↑u₂ : A) + (↑(star u₂) : A)))
| x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
h :
  ‖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 •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)
⊢ x =
    ∑ i : Fin 4,
      ![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)

Tactic:
conv_lhs => rw [this]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
h :
  (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (↑u₁ : A) + (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (star (↑u₁ : A)) +
      ((↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • (↑u₂ : A)) +
        (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • star (↑u₂ : A))) =
    ((↑‖x‖ : ℂ) * 2⁻¹) • (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹) • star (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹ * I) • (↑u₂ : A) +
      ((↑‖x‖ : ℂ) * 2⁻¹ * I) • star (↑u₂ : A)
⊢ ‖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 •
        (↑(![u₁, star u₁, u₂, star u₂] i) : A)

Tactic:
simp [Fin.sum_univ_four, ← Complex.coe_smul]

Premises used: Fin.sum_univ_four, Complex.coe_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
⊢ (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (↑u₁ : A) + (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (star (↑u₁ : A)) +
      ((↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • (↑u₂ : A)) +
        (↑‖x‖ : ℂ) • HSMul.hSMul (α := ℂ) 2⁻¹ (I • star (↑u₂ : A))) =
    ((↑‖x‖ : ℂ) * 2⁻¹) • (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹) • star (↑u₁ : A) + ((↑‖x‖ : ℂ) * 2⁻¹ * I) • (↑u₂ : A) +
      ((↑‖x‖ : ℂ) * 2⁻¹ * I) • star (↑u₂ : A)

Tactic:
module
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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
h₃ :
  ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
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)))
⊢ ‖![(↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹, (↑‖x‖ : ℂ) * 2⁻¹ * I, (↑‖x‖ : ℂ) * 2⁻¹ * I]
        ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))‖ ≤
    ‖x‖ / 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
rw : LE.le (α := Submodule ℂ A) ⊤ (span ℂ (↑(unitary A) : Set A))
⊢ Eq (α := Submodule ℂ A) (span ℂ (↑(unitary A) : Set A)) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
x : A
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))
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ (↑(unitary A) : Set A)) x

Tactic:
obtain ⟨u, c, rfl, h⟩ := CStarAlgebra.exists_sum_four_unitary x

Premises used: CStarAlgebra.exists_sum_four_unitary, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
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:
sum_mem fun i _ ↦ smul_mem _ _ (subset_span (u i).2)

Premises used: unitary, SetLike.coe, Submodule.span, Submodule.subset_span, Complex, sum_mem, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
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:
exact sum_mem fun i _ ↦ smul_mem _ _ (subset_span (u i).2)

Premises used: unitary, SetLike.coe, Submodule.span, Submodule.subset_span, sum_mem, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
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) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b : E) ≤ ‖a‖ * ‖b‖

Tactic:
simpa only [mul_comm] using norm_mul_le b a

Premises used: mul_comm, norm_mul_le
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
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
refine : ‖a‖ ≤ norm (E := E →L[𝕜] E) ((flip (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) = ‖a‖

Tactic:
refine le_antisymm
    (opNorm_le_bound _ (norm_nonneg _) fun b => by simpa only [mul_comm] using norm_mul_le b a) ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, le_antisymm, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
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
this :
  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)
⊢ ‖a‖ ≤ norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)

Tactic:
simpa only [ge_iff_le, opNorm_mul_apply, norm_star] using this

Premises used: norm_star, ge_iff_le, ContinuousLinearMap.opNorm_mul_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
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
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)
⊢ ‖a‖ ≤ 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