awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
hx : 0 ≤ x ∧ ‖x‖ < 1
⊢ (0 ≤ x ∧ ‖x‖ < 1) ∧
    ∀ ⦃x_1 : A⦄, Membership.mem (γ := Set A) ({x_2 : A | x ≤ x_2} ∩ closedBall 0 1) x_1 → IsSelfAdjoint x_1

Tactic:
⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩

Premises used: LE.le.isSelfAdjoint, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
hx : 0 ≤ x ∧ ‖x‖ < 1
⊢ (0 ≤ x ∧ ‖x‖ < 1) ∧
    ∀ ⦃x_1 : A⦄, Membership.mem (γ := Set A) ({x_2 : A | x ≤ x_2} ∩ closedBall 0 1) x_1 → IsSelfAdjoint x_1

Tactic:
exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
i : A
hx : 0 ≤ i ∧ ‖i‖ < 1
⊢ Membership.mem (γ := Set A) (closedBall 0 1) i

Tactic:
simpa using hx.2.le

Premises used: LT.lt.le, And.right
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ (LE.le.{u_1} (α := A) 0 0 ∧ norm.{u_1} (E := A) 0 < 1) ∧
    ∀ ⦃x : A⦄, Membership.mem (γ := Set A) {x : A | 0 ≤ x} x → 0 ≤ x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ ∀ᶠ (x : A) in 𝓟 (closedBall 0 1), ‖x‖ ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : StarAddMonoid E
inst_2 : NormedStarGroup E
x : E
⊢ ‖x‖ ≤ ‖x⋆‖

Tactic:
simpa using NormedStarGroup.norm_star_le x⋆

Premises used: NormedStarGroup.norm_star_le, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : StarAddMonoid E
inst_2 : NormedStarGroup E
x : E
⊢ ‖x⋆‖₊ = ‖x‖₊

Tactic:
Subtype.ext <| norm_star _

Premises used: norm_star, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : StarAddMonoid E
inst_2 : NormedStarGroup E
⊢ Isometry.{u_2, u_2} (α := E) star

Tactic:
show Isometry starAddEquiv from
    AddMonoidHomClass.isometry_of_norm starAddEquiv (show ∀ x, ‖x⋆‖ = ‖x‖ from norm_star)

Premises used: norm_star, AddMonoidHomClass.isometry_of_norm, starAddEquiv
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : StarAddMonoid E
inst_2 : NormedStarGroup E
⊢ ContinuousStar E

Tactic:
⟨star_isometry.continuous⟩

Premises used: star_isometry, ContinuousStar.mk, Isometry.continuous
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NormedCommRing E
inst_1 : StarRing E
inst_2 : NormedStarGroup E
⊢ RingHomIsometric (_root_.starRingEnd E)

Tactic:
⟨@norm_star _ _ _ _⟩

Premises used: norm_star, RingHomIsometric.mk
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
x : ℝ
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
simp only [Real.norm_eq_abs, abs_mul_abs_self, star, id, norm_mul, le_refl]

Premises used: le_refl, id, norm_mul, abs_mul_abs_self, Real.norm_eq_abs, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
inr : ∀ (hx : 0 < ‖x⋆‖), ‖x⋆‖ ≤ ‖x‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆

Premises used: eq_zero_or_norm_pos, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : x⋆ = 0
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
le_of_mul_le_mul_right ?_ hx

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
inr : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
refine le_of_mul_le_mul_right ?_ hx

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖

Tactic:
simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _

Premises used: Norm.norm, sq, mul_comm, LE.le.trans, norm_mul_le, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
this : NormedStarGroup E
⊢ ∀ (x : E), ‖x⋆‖ * ‖x⋆‖ ≤ ‖x⋆⋆ * x⋆‖

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
inr : ∀ (hx : 0 < ‖x⋆‖), ‖x⋆‖ ≤ ‖x‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆

Premises used: eq_zero_or_norm_pos, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : x⋆ = 0
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
le_of_mul_le_mul_right ?_ hx

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : 0 < ‖x⋆‖
inr : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
refine le_of_mul_le_mul_right ?_ hx

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖

Tactic:
simpa using norm_mul_self_le (x := x⋆) |>.trans <| norm_mul_le _ _

Premises used: CStarRing.norm_mul_self_le, LE.le.trans, norm_mul_le, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
rw rw₁ : ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖
⊢ ‖x⋆‖ * ‖x‖ ≤ ‖x‖ * ‖x‖

