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
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h₁ : ‖x.1‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
h₂ : ‖x.2‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
⊢ ‖x.1‖ + ‖x.2‖ ≤
    Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F) +
      Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
norm_fst_le x

Premises used: norm_fst_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
exact norm_fst_le x

Premises used: norm_fst_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.2‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
norm_snd_le x

Premises used: norm_snd_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.2‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
exact norm_snd_le x

Premises used: norm_snd_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ ∀ (x : C⋆ᵐᵒᵈ(A, E × F)),
    nnnorm (E := E × F)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F) ≤
      1 * ‖x‖₊

Tactic:
simpa using norm_equiv_le_norm_prod

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

Tactic:
uniformity_eq_of_bilipschitz antilipschitzWith_two_equiv_prod_aux lipschitzWith_one_equiv_prod_aux

Premises used: Set.Mem, setOf, _private.0.WithCStarModule.lipschitzWith_one_equiv_prod_aux, WithCStarModule, uniformity_eq_of_bilipschitz, _private.0.WithCStarModule.antilipschitzWith_two_equiv_prod_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
s : Set C⋆ᵐᵒᵈ(A, E × F)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
isBounded_iff_of_bilipschitz antilipschitzWith_two_equiv_prod_aux
    lipschitzWith_one_equiv_prod_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
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, E × F) × C⋆ᵐᵒᵈ(A, E × F))) (uniformity C⋆ᵐᵒᵈ(A, E × F)) (uniformity C⋆ᵐᵒᵈ(A, E × F))

Tactic:
uniformity_prod_eq_aux

Premises used: WithCStarModule, _private.0.WithCStarModule.uniformity_prod_eq_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ ∀ (s : Set C⋆ᵐᵒᵈ(A, E × F)), Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
isBounded_prod_iff_aux

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

Tactic:
exacts [uniformity_prod_eq_aux, isBounded_prod_iff_aux]

Premises used: _private.0.WithCStarModule.isBounded_prod_iff_aux, _private.0.WithCStarModule.uniformity_prod_eq_aux
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ Eq (α := Filter (C⋆ᵐᵒᵈ(A, E × F) × C⋆ᵐᵒᵈ(A, E × F))) (uniformity C⋆ᵐᵒᵈ(A, E × F)) (uniformity C⋆ᵐᵒᵈ(A, E × F))

Tactic:
finally
  exacts [uniformity_prod_eq_aux, isBounded_prod_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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ = √(Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A))

Tactic:
rfl
-- 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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ = √(Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A))

Tactic:
with_reducible_and_instances rfl
-- 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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A)

Tactic:
simp [pi_norm]

Premises used: WithCStarModule.pi_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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖)

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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
refine : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) (∑ i : ι, ‖x i‖) 2
⊢ ‖x‖ ≤ ∑ i : ι, ‖x i‖

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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ Eq (α := ℝ) (∑ i : ι, ‖⟪x i, x i⟫_A‖) (∑ i : ι, HPow.hPow (β := ℕ) ‖x i‖ 2)

Tactic:
simp only [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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ∑ i : ι, HPow.hPow (β := ℕ) ‖x i‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) (∑ i : ι, ‖x i‖) 2

Tactic:
sum_sq_le_sq_sum_of_nonneg (fun _ _ ↦ norm_nonneg _)

Premises used: Finset.sum_sq_le_sq_sum_of_nonneg, norm_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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
calc : Eq (α := ℝ) (∑ i : ι, ‖⟪x i, x i⟫_A‖) (∑ i : ι, HPow.hPow (β := ℕ) ‖x i‖ 2)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) (∑ i : ι, ‖x i‖) 2

Tactic:
calc ‖x‖ ^ 2 ≤ ∑ i, ‖⟪x i, x i⟫_A‖ := pi_norm_sq x ▸ norm_sum_le _ _
    _ = ∑ i, ‖x i‖ ^ 2 := by simp only [norm_sq_eq A]
    _ ≤ (∑ i, ‖x i‖) ^ 2 := sum_sq_le_sq_sum_of_nonneg (fun _ _ ↦ norm_nonneg _)

