awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
rw : ⟪x i, Pi.single (M := E) i y i⟫_A = ⟪x i, y⟫_A
h₀ : ∀ (b : ι), Membership.mem (γ := Finset ι) Finset.univ b → b ≠ i → ⟪x b, Pi.single (M := E) i y b⟫_A = 0
h₁ : i ∉ Finset.univ → ⟪x i, Pi.single (M := E) i y i⟫_A = 0
⊢ ∑ x_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A

Tactic:
rw [Finset.sum_eq_single i]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪x i, Pi.single (M := E) i y i⟫_A = ⟪x i, y⟫_A

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∀ (b : ι), Membership.mem (γ := Finset ι) Finset.univ b → b ≠ i → ⟪x b, Pi.single (M := E) i y b⟫_A = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single (M := E) i y i⟫_A = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
i : ι
y : E i
x : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ 0 ≤
    Norm.norm (E := C⋆ᵐᵒᵈ(A, (j : ι) → E j))
      ((Equiv.symm (equiv A ((j : ι) → E j)) : (a : (j : ι) → E j) → C⋆ᵐᵒᵈ(A, (j : ι) → E j)) (Pi.single (M := E) i y) :
        C⋆ᵐᵒᵈ(A, (j : ι) → E j))

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
i : ι
y : E i
x : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ 0 ≤ ‖y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
i : ι
y : E i
x : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
rw :
  HPow.hPow (β := ℕ)
      (Norm.norm (E := C⋆ᵐᵒᵈ(A, (j : ι) → E j))
        ((Equiv.symm (equiv A ((j : ι) → E j)) : (a : (j : ι) → E j) → C⋆ᵐᵒᵈ(A, (j : ι) → E j))
            (Pi.single (M := E) i y) :
          C⋆ᵐᵒᵈ(A, (j : ι) → E j)))
      2 =
    HPow.hPow (β := ℕ) ‖y‖ 2
⊢ Norm.norm (E := C⋆ᵐᵒᵈ(A, (j : ι) → E j))
      ((Equiv.symm (equiv A ((j : ι) → E j)) : (a : (j : ι) → E j) → C⋆ᵐᵒᵈ(A, (j : ι) → E j)) (Pi.single (M := E) i y) :
        C⋆ᵐᵒᵈ(A, (j : ι) → E j)) =
    ‖y‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity)]

Premises used: sq_eq_sq₀
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
inst_8 : DecidableEq ι
i : ι
y : E i
x : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ HPow.hPow (β := ℕ)
      (Norm.norm (E := C⋆ᵐᵒᵈ(A, (j : ι) → E j))
        ((Equiv.symm (equiv A ((j : ι) → E j)) : (a : (j : ι) → E j) → C⋆ᵐᵒᵈ(A, (j : ι) → E j))
            (Pi.single (M := E) i y) :
          C⋆ᵐᵒᵈ(A, (j : ι) → E j)))
      2 =
    HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simp [norm_sq_eq A]

Premises used: CStarModule.norm_sq_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
refine : HPow.hPow (β := ℕ) ‖x i‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖x i‖ ≤ ‖x‖

Tactic:
refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2

Premises used: abs_le_of_sq_le_sq', And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
rw : ‖⟪x i, x i⟫_A‖ ≤ Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A)
⊢ HPow.hPow (β := ℕ) ‖x i‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [pi_norm_sq, norm_sq_eq A]

Premises used: CStarModule.norm_sq_eq, WithCStarModule.pi_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖⟪x i, x i⟫_A‖ ≤ Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A)

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
refine : ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A
⊢ ‖⟪x i, x i⟫_A‖ ≤ Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A)

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

Tactic:
Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (A := A) (x := x j)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

Tactic:
exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (A := A) (x := x j)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
rw :
  ∀ (i : ι),
    Norm.norm.{u_3} (E := E i) ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x i : E i) ≤
      ‖x‖
⊢ Norm.norm (E := (i : ι) → E i)
      ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i) ≤
    ‖x‖

Tactic:
rw [pi_norm_le_iff_of_nonneg (by positivity)]

Premises used: pi_norm_le_iff_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x_1 : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ∀ (i : ι),
    Norm.norm.{u_3} (E := E i) ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x i : E i) ≤
      ‖x‖

Tactic:
simpa using norm_apply_le_norm x

Premises used: WithCStarModule.norm_apply_le_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
simp :
  ‖x‖ ≤
    (↑(Fintype.card ι) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)
⊢ ‖x‖ ≤
    (↑(↑(Fintype.card ι) : NNReal) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        (((linearEquiv ℂ A ((i : ι) → E i) : C⋆ᵐᵒᵈ(A, (i : ι) → E i) ≃ₗ[ℂ] (i : ι) → E i) :
              (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i)
            x :
          (i : ι) → E i)

Tactic:
simp only [NNReal.coe_natCast, linearEquiv_apply]

Premises used: WithCStarModule.linearEquiv_apply, NNReal.coe_natCast
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ≤ ∑ i : ι, ‖x i‖

Tactic:
pi_norm_le_sum_norm x

Premises used: WithCStarModule.pi_norm_le_sum_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ LE.le (α := ℝ) (∑ i : ι, ‖x i‖)
    (∑ x_1 : ι,
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i))

Tactic:
Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..

Premises used: norm_le_pi_norm, Finset.sum_le_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ∑ x_1 : ι,
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i) ≤
    (↑(Fintype.card ι) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
calc :
  ∑ x_1 : ι,
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i) ≤
    (↑(Fintype.card ι) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)
