awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
h :
  Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (m • x))) : (a : Completion f.PreGNS) → Completion f.PreGNS)
h₁ :
  Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x))) :
      (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 (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}

Tactic:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
⊢ Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (m • x))) : (a : Completion f.PreGNS) → Completion f.PreGNS)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
⊢ Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x))) :
      (a : Completion f.PreGNS) → Completion f.PreGNS)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
a : f.PreGNS
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑a : Completion f.PreGNS) :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        (↑a : Completion f.PreGNS) :
      Completion f.PreGNS)

Tactic:
simp [smul_mul_assoc]

Premises used: smul_mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
m : ℂ
x : A
a : Completion f.PreGNS
h :
  IsClosed.{u_1} (X := Completion f.PreGNS)
    {a : Completion f.PreGNS |
      Eq (α := Completion f.PreGNS)
        ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
          Completion f.PreGNS)
        ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
              (a : Completion f.PreGNS) → Completion f.PreGNS)
            a :
          Completion f.PreGNS)}
h₁ :
  ∀ (a : f.PreGNS),
    Eq (α := Completion f.PreGNS)
      ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS)
          (↑a : Completion f.PreGNS) :
        Completion f.PreGNS)
      ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
            (a : Completion f.PreGNS) → Completion f.PreGNS)
          (↑a : Completion f.PreGNS) :
        Completion f.PreGNS)
⊢ Eq (α := Completion f.PreGNS)
    ((completion (f.leftMulMapPreGNS (m • x)) : (a : Completion f.PreGNS) → Completion f.PreGNS) a :
      Completion f.PreGNS)
    ((HSMul.hSMul (β := Completion f.PreGNS →L[ℂ] Completion f.PreGNS) m (completion (f.leftMulMapPreGNS x)) :
          (a : Completion f.PreGNS) → Completion f.PreGNS)
        a :
      Completion f.PreGNS)

Tactic:
induction a using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih a => simp [smul_mul_assoc]

Premises used: smul_mul_assoc, isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
⊢ ∀ (m : ℂ) (x : A),
    completion (f.leftMulMapPreGNS (m • x)) =
      HSMul.hSMul (α := ℂ) (β := f.GNS →L[ℂ] f.GNS) ((MonoidHom.id ℂ : (a : ℂ) → ℂ) m : ℂ)
        (completion (f.leftMulMapPreGNS x))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
⊢ Eq (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS 0)) 0

Tactic:
simpa using f.completion_leftMulMapPreGNS_map_smul 0 0

Premises used: _private.0.PositiveLinearMap.completion_leftMulMapPreGNS_map_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
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)
      ((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.leftMulMapPreGNS (x + x_1)) =
    HAdd.hAdd (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))

Tactic:
ext c
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)
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)
⊢ 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:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (x + x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
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:
simp [add_mul, Completion.coe_add]

Premises used: add_mul, UniformSpace.Completion.coe_add
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)}
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)
⊢ 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)

Tactic:
induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp [add_mul, Completion.coe_add]

Premises used: add_mul, isClosed_eq, UniformSpace.Completion.coe_add
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
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)
⊢ completion (f.leftMulMapPreGNS (x * x_1)) =
    HMul.hMul (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS x)) (completion (f.leftMulMapPreGNS x_1))

Tactic:
ext c
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)
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)
⊢ 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:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ Continuous (X := Completion f.PreGNS) (Y := Completion f.PreGNS)
    (⇑(completion (f.leftMulMapPreGNS (x * x_1))) : (a : Completion f.PreGNS) → Completion f.PreGNS)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 : A
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)}
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)
⊢ 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:
induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)))

Tactic:
(eq_adjoint_iff (f.leftMulMapPreGNS (star a)).completion
      (f.leftMulMapPreGNS a).completion).mpr ?_

Premises used: Iff.mpr, ContinuousLinearMap.eq_adjoint_iff, ContinuousLinearMap.completion, PositiveLinearMap.leftMulMapPreGNS, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
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⟫_ℂ
⊢ Eq (α := f.GNS →L[ℂ] f.GNS) (completion (f.leftMulMapPreGNS (star a))) (star (completion (f.leftMulMapPreGNS a)))

Tactic:
refine (eq_adjoint_iff (f.leftMulMapPreGNS (star a)).completion
      (f.leftMulMapPreGNS a).completion).mpr ?_

Premises used: Iff.mpr, ContinuousLinearMap.eq_adjoint_iff, ContinuousLinearMap.completion, PositiveLinearMap.leftMulMapPreGNS, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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⟫_ℂ
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⟫_ℂ
⊢ 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:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
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:
simp [mul_assoc, preGNS_inner_def]

Premises used: mul_assoc, PositiveLinearMap.preGNS_inner_def
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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⟫_ℂ}
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))
⊢ ⟪(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:
induction x, y using induction_on₂ with
    | hp => apply isClosed_eq <;> fun_prop
    | ih x y => simp [mul_assoc, preGNS_inner_def]

Premises used: mul_assoc, PositiveLinearMap.preGNS_inner_def, isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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) ((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) a : f.GNS →L[ℂ] f.GNS)
    (completion (f.leftMulMapPreGNS a) : Completion f.PreGNS →L[ℂ] Completion f.PreGNS)

Tactic:
rfl

Premises used: ContinuousLinearMap.completion, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
a : A
b : f.PreGNS
⊢ Eq (α := f.GNS)
    ((((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) a : f.GNS →L[ℂ] f.GNS) : (a : f.GNS) → f.GNS)
        (↑b : Completion f.PreGNS) :
      f.GNS)
    ((↑((f.leftMulMapPreGNS a : (a : f.PreGNS) → f.PreGNS) b) : Completion f.PreGNS) : Completion f.PreGNS)

Tactic:
simp [gnsNonUnitalStarAlgHom_apply]

Premises used: PositiveLinearMap.gnsNonUnitalStarAlgHom_apply
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
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))
⊢ Eq.{u_2 + 1} (α := f.GNS (A := A) →L[ℂ] f.GNS (A := A)) ((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1) 1

Tactic:
ext b
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
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)
h₁ : Continuous.{u_2, u_2} (X := Completion (f.PreGNS (A := A))) (Y := f.GNS (A := A)) (⇑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))}

Tactic:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ 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:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ Continuous.{u_2, u_2} (X := Completion (f.PreGNS (A := A))) (Y := f.GNS (A := A)) (⇑1 : (a : f.GNS) → f.GNS)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
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:
simp [gnsNonUnitalStarAlgHom]

Premises used: PositiveLinearMap.gnsNonUnitalStarAlgHom