Premises used: Norm.norm, Finset.univ, Finset.sum_sq_le_sq_sum_of_nonneg, norm_nonneg, Finset.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 y z : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ∑ i : ι, ⟪x i, (y + z) i⟫_A = HAdd.hAdd (α := A) (∑ i : ι, ⟪x i, y i⟫_A) (∑ i : ι, ⟪x i, z i⟫_A)

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- 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)
h : x = 0
⊢ Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0

Tactic:
simp [h]
-- 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)
refine : ∀ (h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0), x = 0
⊢ Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- 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)
h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0
h₁ : ∀ (i : ι), x i = 0 i
⊢ x = 0

Tactic:
ext i
-- 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)
h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0
i : ι
⊢ x i = 0 i

Tactic:
inner_self.mp <| le_antisymm (le_of_le_of_eq ?_ h) inner_self_nonneg

Premises used: le_of_le_of_eq, CStarModule.inner_self, le_antisymm, Iff.mp, 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)
h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0
i : ι
h₁ : ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A
⊢ x i = 0 i

Tactic:
refine inner_self.mp <| le_antisymm (le_of_le_of_eq ?_ h) inner_self_nonneg

Premises used: le_of_le_of_eq, CStarModule.inner_self, le_antisymm, Iff.mp, 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)
h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0
i : ι
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

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

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)
h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0
i : ι
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

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

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
⊢ ∀ {a : A} {x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)}, ∑ i : ι, ⟪x i, (a • y) i⟫_A = a * ∑ i : ι, ⟪x i, y i⟫_A

Tactic:
simp [mul_sum]

Premises used: Finset.mul_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
⊢ ∀ {z : ℂ} {x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)},
    ∑ i : ι, ⟪x i, (z • y) i⟫_A = HSMul.hSMul (β := A) z (∑ i : ι, ⟪x i, y i⟫_A)

Tactic:
simp [smul_sum]

Premises used: Finset.smul_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 y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ Eq.{u_1 + 1} (α := A) (star (∑ i : ι, ⟪x i, y i⟫_A)) (∑ i : ι, ⟪y i, x i⟫_A)

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)
⊢ ‖x‖ = √(Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A))

Tactic:
rfl
-- 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‖ = √(Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A))

Tactic:
with_reducible_and_instances rfl
-- 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 y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ⟪x, y⟫_A = ∑ i : ι, ⟪x i, y i⟫_A

Tactic:
rfl

Premises used: rfl
-- 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
simp : ∑ x_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_A
⊢ ⟪(Equiv.symm (equiv A ((j : ι) → E j)) : (a : (j : ι) → E j) → C⋆ᵐᵒᵈ(A, (j : ι) → E j)) (Pi.single (M := E) i y),
      x⟫_A =
    ⟪y, x i⟫_A

Tactic:
simp only [pi_inner, equiv_symm_pi_apply]

Premises used: WithCStarModule.pi_inner, WithCStarModule.equiv_symm_pi_apply
-- 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 : ⟪Pi.single (M := E) i y i, x i⟫_A = ⟪y, x i⟫_A
h₀ : ∀ (b : ι), Membership.mem (γ := Finset ι) Finset.univ b → b ≠ i → ⟪Pi.single (M := E) i y b, x b⟫_A = 0
h₁ : i ∉ Finset.univ → ⟪Pi.single (M := E) i y i, x i⟫_A = 0
⊢ ∑ x_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_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
⊢ ⟪Pi.single (M := E) i y i, x i⟫_A = ⟪y, x i⟫_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 → ⟪Pi.single (M := E) i y b, x 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 → ⟪Pi.single (M := E) i y i, x 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 ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
simp : ∑ x_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A
⊢ ⟪x,
      (Equiv.symm (equiv A ((i : ι) → E i)) : (a : (i : ι) → E i) → C⋆ᵐᵒᵈ(A, (i : ι) → E i))
        (Pi.single (M := E) i y)⟫_A =
    ⟪x i, y⟫_A

Tactic:
simp only [pi_inner, equiv_symm_pi_apply]

Premises used: WithCStarModule.pi_inner, WithCStarModule.equiv_symm_pi_apply