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
a : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A) (-(a.toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x (-(a.toProd.1 : (a : A) → A) y : A)

Tactic:
simp only [neg_mul, mul_neg, central]

Premises used: DoubleCentralizer.central, neg_mul, mul_neg
-- 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 b : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A) ((a.toProd.2 - b.toProd.2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 - b.toProd.1 : (a : A) → A) y : A)

Tactic:
simp only [ContinuousLinearMap.sub_apply, _root_.sub_mul, _root_.mul_sub, central]

Premises used: mul_sub, DoubleCentralizer.central, ContinuousLinearMap.sub_apply, sub_mul
-- 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
S : Type u_3
inst_5 : Monoid S
inst_6 : DistribMulAction S A
inst_7 : SMulCommClass 𝕜 S A
inst_8 : ContinuousConstSMul S A
inst_9 : IsScalarTower S A A
inst_10 : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A) ((s • a.toProd.2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((s • a.toProd.1 : (a : A) → A) y : A)

Tactic:
simp only [ContinuousLinearMap.smul_apply, mul_smul_comm, smul_mul_assoc, central]

Premises used: ContinuousLinearMap.smul_apply, DoubleCentralizer.central, smul_mul_assoc, mul_smul_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
S : Type u_3
inst_5 : Monoid S
inst_6 : DistribMulAction S A
inst_7 : SMulCommClass 𝕜 S A
inst_8 : ContinuousConstSMul S A
inst_9 : IsScalarTower S A A
inst_10 : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
⊢ (s • a).toProd = s • a.toProd

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
S : Type u_3
inst_5 : Monoid S
inst_6 : DistribMulAction S A
inst_7 : SMulCommClass 𝕜 S A
inst_8 : ContinuousConstSMul S A
inst_9 : IsScalarTower S A A
inst_10 : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
⊢ (s • a).toProd.1 = s • a.toProd.1

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
S : Type u_3
inst_5 : Monoid S
inst_6 : DistribMulAction S A
inst_7 : SMulCommClass 𝕜 S A
inst_8 : ContinuousConstSMul S A
inst_9 : IsScalarTower S A A
inst_10 : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
⊢ (s • a).toProd.2 = s • a.toProd.2

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 b : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A) ((b.toProd.2 : (a : A) → A) ((a.toProd.2 : (a : A) → A) x : A) : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 : (a : A) → A) ((b.toProd.1 : (a : A) → A) y : A) : A)

Tactic:
simp only [central]

Premises used: DoubleCentralizer.central
-- 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
n : ℕ
x y : A
rw :
  HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)
⊢ HMul.hMul (α := A) (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).1 : (a : A) → A) y : A)

Tactic:
rw [Prod.snd_natCast, Prod.fst_natCast]

Premises used: Prod.fst_natCast, Prod.snd_natCast
-- 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
n : ℕ
x y : A
⊢ HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)

Tactic:
simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]

Premises used: ContinuousLinearMap.smul_apply, smul_mul_assoc, ContinuousLinearMap.one_apply, mul_smul_comm, Nat.smul_one_eq_cast
-- 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
n : ℤ
x y : A
rw :
  HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)
⊢ HMul.hMul (α := A) (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : (A →L[𝕜] A) × (A →L[𝕜] A)).1 : (a : A) → A) y : A)

Tactic:
rw [Prod.snd_intCast, Prod.fst_intCast]

Premises used: Prod.fst_intCast, Prod.snd_intCast
-- 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
n : ℤ
x y : A
⊢ HMul.hMul (α := A) (((↑n : A →L[𝕜] A) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((↑n : A →L[𝕜] A) : (a : A) → A) y : A)

Tactic:
simp only [← Int.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]

Premises used: Int.smul_one_eq_cast, ContinuousLinearMap.smul_apply, smul_mul_assoc, ContinuousLinearMap.one_apply, mul_smul_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
a : 𝓜(𝕜, A)
x y : A
⊢ HMul.hMul (α := A) (((HPow.hPow (β := ℕ) a.toProd 0).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((HPow.hPow (β := ℕ) a.toProd 0).1 : (a : A) → A) y : A)

Tactic:
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)
k : ℕ
hk :
  ∀ (x y : A),
    HMul.hMul (α := A) (((a.toProd ^ k).2 : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x (((a.toProd ^ k).1 : (a : A) → A) y : A)
x y : A
succ :
  ∀
    (hk :
      ∀ (x y : A),
        HMul.hMul (α := A) ((a.toProd.2 ^ k : (a : A) → A) x : A) y =
          HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) y : A))
    (x y : A),
    HMul.hMul (α := A) ((a.toProd.2 ^ (k + 1) : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
⊢ HMul.hMul (α := A) (((a.toProd ^ (k + 1)).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((a.toProd ^ (k + 1)).1 : (a : A) → A) y : A)

Tactic:
rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢

Premises used: Prod.pow_snd, Prod.pow_fst
-- 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)
k : ℕ
hk :
  ∀ (x y : A),
    HMul.hMul (α := A) ((a.toProd.2 ^ k : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) y : A)
x y : A
succ :
  HMul.hMul (α := A) ((a.toProd.2 * a.toProd.2 ^ k : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
succ₁ :
  HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) ((a.toProd.2 ^ k : (a : A) → A) x : A) : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
succ₂ :
  HMul.hMul (α := A) (β := A) ((a.toProd.2 ^ k : (a : A) → A) x : A) ((a.toProd.1 : (a : A) → A) y : A) =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
succ₃ :
  HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) ((a.toProd.1 : (a : A) → A) y : A) : A) =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)
succ₄ :
  HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) ((a.toProd.1 : (a : A) → A) y : A) : A) =
    HMul.hMul (β := A) x ((a.toProd.1 ^ k * a.toProd.1 : (a : A) → A) y : A)
