awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(completion (f.leftMulMapPreGNS (x + x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
h :
  Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (x + x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h₁ : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))) :
    (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
c : Completion f.PreGNS
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
have h : IsClosed.{u_1} (X := Completion f.PreGNS)
  {a : Completion f.PreGNS |
    Eq (α := Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
        Completion f.PreGNS)
      ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
            (a : Completion f.PreGNS) → Completion f.PreGNS)
          a :
        Completion f.PreGNS)}
Tactic: induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp [add_mul, Completion.coe_add]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
c : Completion f.PreGNS
h :
  IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
have h₁ : ∀ (c : f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x + x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑c : Completion f.PreGNS) :
      Completion f.PreGNS)
    ((HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑c : Completion f.PreGNS) :
      Completion f.PreGNS)
Tactic: induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp [add_mul, Completion.coe_add]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ completion (f.leftMulMapPreGNS (x * x_1)) =
    HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))
have h : ∀ (c : Completion f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
Tactic: ext c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(completion (f.leftMulMapPreGNS (x * x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
h :
  Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (x * x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
⊢ IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
have h₁ : Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
  (⇑(HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))) :
    (a : Completion f.PreGNS) → Completion f.PreGNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
c : Completion f.PreGNS
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
have h : IsClosed.{u_1} (X := Completion f.PreGNS)
  {a : Completion f.PreGNS |
    Eq (α := Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
        Completion f.PreGNS)
      ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
            (a : Completion f.PreGNS) → Completion f.PreGNS)
          a :
        Completion f.PreGNS)}
Tactic: induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
c : Completion f.PreGNS
h :
  IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS) c :
      Completion f.PreGNS)
    ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        c :
      Completion f.PreGNS)
have h₁ : ∀ (c : f.PreGNS),
  Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (x * x_1)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑c : Completion f.PreGNS) :
      Completion f.PreGNS)
    ((HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑c : Completion f.PreGNS) :
      Completion f.PreGNS)
Tactic: induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
⊢ Eq (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS (star a))) (star (completion (f.leftMulMapPreGNS a)))
have refine : ∀ (x y : Completion f.PreGNS),
  ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x, y⟫_ℂ =
    ⟪x, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) y⟫_ℂ
Tactic: refine (eq_adjoint_iff (f.leftMulMapPreGNS (star a)).completion
      (f.leftMulMapPreGNS a).completion).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
⊢ IsClosed.{u_1} (X := Completion f.PreGNS × Completion f.PreGNS)
    {x : Completion f.PreGNS × Completion f.PreGNS |
      ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.1, x.2⟫_ℂ =
        ⟪x.1, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.2⟫_ℂ}
have hp : Continuous (Y := ℂ) fun (y : Completion f.PreGNS × Completion f.PreGNS) ↦
  ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) y.1, y.2⟫_ℂ
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
hp :
  Continuous (Y := ℂ) fun (y : Completion f.PreGNS × Completion f.PreGNS) ↦
    ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) y.1, y.2⟫_ℂ
⊢ IsClosed.{u_1} (X := Completion f.PreGNS × Completion f.PreGNS)
    {x : Completion f.PreGNS × Completion f.PreGNS |
      ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.1, x.2⟫_ℂ =
        ⟪x.1, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.2⟫_ℂ}
have hp₁ : Continuous (Y := ℂ) fun (y : Completion f.PreGNS × Completion f.PreGNS) ↦
  ⟪y.1, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) y.2⟫_ℂ
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x y : Completion f.PreGNS
⊢ ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x, y⟫_ℂ =
    ⟪x, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) y⟫_ℂ
have hp : IsClosed.{u_1} (X := Completion f.PreGNS × Completion f.PreGNS)
  {x : Completion f.PreGNS × Completion f.PreGNS |
    ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.1, x.2⟫_ℂ =
      ⟪x.1, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.2⟫_ℂ}
Tactic: induction x, y using induction_on₂ with
    | hp => apply isClosed_eq <;> fun_prop
    | ih x y => simp [mul_assoc, preGNS_inner_def]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
x y : Completion f.PreGNS
hp :
  IsClosed.{u_1} (X := Completion f.PreGNS × Completion f.PreGNS)
    {x : Completion f.PreGNS × Completion f.PreGNS |
      ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.1, x.2⟫_ℂ =
        ⟪x.1, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) x.2⟫_ℂ}
⊢ ⟪(completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS) x, y⟫_ℂ =
    ⟪x, (completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) y⟫_ℂ
have ih : ∀ (x y : f.PreGNS),
  inner ℂ (E := Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS (star a)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
          (↑x : Completion f.PreGNS) :
        Completion f.PreGNS)
      ((↑y : Completion f.PreGNS) : Completion f.PreGNS) =
    inner ℂ (E := Completion f.PreGNS) (↑x : Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS a) : (a : Completion f.PreGNS) → Completion f.PreGNS) (↑y : Completion f.PreGNS))
