awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ Eq (α := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0 : E × F)
have a : Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
  ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
a :
  Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1
⊢ Eq (α := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0 : E × F)
have a₁ : Eq.{u_3 + 1} (α := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
  ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1
have a : inner.{u_1, u_2} A (E := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1 ≤
  0
Tactic: refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ Eq.{u_3 + 1} (α := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).2
have a : inner.{u_1, u_3} A (E := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2 ≤
  0
Tactic: refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
⊢ max ‖x.1‖ ‖x.2‖ ≤ √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have simp : ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
Tactic: simp only [norm_eq_sqrt_norm_inner_self (A := A) (E := E),
    norm_eq_sqrt_norm_inner_self (A := A) (E := F), max_le_iff, norm_nonneg,
    Real.sqrt_le_sqrt_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have left : ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
left : ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have right : ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have left : 0 ≤ ⟪x.1, x.1⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
left : 0 ≤ ⟪x.1, x.1⟫_A
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have left₁ : ⟪x.1, x.1⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have right : 0 ≤ ⟪x.2, x.2⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
right : 0 ≤ ⟪x.2, x.2⟫_A
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
have right₁ : ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
have apply : ‖x.1‖ + ‖x.2‖ ≤
  (↑2 : ℝ) *
    Norm.norm (E := E × F)
      (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
Tactic: apply prod_norm_le_norm_add x |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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‖ + ‖x.2‖ ≤
    (↑2 : ℝ) *
      Norm.norm (E := E × F)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
have simp : ‖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: simp only [NNReal.coe_ofNat, linearEquiv_apply, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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‖ + ‖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)
have h₁ : ‖x.1‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
⊢ ‖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)
have h₂ : ‖x.2‖ ≤ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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‖ ≤ ∑ i : ι, ‖x i‖
have refine : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) (∑ i : ι, ‖x i‖) 2
Tactic: refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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 ≤ HPow.hPow (α := ℝ) (β := ℕ) (∑ i : ι, ‖x i‖) 2
have calc : Eq (α := ℝ) (∑ i : ι, ‖⟪x i, x i⟫_A‖) (∑ i : ι, HPow.hPow (β := ℕ) ‖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 _)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
⊢ Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0 ↔ x = 0
have refine : ∀ (h : Eq.{u_1 + 1} (α := A) (∑ i : ι, ⟪x i, x i⟫_A) 0), x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ x = 0
have h₁ : ∀ (i : ι), x i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
have h₁ : ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A
Tactic: refine inner_self.mp <| le_antisymm (le_of_le_of_eq ?_ h) inner_self_nonneg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ ⟪(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
have simp : ∑ x_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_A
Tactic: simp only [pi_inner, equiv_symm_pi_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_A
have rw : ⟪Pi.single (M := E) i y i, x i⟫_A = ⟪y, x i⟫_A
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ ∑ x_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_A
have h₀ : ∀ (b : ι), Membership.mem (γ := Finset ι) Finset.univ b → b ≠ i → ⟪Pi.single (M := E) i y b, x b⟫_A = 0
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ ∑ x_1 : ι, ⟪Pi.single (M := E) i y x_1, x x_1⟫_A = ⟪y, x i⟫_A
have h₁ : i ∉ Finset.univ → ⟪Pi.single (M := E) i y i, x i⟫_A = 0
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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,
      (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
have simp : ∑ x_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A
Tactic: simp only [pi_inner, equiv_symm_pi_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A
have rw : ⟪x i, Pi.single (M := E) i y i⟫_A = ⟪x i, y⟫_A
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ ∑ x_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A
have h₀ : ∀ (b : ι), Membership.mem (γ := Finset ι) Finset.univ b → b ≠ i → ⟪x b, Pi.single (M := E) i y b⟫_A = 0
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ ∑ x_1 : ι, ⟪x x_1, Pi.single (M := E) i y x_1⟫_A = ⟪x i, y⟫_A
have h₁ : i ∉ Finset.univ → ⟪x i, Pi.single (M := E) i y i⟫_A = 0
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ 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‖
have 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
Tactic: rw [← sq_eq_sq₀ (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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‖
have refine : HPow.hPow (β := ℕ) ‖x i‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x i‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have rw : ‖⟪x i, x i⟫_A‖ ≤ Norm.norm.{u_1} (E := A) (∑ i : ι, ⟪x i, x i⟫_A)
Tactic: rw [pi_norm_sq, norm_sq_eq A]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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)
have refine : ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
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
⊢ 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‖
have 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‖
Tactic: rw [pi_norm_le_iff_of_nonneg (by positivity)]