awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
a : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A)
      ((((↑(↑(starₗᵢ 𝕜) : A ≃L⋆[𝕜] A) : A →L⋆[𝕜] A) ∘SL a.toProd.1) ∘SL (↑(↑(starₗᵢ 𝕜) : A ≃L⋆[𝕜] A) : A →L⋆[𝕜] A) :
            (a : A) → A)
          x :
        A)
      y =
    HMul.hMul (β := A) x
      ((((↑(↑(starₗᵢ 𝕜) : A ≃L⋆[𝕜] A) : A →L⋆[𝕜] A) ∘SL a.toProd.2) ∘SL (↑(↑(starₗᵢ 𝕜) : A ≃L⋆[𝕜] A) : A →L⋆[𝕜] A) :
            (a : A) → A)
          y :
        A)

Tactic:
simpa only [star_mul, star_star] using (congr_arg star (a.central (star y) (star x))).symm

Premises used: star_star, DoubleCentralizer.central, congr_arg, StarMul.star_mul, Eq.symm, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
a : 𝓜(𝕜, A)
b : A
⊢ Eq (α := A) (((star a).toProd.1 : (a : A) → A) b : A) (star ((a.toProd.2 : (a : A) → A) (star b)) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
a : 𝓜(𝕜, A)
b : A
⊢ Eq (α := A) (((star a).toProd.2 : (a : A) → A) b : A) (star ((a.toProd.1 : (a : A) → A) (star b)) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝓜(𝕜, A)
h : ∀ (x_1 : A), Eq (α := A) (((star (star x)).toProd.1 : (a : A) → A) x_1 : A) ((x.toProd.1 : (a : A) → A) x_1 : A)
h₁ : ∀ (x_1 : A), Eq (α := A) (((star (star x)).toProd.2 : (a : A) → A) x_1 : A) ((x.toProd.2 : (a : A) → A) x_1 : A)
⊢ star (star x) = x

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝓜(𝕜, A)
x_1 : A
⊢ Eq (α := A) (((star (star x)).toProd.1 : (a : A) → A) x_1 : A) ((x.toProd.1 : (a : A) → A) x_1 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝓜(𝕜, A)
x_1 : A
⊢ Eq (α := A) (((star (star x)).toProd.2 : (a : A) → A) x_1 : A) ((x.toProd.2 : (a : A) → A) x_1 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
h :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x + x_1)).toProd.1 : (a : A) → A) x_2 : A)
      (((star x + star x_1).toProd.1 : (a : A) → A) x_2 : A)
h₁ :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x + x_1)).toProd.2 : (a : A) → A) x_2 : A)
      (((star x + star x_1).toProd.2 : (a : A) → A) x_2 : A)
⊢ star (x + x_1) = star x + star x_1

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x + x_1)).toProd.1 : (a : A) → A) x_2 : A) (((star x + star x_1).toProd.1 : (a : A) → A) x_2 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x + x_1)).toProd.2 : (a : A) → A) x_2 : A) (((star x + star x_1).toProd.2 : (a : A) → A) x_2 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
h :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x * x_1)).toProd.1 : (a : A) → A) x_2 : A)
      (((star x_1 * star x).toProd.1 : (a : A) → A) x_2 : A)
h₁ :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x * x_1)).toProd.2 : (a : A) → A) x_2 : A)
      (((star x_1 * star x).toProd.2 : (a : A) → A) x_2 : A)
⊢ star (x * x_1) = star x_1 * star x

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x * x_1)).toProd.1 : (a : A) → A) x_2 : A) (((star x_1 * star x).toProd.1 : (a : A) → A) x_2 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x * x_1)).toProd.2 : (a : A) → A) x_2 : A) (((star x_1 * star x).toProd.2 : (a : A) → A) x_2 : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝕜
x_1 : 𝓜(𝕜, A)
h :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x • x_1)).toProd.1 : (a : A) → A) x_2 : A)
      (((star x • star x_1).toProd.1 : (a : A) → A) x_2 : A)
h₁ :
  ∀ (x_2 : A),
    Eq (α := A) (((star (x • x_1)).toProd.2 : (a : A) → A) x_2 : A)
      (((star x • star x_1).toProd.2 : (a : A) → A) x_2 : A)
⊢ star (x • x_1) = star x • star x_1

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝕜
x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x • x_1)).toProd.1 : (a : A) → A) x_2 : A) (((star x • star x_1).toProd.1 : (a : A) → A) x_2 : A)

Tactic:
star_smul _ _

Premises used: StarModule.star_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝕜
x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x • x_1)).toProd.1 : (a : A) → A) x_2 : A) (((star x • star x_1).toProd.1 : (a : A) → A) x_2 : A)

Tactic:
exact star_smul _ _

Premises used: StarModule.star_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝕜
x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x • x_1)).toProd.2 : (a : A) → A) x_2 : A) (((star x • star x_1).toProd.2 : (a : A) → A) x_2 : A)