Tactic: induction x, y using induction_on₂ with
    | hp => apply isClosed_eq <;> fun_prop
    | ih x y => simp [mul_assoc, preGNS_inner_def]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ Eq.{u_2 + 1} (α := f.GNS (A := A) →L[ℂ] f.GNS (A := A)) ((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1) 1
have h : ∀ (b : f.GNS (A := A)),
  Eq (α := f.GNS (A := A))
    (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
    ((1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
Tactic: ext b
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ IsClosed.{u_2} (X := Completion (f.PreGNS (A := A)))
    {a : Completion (f.PreGNS (A := A)) |
      Eq (α := f.GNS (A := A))
        (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))
        ((1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))}
have h : Continuous.{u_2, u_2} (X := Completion (f.PreGNS (A := A))) (Y := f.GNS (A := A))
  (⇑((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1) : (a : f.GNS) → f.GNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
h :
  Continuous.{u_2, u_2} (X := Completion (f.PreGNS (A := A))) (Y := f.GNS (A := A))
    (⇑((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1) : (a : f.GNS) → f.GNS)
⊢ IsClosed.{u_2} (X := Completion (f.PreGNS (A := A)))
    {a : Completion (f.PreGNS (A := A)) |
      Eq (α := f.GNS (A := A))
        (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))
        ((1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))}
have h₁ : Continuous.{u_2, u_2} (X := Completion (f.PreGNS (A := A))) (Y := f.GNS (A := A)) (⇑1 : (a : f.GNS) → f.GNS)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
b : f.GNS (A := A)
⊢ Eq (α := f.GNS (A := A))
    (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
    ((1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
have h : IsClosed.{u_2} (X := Completion (f.PreGNS (A := A)))
  {a : Completion (f.PreGNS (A := A)) |
    Eq (α := f.GNS (A := A))
      (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))
      ((1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))}
Tactic: induction b using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih b => simp [gnsNonUnitalStarAlgHom]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
b : f.GNS (A := A)
h :
  IsClosed.{u_2} (X := Completion (f.PreGNS (A := A)))
    {a : Completion (f.PreGNS (A := A)) |
      Eq (α := f.GNS (A := A))
        (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))
        ((1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))}
⊢ Eq (α := f.GNS (A := A))
    (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
    ((1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
have h₁ : ∀ (b : f.PreGNS (A := A)),
  Eq (α := f.GNS (A := A))
    (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) (↑b : Completion f.PreGNS) :
      f.GNS (A := A))
    ((1 : (a : f.GNS) → f.GNS) (↑b : Completion f.PreGNS) : f.GNS (A := A))
Tactic: induction b using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih b => simp [gnsNonUnitalStarAlgHom]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
have a : ∀ (x : ℝ),
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
      x →
    0 ≤ x
Tactic: apply Multiset.single_le_sum
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
a :
  ∀ (x : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ)) x →
      0 ≤ x
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
have a₁ : Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
  (HPow.hPow (β := ℕ) ‖U i j‖ 2)
Tactic: apply Multiset.single_le_sum
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
h_x :
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
    x
⊢ 0 ≤ x
have h_x₁ : ∃ (a : n), Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
Tactic: rw [Multiset.mem_map] at h_x
Cleared hypotheses: h_x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
h_x : ∃ (a : n), Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
⊢ 0 ≤ x
have a : ∀ (a : n) (h_a : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x), 0 ≤ x
Tactic: obtain ⟨a, h_a⟩ := h_x
Cleared hypotheses: h_x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
a : n
h_a : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
⊢ 0 ≤ x
have a₁ : 0 ≤ HPow.hPow (β := ℕ) ‖U i a‖ 2
Tactic: rw [← h_a.2]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
    (HPow.hPow (β := ℕ) ‖U i j‖ 2)
have a : ∃ (a : n),
  Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧
    HPow.hPow (β := ℕ) ‖U i a‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2
Tactic: rw [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ ∃ (a : n),
    Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧
      HPow.hPow (β := ℕ) ‖U i a‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2
have h : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) j ∧
  HPow.hPow (β := ℕ) ‖U i j‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2
Tactic: use j
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ ‖U i j‖ ≤ 1
have norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
Tactic: have norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2 := by
    apply Multiset.single_le_sum
    · intro x h_x
      rw [Multiset.mem_map] at h_x
      obtain ⟨a, h_a⟩ := h_x
      rw [← h_a.2]
      apply sq_nonneg
    · rw [Multiset.mem_map]
      use j
      simp only [Finset.mem_univ_val, and_self_iff]