succ₅ succ₆ :
  HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) ((a.toProd.1 : (a : A) → A) y : A) : A) =
    HMul.hMul (β := A) x ((a.toProd.1 ^ k : (a : A) → A) ((a.toProd.1 : (a : A) → A) y : A) : A)
⊢ HMul.hMul (α := A) ((a.toProd.2 ^ (k + 1) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((a.toProd.1 ^ (k + 1) : (a : A) → A) y : A)

Tactic:
rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]

Premises used: ContinuousLinearMap.mul_apply, pow_succ, DoubleCentralizer.central, Prod.fst, Prod.snd, pow_succ', DoubleCentralizer.toProd
-- 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)
n : ℕ
x y : A
zero :
  ∀ (x y : A),
    HMul.hMul (α := A) (((HPow.hPow (β := ℕ) a.toProd 0).2 : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x (((HPow.hPow (β := ℕ) a.toProd 0).1 : (a : A) → A) y : A)
succ :
  ∀ (k : ℕ)
    (hk :
      ∀ (x y : A),
        HMul.hMul (α := A) (((a.toProd ^ k).2 : (a : A) → A) x : A) y =
          HMul.hMul (β := A) x (((a.toProd ^ k).1 : (a : A) → A) y : A))
    (x y : A),
    HMul.hMul (α := A) (((a.toProd ^ (k + 1)).2 : (a : A) → A) x : A) y =
      HMul.hMul (β := A) x (((a.toProd ^ (k + 1)).1 : (a : A) → A) y : A)
⊢ HMul.hMul (α := A) (((a.toProd ^ n).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x (((a.toProd ^ n).1 : (a : A) → A) y : A)

Tactic:
induction n generalizing x y with
      | zero => rfl
      | succ k hk =>
        rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
        rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]

Premises used: ContinuousLinearMap.mul_apply, pow_succ, DoubleCentralizer.central, ContinuousLinearMap.zero, Prod.fst, Prod.pow_snd, Prod.snd, Prod.pow_fst, pow_succ', DoubleCentralizer.toProd
-- 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 b : 𝓜(𝕜, A)
⊢ (a + b).toProd = a.toProd + b.toProd

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
⊢ Eq.{u_2 + 1} (α := (A →L[𝕜] A) × (A →L[𝕜] A)) (toProd 0) 0

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).toProd = -a.toProd

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 b : 𝓜(𝕜, A)
⊢ (a - b).toProd = a.toProd - b.toProd

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
⊢ Eq.{u_2 + 1} (α := (A →L[𝕜] A) × (A →L[𝕜] A)) (toProd 1) 1

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
n : ℕ
⊢ Eq.{u_2 + 1} (α := (A →L[𝕜] A) × (A →L[𝕜] A)) (toProd (↑n : 𝓜(𝕜, A))) (↑n : (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
n : ℤ
⊢ Eq.{u_2 + 1} (α := (A →L[𝕜] A) × (A →L[𝕜] A)) (toProd (↑n : 𝓜(𝕜, A))) (↑n : (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
n : ℕ
a : 𝓜(𝕜, A)
⊢ (a ^ n).toProd = a.toProd ^ n

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 b : 𝓜(𝕜, A)
⊢ (a + b).toProd.1 = a.toProd.1 + b.toProd.1

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 b : 𝓜(𝕜, A)
⊢ (a + b).toProd.2 = a.toProd.2 + b.toProd.2

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
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd 0).1 0

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
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd 0).2 0

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).toProd.1 = -a.toProd.1

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).toProd.2 = -a.toProd.2

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 b : 𝓜(𝕜, A)
⊢ (a - b).toProd.1 = a.toProd.1 - b.toProd.1

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 b : 𝓜(𝕜, A)
⊢ (a - b).toProd.2 = a.toProd.2 - b.toProd.2

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
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd 1).1 1

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
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd 1).2 1

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 b : 𝓜(𝕜, A)
⊢ (a * b).toProd.1 = a.toProd.1 * b.toProd.1

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 b : 𝓜(𝕜, A)
⊢ (a * b).toProd.2 = b.toProd.2 * a.toProd.2

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
n : ℕ
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd (↑n : 𝓜(𝕜, A))).1 (↑n : 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
n : ℕ
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd (↑n : 𝓜(𝕜, A))).2 (↑n : 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
n : ℤ
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd (↑n : 𝓜(𝕜, A))).1 (↑n : 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
n : ℤ
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd (↑n : 𝓜(𝕜, A))).2 (↑n : 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
n : ℕ
a : 𝓜(𝕜, A)
⊢ (a ^ n).toProd.1 = a.toProd.1 ^ n

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
n : ℕ
a : 𝓜(𝕜, A)
⊢ (a ^ n).toProd.2 = a.toProd.2 ^ n

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
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := 𝓜(𝕜, A)) toProdMulOpposite