Tactic:
rw [norm_star]

Premises used: norm_star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
nth_rw : ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
nth_rw 1 [← star_star x]

Premises used: star_star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
simp only [norm_star_mul_self, norm_star]

Premises used: norm_star, CStarRing.norm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
rw : ‖x‖ * ‖x‖ = ‖x⋆‖ * ‖x‖
rw₁ rw₂ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖

Tactic:
rw [norm_star_mul_self, norm_star]

Premises used: norm_star, CStarRing.norm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x * x⋆‖₊ = ‖x‖₊ * ‖x‖₊

Tactic:
Subtype.ext norm_self_mul_star

Premises used: NNReal, CStarRing.norm_self_mul_star, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x⋆ * x‖₊ = ‖x‖₊ * ‖x‖₊

Tactic:
Subtype.ext norm_star_mul_self

Premises used: NNReal, CStarRing.norm_star_mul_self, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x * x‖ = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simpa [sq, hx.star_eq] using CStarRing.norm_star_mul_self (x := x)

Premises used: sq, CStarRing.norm_star_mul_self, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x * x‖₊ = HPow.hPow (β := ℕ) ‖x‖₊ 2

Tactic:
Subtype.ext hx.norm_mul_self

Premises used: IsSelfAdjoint.norm_mul_self, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
rw : ‖x‖ * ‖x‖ = 0 ↔ x = 0
⊢ x⋆ * x = 0 ↔ x = 0

Tactic:
rw [← norm_eq_zero, norm_star_mul_self]

Premises used: norm_eq_zero, CStarRing.norm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0

Tactic:
mul_self_eq_zero.trans norm_eq_zero

Premises used: norm_eq_zero, mul_self_eq_zero, Iff.trans
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0

Tactic:
exact mul_self_eq_zero.trans norm_eq_zero

Premises used: norm_eq_zero, mul_self_eq_zero, Iff.trans
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ x⋆ * x ≠ 0 ↔ x ≠ 0

Tactic:
simp only [Ne, star_mul_self_eq_zero_iff]

Premises used: CStarRing.star_mul_self_eq_zero_iff, Ne
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ x * x⋆ = 0 ↔ x = 0

Tactic:
simpa only [star_eq_zero, star_star] using @star_mul_self_eq_zero_iff _ _ _ _ (star x)

Premises used: star_eq_zero, star_star, CStarRing.star_mul_self_eq_zero_iff, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ x * x⋆ ≠ 0 ↔ x ≠ 0

Tactic:
simp only [Ne, mul_star_self_eq_zero_iff]

Premises used: Ne, CStarRing.mul_star_self_eq_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
simp : HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ max (HPow.hPow (β := ℕ) ‖x.1‖ 2) (HPow.hPow (β := ℕ) ‖x.2‖ 2)
⊢ max ‖x.1‖ ‖x.2‖ * max ‖x.1‖ ‖x.2‖ ≤ max ‖(x⋆ * x).1‖ ‖(x⋆ * x).2‖

Tactic:
simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]

Premises used: sq, Prod.snd_mul, CStarRing.norm_star_mul_self, Prod.fst_mul, Prod.snd_star, Prod.fst_star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
rw :
  HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ max (HPow.hPow (β := ℕ) ‖x.1‖ 2) (HPow.hPow (β := ℕ) ‖x.2‖ 2)

Tactic:
rw [le_sup_iff]

Premises used: le_sup_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
inl :
  ∀ (h : ‖x.1‖ ≤ ‖x.2‖),
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
      HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
inr :
  ∀ (h : ‖x.2‖ ≤ ‖x.1‖),
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
      HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2

Tactic:
rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)

Premises used: Norm.norm, le_total, Prod.fst, Prod.snd
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
h : ‖x.1‖ ≤ ‖x.2‖
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2

Tactic:
simp [h]
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
h : ‖x.2‖ ≤ ‖x.1‖
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2

Tactic:
simp [h]
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
le_of_eq (Eq.symm ?_)

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
refine : ‖x⋆ * x‖ = ‖x‖ * ‖x‖
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
refine le_of_eq (Eq.symm ?_)

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
simp :
  (↑(Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) : ℝ) =
    HPow.hPow (β := ℕ) (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ) 2
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖

Tactic:
simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]

Premises used: Norm.norm, Pi.mul_apply, sq, Pi.star_apply, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
norm_cast :
  (Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) =
    HPow.hPow (α := NNReal) (β := ℕ) (Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) 2