⊢ ‖x‖ ≤
    (↑(Fintype.card ι) : ℝ) *
      Norm.norm (E := (i : ι) → E i)
        ((equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x : (i : ι) → E i)

Tactic:
calc ‖x‖ ≤ ∑ i, ‖x i‖ := pi_norm_le_sum_norm x
      _ ≤ ∑ _, ‖⇑x‖ := Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..
      _ ≤ Fintype.card ι * ‖⇑x‖ := by simp

Premises used: norm_le_pi_norm, Fintype.card, WithCStarModule.pi_norm_le_sum_norm, Finset.sum_le_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ ∀ (x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)),
    nnnorm (E := (i : ι) → E i)
        (((linearEquiv ℂ A ((i : ι) → E i) : C⋆ᵐᵒᵈ(A, (i : ι) → E i) ≃ₗ[ℂ] (i : ι) → E i) :
              (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i)
            x :
          (i : ι) → E i) ≤
      1 * ‖x‖₊

Tactic:
simpa using norm_equiv_le_norm_pi

Premises used: WithCStarModule.norm_equiv_le_norm_pi
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, (i : ι) → E i) × C⋆ᵐᵒᵈ(A, (i : ι) → E i))) (𝓤 C⋆ᵐᵒᵈ(A, (i : ι) → E i))
    (𝓤 C⋆ᵐᵒᵈ(A, (i : ι) → E i))

Tactic:
uniformity_eq_of_bilipschitz antilipschitzWith_card_equiv_pi_aux lipschitzWith_one_equiv_pi_aux

Premises used: _private.0.WithCStarModule.lipschitzWith_one_equiv_pi_aux, _private.0.WithCStarModule.antilipschitzWith_card_equiv_pi_aux, uniformity_eq_of_bilipschitz
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
s : Set C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ IsBounded s ↔ IsBounded s

Tactic:
isBounded_iff_of_bilipschitz antilipschitzWith_card_equiv_pi_aux lipschitzWith_one_equiv_pi_aux s

Premises used: isBounded_iff_of_bilipschitz
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, (i : ι) → E i) × C⋆ᵐᵒᵈ(A, (i : ι) → E i))) (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))
    (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))

Tactic:
uniformity_pi_eq_aux

Premises used: _private.0.WithCStarModule.uniformity_pi_eq_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ ∀ (s : Set C⋆ᵐᵒᵈ(A, (i : ι) → E i)), Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
isBounded_pi_iff_aux

Premises used: _private.0.WithCStarModule.isBounded_pi_iff_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, (i : ι) → E i) × C⋆ᵐᵒᵈ(A, (i : ι) → E i))) (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))
    (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))

Tactic:
exacts [uniformity_pi_eq_aux, isBounded_pi_iff_aux]

Premises used: _private.0.WithCStarModule.uniformity_pi_eq_aux, _private.0.WithCStarModule.isBounded_pi_iff_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst_2 : Fintype ι
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → Module ℂ (E i)
inst_5 : (i : ι) → SMul.{u_1, u_3} A (E i)
inst_6 : (i : ι) → CStarModule.{u_1, u_3} A (E i)
inst_7 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, (i : ι) → E i) × C⋆ᵐᵒᵈ(A, (i : ι) → E i))) (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))
    (uniformity C⋆ᵐᵒᵈ(A, (i : ι) → E i))

Tactic:
finally
  exacts [uniformity_pi_eq_aux, isBounded_pi_iff_aux]
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ ∀ {x y z : E}, ⟪x, y + z⟫_ℂ = ⟪x, y⟫_ℂ + ⟪x, z⟫_ℂ

Tactic:
simp [_root_.inner_add_right]

Premises used: inner_add_right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x : E
rw : LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) ⟪x, x⟫_ℂ : ℝ)
⊢ 0 ≤ ⟪x, x⟫_ℂ

Tactic:
rw [← inner_self_ofReal_re, RCLike.ofReal_nonneg]

Premises used: RCLike.ofReal_nonneg, inner_self_ofReal_re
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) ⟪x, x⟫_ℂ : ℝ)

Tactic:
inner_self_nonneg

Premises used: inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℂ) → ℝ) ⟪x, x⟫_ℂ : ℝ)

Tactic:
exact inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ ∀ {x : E}, ⟪x, x⟫_ℂ = 0 ↔ x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ ∀ {a : ℂ} {x y : E}, ⟪x, a • y⟫_ℂ = a * ⟪x, y⟫_ℂ

Tactic:
simp [inner_smul_right]

Premises used: inner_smul_right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
⊢ ∀ {z : ℂ} {x y : E}, ⟪x, z • y⟫_ℂ = z • ⟪x, y⟫_ℂ

Tactic:
simp [inner_smul_right, smul_eq_mul]

Premises used: inner_smul_right, smul_eq_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x x_1 : E
⊢ star ⟪x, x_1⟫_ℂ = ⟪x_1, x⟫_ℂ

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℂ E
x : E
⊢ ‖x‖ = √‖⟪x, x⟫_ℂ‖

Tactic:
simpa only [← inner_self_re_eq_norm] using norm_eq_sqrt_re_inner x

Premises used: inner_self_re_eq_norm, norm_eq_sqrt_re_inner