awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ 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)
have 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)
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]
Cleared hypotheses: n, x, y
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
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]
Cleared hypotheses: n, x, y
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
            mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
            mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have simp_rw₂ : HSMul.hSMul (β := A) k ((1 : (a : A) → A) x : A) * y = x * HSMul.hSMul (β := 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have simp_rw₃ : k • x * y = x * k • y
Tactic: simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
            mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ 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)
have simp_rw₄ : k • x * y = k • (x * y)
Tactic: simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
            mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (star x) = x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (star x) = x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x + x_1) = star x + star x_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x + x_1) = star x + star x_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x * x_1) = star x_1 * star x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x * x_1) = star x_1 * star x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x • x_1) = star x • star x_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ star (x • x_1) = star x • star x_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ 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 : 𝕜) → 𝓜(𝕜, 𝕜))
have 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
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ 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 : 𝕜) → 𝓜(𝕜, 𝕜))
have 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
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
have 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 : 𝕜)
Tactic: refine ContinuousLinearMap.ext fun y => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ CompleteSpace.{u_2} 𝓜(𝕜, A)
have rw : IsComplete.{u_2} (α := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
Tactic: rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.isUniformInducing]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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
⊢ IsComplete.{u_2} (α := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
have h : IsClosed.{u_2} (X := (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) (Set.range (ι := 𝓜(𝕜, A)) toProdMulOpposite)
Tactic: apply IsClosed.isComplete