⊢ (↑(Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) : ℝ) =
    HPow.hPow (β := ℕ) (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ) 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x_1 : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ LE.le (α := NNReal) ((fun (x : NNReal) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : NNReal) ↦ HPow.hPow (β := ℕ) x 2) y)

Tactic:
simpa only [sq] using mul_le_mul' h h

Premises used: sq, mul_le_mul'
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ Eq (α := NNReal) ((fun (x : NNReal) ↦ HPow.hPow (β := ℕ) x 2) ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ (Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) =
    HPow.hPow (α := NNReal) (β := ℕ) (Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) 2

Tactic:
exact
      (Finset.comp_sup_eq_sup_comp_of_is_total (fun x : NNReal => x ^ 2)
          (fun x y h => by simpa only [sq] using mul_le_mul' h h) (by simp)).symm

Premises used: Finset.comp_sup_eq_sup_comp_of_is_total, HPow.hPow, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
⊢ CStarRing (ι → R₁)

Tactic:
Pi.cstarRing

Premises used: Pi.cstarRing
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
⊢ 0 < norm.{u_2} (E := E) 1

Tactic:
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
rw₁ : ‖HMul.hMul (α := E) 1⋆ 1‖ = 1 * norm.{u_2} (E := E) 1
rw₂ : norm.{u_2} (E := E) 1⋆ = 1 * norm.{u_2} (E := E) 1
rw₃ : norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
rw₄ rw₅ : norm.{u_2} (E := E) 1 = norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1

Tactic:
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]

Premises used: CStarRing.norm_star_mul_self, LT.lt.ne', mul_one, mul_left_inj', one_mul, star_one
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
⊢ NormOneClass E

Tactic:
⟨norm_one⟩

Premises used: NormOneClass.mk, CStarRing.norm_one
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
rw₂ : ‖(↑U : E)‖ * ‖(↑U : E)‖ = 1
rw₃ : ‖(↑U : E)⋆ * (↑U : E)‖ = 1
rw₄ : norm.{u_2} (E := E) 1 = 1
rw₅ rw₆ : Eq (α := ℝ) 1 1
⊢ ‖(↑U : E)‖ = 1

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]

Premises used: one_pow, sq, zero_le_one, CStarRing.norm_star_mul_self, sq_eq_sq₀, OfNat.ofNat, Unitary.coe_star_mul_self, norm_nonneg, CStarRing.norm_one
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : E
hU : Membership.mem (γ := Submonoid E) (unitary E) U
⊢ ‖U‖ = 1

Tactic:
norm_coe_unitary ⟨U, hU⟩

Premises used: Subtype.mk, CStarRing.norm_coe_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
U : ↥(unitary E)
A : E
rw : HPow.hPow (β := ℕ) ‖(↑U : E) * A‖ 2 = HPow.hPow (β := ℕ) ‖A‖ 2
⊢ ‖(↑U : E) * A‖ = ‖A‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]

Premises used: sq_eq_sq₀, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
U : ↥(unitary E)
A : E
⊢ HPow.hPow (β := ℕ) ‖(↑U : E) * A‖ 2 = HPow.hPow (β := ℕ) ‖A‖ 2

Tactic:
simp [sq, ← CStarRing.norm_star_mul_self, mul_assoc, ← mul_assoc (U : E)⋆]

Premises used: mul_assoc, sq, CStarRing.norm_star_mul_self, Subtype.val, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖U • A‖ = ‖A‖

Tactic:
norm_coe_unitary_mul U A

Premises used: CStarRing.norm_coe_unitary_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
U A : E
hU : Membership.mem (γ := Submonoid E) (unitary E) U
⊢ ‖U * A‖ = ‖A‖

Tactic:
norm_coe_unitary_mul ⟨U, hU⟩ A

Premises used: Subtype.mk, CStarRing.norm_coe_unitary_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖A * (↑U : E)‖ = ‖A‖

Tactic:
simpa [← norm_star (A * U)] using norm_coe_unitary_mul (star U) (star A)

Premises used: norm_star, HMul.hMul, CStarRing.norm_coe_unitary_mul, Subtype.val, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
A U : E
hU : Membership.mem (γ := Submonoid E) (unitary E) U
⊢ ‖A * U‖ = ‖A‖

Tactic:
norm_mul_coe_unitary A ⟨U, hU⟩

Premises used: CStarRing.norm_mul_coe_unitary, Subtype.mk
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp only [pow_zero, pow_one]

Premises used: pow_zero, pow_one