Tactic:
fun _a _b h =>
    let h' := Prod.ext_iff.mp h
    ext (𝕜 := 𝕜) (A := A) _ _ <| Prod.ext h'.1 <| MulOpposite.op_injective h'.2

Premises used: MulOpposite.op_injective, Prod.ext_iff, And.right, And.left, Prod.ext, Iff.mp, DoubleCentralizer.ext, Function.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)
⊢ Membership.mem (γ := Set ((A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ))
    {lr : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ |
      ∀ (x y : A),
        HMul.hMul (α := A) ((unop lr.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((lr.1 : (a : A) → A) y : A)}
    a.toProdMulOpposite

Tactic:
a.central

Premises used: Set.Mem, DoubleCentralizer.central, setOf
-- 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)
⊢ Membership.mem (γ := Set ((A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ))
    {lr : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ |
      ∀ (x y : A),
        HMul.hMul (α := A) ((unop lr.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((lr.1 : (a : A) → A) y : A)}
    a.toProdMulOpposite

Tactic:
exact a.central

Premises used: DoubleCentralizer.central
-- 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
k : 𝕜
x y : A
simp_rw :
  HMul.hMul (α := A) ((((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) k : A →L[𝕜] A) : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) k : A →L[𝕜] A) : (a : A) → A) y : A)
simp_rw₁ :
  HMul.hMul (α := A) ((HSMul.hSMul (β := A →L[𝕜] A) k 1 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x ((HSMul.hSMul (β := A →L[𝕜] A) k 1 : (a : A) → A) y : A)
simp_rw₂ : HSMul.hSMul (β := A) k ((1 : (a : A) → A) x : A) * y = x * HSMul.hSMul (β := A) k ((1 : (a : A) → A) y : A)
simp_rw₃ : k • x * y = x * k • y
simp_rw₄ : k • x * y = k • (x * y)
⊢ HMul.hMul (α := A)
      ((((algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A)) : (a : 𝕜) → (A →L[𝕜] A) × (A →L[𝕜] A)) k).2 : (a : A) → A) x : A) y =
    HMul.hMul (β := A) x
      ((((algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A)) : (a : 𝕜) → (A →L[𝕜] A) × (A →L[𝕜] A)) k).1 : (a : A) → A) y : A)

Tactic:
simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
            mul_smul_comm, smul_mul_assoc]

Premises used: ContinuousLinearMap.smul_apply, smul_mul_assoc, ContinuousLinearMap.one_apply, Algebra.algebraMap_eq_smul_one, Prod.algebraMap_apply, mul_smul_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
k : 𝕜
⊢ Eq.{u_2 + 1} (α := (A →L[𝕜] A) × (A →L[𝕜] A)) (toProd ((algebraMap 𝕜 𝓜(𝕜, A) : (a : 𝕜) → 𝓜(𝕜, A)) k))
    ((algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A)) : (a : 𝕜) → (A →L[𝕜] A) × (A →L[𝕜] A)) k)

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
k : 𝕜
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd ((algebraMap 𝕜 𝓜(𝕜, A) : (a : 𝕜) → 𝓜(𝕜, A)) k)).1
    ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) k)

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
k : 𝕜
⊢ Eq.{u_2 + 1} (α := A →L[𝕜] A) (toProd ((algebraMap 𝕜 𝓜(𝕜, A) : (a : 𝕜) → 𝓜(𝕜, A)) k)).2
    ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) k)

Tactic:
rfl

Premises used: rfl