Tactic:
star_smul _ _

Premises used: StarModule.star_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing 𝕜
inst_6 : StarRing A
inst_7 : StarModule 𝕜 A
inst_8 : NormedStarGroup A
x : 𝕜
x_1 : 𝓜(𝕜, A)
x_2 : A
⊢ Eq (α := A) (((star (x • x_1)).toProd.2 : (a : A) → A) x_2 : A) (((star x • star x_1).toProd.2 : (a : A) → A) x_2 : A)

Tactic:
exact star_smul _ _

Premises used: StarModule.star_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : A
⊢ Eq (α := A →L[𝕜] A)
    (toProd
        ((↑𝕜 :
            {A : Type u_2} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_5 : NonUnitalNormedRing A] →
                  [inst_6 : NormedSpace 𝕜 A] →
                    [inst_7 : SMulCommClass 𝕜 A A] → [inst_8 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
          a)).1
    ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : A
⊢ Eq (α := A →L[𝕜] A)
    (toProd
        ((↑𝕜 :
            {A : Type u_2} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_5 : NonUnitalNormedRing A] →
                  [inst_6 : NormedSpace 𝕜 A] →
                    [inst_7 : SMulCommClass 𝕜 A A] → [inst_8 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
          a)).2
    ((ContinuousLinearMap.flip (mul 𝕜 A) : (a : A) → A →L[𝕜] A) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h :
  ∀ (x : 𝕜),
    Eq (α := 𝕜 →L[𝕜] 𝕜)
      (toProd
          ((↑𝕜 :
              {A : Type u_1} →
                [inst : NontriviallyNormedField 𝕜] →
                  [inst_1 : NonUnitalNormedRing A] →
                    [inst_2 : NormedSpace 𝕜 A] →
                      [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
            x)).1
      (toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).1
h₁ :
  ∀ (x : 𝕜),
    Eq (α := 𝕜 →L[𝕜] 𝕜)
      (toProd
          ((↑𝕜 :
              {A : Type u_1} →
                [inst : NontriviallyNormedField 𝕜] →
                  [inst_1 : NonUnitalNormedRing A] →
                    [inst_2 : NormedSpace 𝕜 A] →
                      [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
            x)).2
      (toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2
⊢ Eq (α := (a : 𝕜) → 𝓜(𝕜, 𝕜))
    (↑𝕜 :
      {A : Type u_1} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NonUnitalNormedRing A] →
            [inst_2 : NormedSpace 𝕜 A] →
              [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
    (⇑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) : (a : 𝕜) → 𝓜(𝕜, 𝕜))

Tactic:
ext x : 3
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜)
    (toProd
        ((↑𝕜 :
            {A : Type u_1} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NonUnitalNormedRing A] →
                  [inst_2 : NormedSpace 𝕜 A] →
                    [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
          x)).1
    (toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).1

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜)
    (toProd
        ((↑𝕜 :
            {A : Type u_1} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NonUnitalNormedRing A] →
                  [inst_2 : NormedSpace 𝕜 A] →
                    [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
          x)).2
    (toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2

Tactic:
ContinuousLinearMap.ext fun y => ?_

Premises used: ContinuousLinearMap.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
h :
  ∀ (y : 𝕜),
    Eq (α := 𝕜)
      (((toProd
                ((↑𝕜 :
                    {A : Type u_1} →
                      [inst : NontriviallyNormedField 𝕜] →
                        [inst_1 : NonUnitalNormedRing A] →
                          [inst_2 : NormedSpace 𝕜 A] →
                            [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
                  x)).2 :
            (a : 𝕜) → 𝕜)
          y :
        𝕜)
      (((toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2 : (a : 𝕜) → 𝕜) y : 𝕜)
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜)
    (toProd
        ((↑𝕜 :
            {A : Type u_1} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NonUnitalNormedRing A] →
                  [inst_2 : NormedSpace 𝕜 A] →
                    [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
          x)).2
    (toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2

Tactic:
refine ContinuousLinearMap.ext fun y => ?_

Premises used: ContinuousLinearMap.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x y : 𝕜
⊢ Eq (α := 𝕜)
    (((toProd
              ((↑𝕜 :
                  {A : Type u_1} →
                    [inst : NontriviallyNormedField 𝕜] →
                      [inst_1 : NonUnitalNormedRing A] →
                        [inst_2 : NormedSpace 𝕜 A] →
                          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
                x)).2 :
          (a : 𝕜) → 𝕜)
        y :
      𝕜)
    (((toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2 : (a : 𝕜) → 𝕜) y : 𝕜)

Tactic:
mul_comm y x

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x y : 𝕜
⊢ Eq (α := 𝕜)
    (((toProd
              ((↑𝕜 :
                  {A : Type u_1} →
                    [inst : NontriviallyNormedField 𝕜] →
                      [inst_1 : NonUnitalNormedRing A] →
                        [inst_2 : NormedSpace 𝕜 A] →
                          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → (a : A) → 𝓜(𝕜, A))
                x)).2 :
          (a : 𝕜) → 𝕜)
        y :
      𝕜)
    (((toProd ((algebraMap 𝕜 𝓜(𝕜, 𝕜) : (a : 𝕜) → 𝓜(𝕜, 𝕜)) x)).2 : (a : 𝕜) → 𝕜) y : 𝕜)

Tactic:
exact mul_comm y x

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := 𝓜(𝕜, A)) (β := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
    (⇑toProdMulOppositeHom : (a : 𝓜(𝕜, A)) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)

Tactic:
simpa using toProdMulOpposite_injective

Premises used: DoubleCentralizer.toProdMulOpposite_injective
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ ‖a‖ =
    norm (E := (A →L[𝕜] A) × (A →L[𝕜] A))
      ((toProdHom : (a : 𝓜(𝕜, A)) → (A →L[𝕜] A) × (A →L[𝕜] A)) a : (A →L[𝕜] A) × (A →L[𝕜] A))

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ ‖a‖₊ =
    nnnorm (E := (A →L[𝕜] A) × (A →L[𝕜] A))
      ((toProdHom : (a : 𝓜(𝕜, A)) → (A →L[𝕜] A) × (A →L[𝕜] A)) a : (A →L[𝕜] A) × (A →L[𝕜] A))

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ ‖a‖ =
    norm (E := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
      ((toProdMulOppositeHom : (a : 𝓜(𝕜, A)) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) a : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ ‖a‖₊ =
    nnnorm (E := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
      ((toProdMulOppositeHom : (a : 𝓜(𝕜, A)) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) a : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
⊢ IsUniformEmbedding.{u_2, u_2} (α := 𝓜(𝕜, A)) toProdMulOpposite

Tactic:
isUniformEmbedding_comap toProdMulOpposite_injective

Premises used: isUniformEmbedding_comap, Set.Mem, DoubleCentralizer.toProdMulOpposite_injective, setOf, DoubleCentralizer.toProdMulOpposite
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
rw : IsComplete.{u_2} (α := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
⊢ CompleteSpace.{u_2} 𝓜(𝕜, A)

Tactic:
rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.isUniformInducing]

Premises used: IsUniformEmbedding.isUniformInducing, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite, completeSpace_iff_isComplete_range
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
h : IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
⊢ IsComplete.{u_2} (α := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)

Tactic:
apply IsClosed.isComplete

Premises used: IsClosed.isComplete
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
h :
  IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
    (⋂ (i : A),
      ⋂ (i_1 : A),
        {x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ |
          HMul.hMul (α := A) ((unop x.2 : (a : A) → A) i : A) i_1 = HMul.hMul (β := A) i ((x.1 : (a : A) → A) i_1 : A)})
⊢ IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)

Tactic:
simp only [range_toProdMulOpposite, Set.setOf_forall]

Premises used: DoubleCentralizer.range_toProdMulOpposite, Set.setOf_forall
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
x y : A
⊢ Continuous (Y := A) fun (x_1 : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) ↦ HMul.hMul (α := A) ((unop x_1.2 : (a : A) → A) x : A) y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
x y : A
⊢ Continuous (Y := A) fun (x_1 : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) ↦ HMul.hMul (β := A) x ((x_1.1 : (a : A) → A) y : A)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : CompleteSpace A
⊢ IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
    (⋂ (i : A),
      ⋂ (i_1 : A),
        {x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ |
          HMul.hMul (α := A) ((unop x.2 : (a : A) → A) i : A) i_1 = HMul.hMul (β := A) i ((x.1 : (a : A) → A) i_1 : A)})

Tactic:
exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq (by fun_prop) (by fun_prop)

Premises used: isClosed_eq, isClosed_iInter
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
b : A
grw : C * (‖f‖₊ * ‖b‖₊) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
⊢ C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2

Tactic:
grw [f.le_opNNNorm b]

Premises used: ContinuousLinearMap.le_opNNNorm
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
b : A
ring_nf : C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2 ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2
⊢ C * (‖f‖₊ * ‖b‖₊) * ‖b‖₊ ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2

Tactic:
ring_nf
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : StarRing A
inst_6 : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h :
  ∀ (b : A),
    HPow.hPow (β := ℕ) (nnnorm (E := A) ((f : (a : A) → A) b : A)) 2 ≤
      C * nnnorm (E := A) ((f : (a : A) → A) b : A) * ‖b‖₊
b : A
⊢ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2 ≤ C * ‖f‖₊ * HPow.hPow (β := ℕ) ‖b‖₊ 2

Tactic:
rfl