awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
have h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2 := by
    calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left,
            ← add_assoc, norm_nonneg, Real.sq_sqrt]
          exact norm_add₃_le
      _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
      _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
      _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
          simp [norm_eq_sqrt_norm_inner_self (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
refine : 0 ≤ ‖x‖ + ‖y‖
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
refine (pow_le_pow_iff_left₀ (CStarModule.norm_nonneg A) ?_ (by simp)).mp h

Premises used: CStarModule.norm_nonneg, pow_le_pow_iff_left₀, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ 0 ≤ ‖x‖ + ‖y‖

Tactic:
add_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

Premises used: CStarModule.norm_nonneg, add_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ 0 ≤ ‖x‖ + ‖y‖

Tactic:
exact add_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

Premises used: CStarModule.norm_nonneg, add_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
c : ℂ
x : E
⊢ ‖c •> x‖ = ‖c‖ * ‖x‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self (A := A), norm_smul, ← mul_assoc]

Premises used: norm_smul, mul_assoc, CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

Tactic:
Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩

Premises used: Norm.norm, Inv.inv, And.intro, Exists.intro, HSMul.hSMul, Eq.symm, IsGreatest.csSup_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
refine_1 : ‖‖v‖⁻¹ •> v‖ ≤ 1
refine_2 : ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖
refine_3 : Membership.mem (γ := Set ℝ) (upperBounds {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}) ‖v‖
⊢ ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

Tactic:
refine Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩

Premises used: Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ 0 ≤ ‖v‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖‖v‖⁻¹ •> v‖ ≤ 1

Tactic:
simpa only [norm_smul, norm_inv, norm_norm] using inv_mul_le_one_of_le₀ le_rfl (by positivity)

Premises used: le_rfl, norm_smul, norm_norm, norm_inv, inv_mul_le_one_of_le₀
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖

Tactic:
simp [norm_smul, ← norm_sq_eq, pow_two, ← mul_assoc]

Premises used: pow_two, norm_smul, mul_assoc, CStarModule.norm_sq_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ ‖⟪w, v⟫_A‖ ≤ ‖w‖ * ‖v‖

Tactic:
norm_inner_le E

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
ha : 0 ≤ ‖v‖
⊢ ‖w‖ * ‖v‖ ≤ 1 * ‖v‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
⊢ 1 * ‖v‖ = ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
w : E
hw : ‖w‖ ≤ 1
calc : ‖w‖ * ‖v‖ ≤ 1 * ‖v‖
calc₁ : 1 * ‖v‖ = ‖v‖
⊢ ‖⟪w, v⟫_A‖ ≤ ‖v‖

Tactic:
calc _ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
      _ ≤ 1 * ‖v‖ := by gcongr
      _ = ‖v‖ := by simp

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : SMul A E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℂ E
inst_6 : CStarModule A E
x y : E
⊢ Norm.norm.{u_1} (E := A) ((((innerₛₗ : (a : E) → E →ₗ[ℂ] A) x : E →ₗ[ℂ] A) : (a : E) → A) y : A) ≤ 1 * ‖x‖ * ‖y‖

Tactic:
simp [innerₛₗ_apply, norm_inner_le E]

Premises used: CStarModule.innerₛₗ_apply, CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : SMul A E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℂ E
inst_6 : CStarModule A E
x y : E
⊢ (((innerSL : (a : E) → E →L[ℂ] A) x : E →L[ℂ] A) : (a : E) → A) y = ⟪x, y⟫_A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : SMul A E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℂ E
inst_6 : CStarModule A E
simp_rw :
  Continuous.{u_2, u_1} (Y := A) fun (x : E × E) ↦ (((innerSL : (a : E) → E →L[ℂ] A) x.1 : E →L[ℂ] A) : (a : E) → A) x.2
⊢ Continuous.{u_2, u_1} (Y := A) fun (x : E × E) ↦ ⟪x.1, x.2⟫_A

Tactic:
simp_rw [← innerSL_apply]

Premises used: CStarModule.innerSL_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : SMul A E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℂ E
inst_6 : CStarModule A E
⊢ Continuous.{u_2, u_1} (Y := A) fun (x : E × E) ↦ (((innerSL : (a : E) → E →L[ℂ] A) x.1 : E →L[ℂ] A) : (a : E) → A) x.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
inst : AddCommGroup E
⊢ Eq (α := E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) 0 : E) (0 : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
inst : AddCommGroup E
⊢ Eq (α := C⋆ᵐᵒᵈ(A, E)) (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) 0 : C⋆ᵐᵒᵈ(A, E)) (0 : C⋆ᵐᵒᵈ(A, E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x y : C⋆ᵐᵒᵈ(A, E)
inst : AddCommGroup E
⊢ (equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) (x + y) =
    HAdd.hAdd (α := E) (β := E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) x : E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) y : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x' y' : E
inst : AddCommGroup E
⊢ ((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) (x' + y') =
    HAdd.hAdd (α := C⋆ᵐᵒᵈ(A, E)) (β := C⋆ᵐᵒᵈ(A, E)) (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) x' : C⋆ᵐᵒᵈ(A, E))
      (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) y' : C⋆ᵐᵒᵈ(A, E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x y : C⋆ᵐᵒᵈ(A, E)
inst : AddCommGroup E
⊢ (equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) (x - y) =
    HSub.hSub (α := E) (β := E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) x : E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) y : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x' y' : E
inst : AddCommGroup E
⊢ ((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) (x' - y') =
    HSub.hSub (α := C⋆ᵐᵒᵈ(A, E)) (β := C⋆ᵐᵒᵈ(A, E)) (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) x' : C⋆ᵐᵒᵈ(A, E))
      (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) y' : C⋆ᵐᵒᵈ(A, E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x : C⋆ᵐᵒᵈ(A, E)
inst : AddCommGroup E
⊢ Eq (α := E) ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) (-x) : E) (-(equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
x' : E
inst : AddCommGroup E
⊢ Eq (α := C⋆ᵐᵒᵈ(A, E)) (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) (-x') : C⋆ᵐᵒᵈ(A, E))
    (-((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) x' : C⋆ᵐᵒᵈ(A, E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
A : Type u_3
E : Type u_4
inst : SMul R E
c : R
x : C⋆ᵐᵒᵈ(A, E)
⊢ (equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) (c • x) = HSMul.hSMul (β := E) c ((equiv A E : (a : C⋆ᵐᵒᵈ(A, E)) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
A : Type u_3
E : Type u_4
inst : SMul R E
c : R
x' : E
⊢ ((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) (c • x') =
    HSMul.hSMul (β := C⋆ᵐᵒᵈ(A, E)) c (((equiv A E).symm : (a : E) → C⋆ᵐᵒᵈ(A, E)) x' : C⋆ᵐᵒᵈ(A, E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_3
E : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : AddCommGroup E
inst_2 : Module R E
⊢ Eq (α := Submodule R C⋆ᵐᵒᵈ(A, E)) (Submodule.map (↑(LinearEquiv.symm (linearEquiv R A E)) : E →ₗ[R] C⋆ᵐᵒᵈ(A, E)) ⊤) ⊤

Tactic:
Submodule.map_eq_top_iff.mpr rfl

Premises used: Iff.mpr, Submodule.map_eq_top_iff, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
R' : Type u_2
A : Type u_3
E : Type u_4
inst : UniformSpace E
inst_1 : CompleteSpace E
⊢ CompleteSpace.{u_4} C⋆ᵐᵒᵈ(A, E)

Tactic:
uniformEquiv.completeSpace_iff.mpr inferInstance

Premises used: Iff.mpr, WithCStarModule.uniformEquiv, inferInstance, UniformEquiv.completeSpace_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
R' : Type u_2
A : Type u_3
E : Type u_4
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : ContinuousAdd E
⊢ ContinuousAdd.{u_4} C⋆ᵐᵒᵈ(A, E)

Tactic:
ContinuousAdd.induced (addEquiv A E)

Premises used: WithCStarModule.addEquiv, ContinuousAdd.induced
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
R' : Type u_2
A : Type u_3
E : Type u_4
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
⊢ IsUniformAddGroup.{u_4} C⋆ᵐᵒᵈ(A, E)

Tactic:
IsUniformAddGroup.comap (addEquiv A E)

Premises used: IsUniformAddGroup.comap, WithCStarModule.addEquiv
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
R' : Type u_2
A : Type u_3
E : Type u_4
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup E
inst_3 : UniformSpace E
inst_4 : Module R E
inst_5 : ContinuousSMul R E
⊢ ContinuousSMul.{u_1, u_4} R C⋆ᵐᵒᵈ(A, E)

Tactic:
ContinuousSMul.induced (linearEquiv R A E)

Premises used: WithCStarModule.linearEquiv, ContinuousSMul.induced
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ Eq.{u_3 + 1} (α := E) 0.1 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ Eq.{u_4 + 1} (α := F) 0.2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x y : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (x + y).1 = x.1 + y.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x y : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (x + y).2 = x.2 + y.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x y : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (x - y).1 = x.1 - y.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x y : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (x - y).2 = x.2 - y.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (-x).1 = -x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : C⋆ᵐᵒᵈ(A, E × F)
inst : AddCommGroup E
inst_1 : AddCommGroup F
⊢ (-x).2 = -x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
A : Type u_2
E : Type u_3
F : Type u_4
inst : SMul R E
inst_1 : SMul R F
x : C⋆ᵐᵒᵈ(A, E × F)
c : R
⊢ (c • x).1 = c • x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
A : Type u_2
E : Type u_3
F : Type u_4
inst : SMul R E
inst_1 : SMul R F
x : C⋆ᵐᵒᵈ(A, E × F)
c : R
⊢ (c • x).2 = c • x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1 = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2 = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : E × F
⊢ ((Equiv.symm (equiv A (E × F)) : (a : E × F) → C⋆ᵐᵒᵈ(A, E × F)) x).1 = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
E : Type u_3
F : Type u_4
x : E × F
⊢ ((Equiv.symm (equiv A (E × F)) : (a : E × F) → C⋆ᵐᵒᵈ(A, E × F)) x).2 = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_1
ι : Type u_2
E : ι → Type u_3
x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
h : ∀ (i : ι), x i = y i
⊢ x = y

Tactic:
funext h

Premises used: funext, WithCStarModule
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
i : ι
inst : (i : ι) → AddCommGroup (E i)
⊢ Eq.{u_4 + 1} (α := E i) (0 i) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
inst : (i : ι) → AddCommGroup (E i)
⊢ (x + y) i = x i + y i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
inst : (i : ι) → AddCommGroup (E i)
⊢ (x - y) i = x i - y i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
inst : (i : ι) → AddCommGroup (E i)
⊢ (-x) i = -x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
R : Type u_1
A : Type u_2
ι : Type u_3
E : ι → Type u_4
inst : (i : ι) → SMul.{u_1, u_4} R (E i)
c : R
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
⊢ (c • x) i = c • x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
⊢ (equiv A ((i : ι) → E i) : (a : C⋆ᵐᵒᵈ(A, (i : ι) → E i)) → (i : ι) → E i) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Synonym
Goal:
A : Type u_2
ι : Type u_3
E : ι → Type u_4
x : (i : ι) → E i
i : ι
⊢ (Equiv.symm (equiv A ((i : ι) → E i)) : (a : (i : ι) → E i) → C⋆ᵐᵒᵈ(A, (i : ι) → E i)) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u
A : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
h : a.toProd = b.toProd
mk :
  ∀ (toProd : (A →L[𝕜] A) × (A →L[𝕜] A))
    (central :
      ∀ (x y : A),
        HMul.hMul (α := A) ((toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd.1 : (a : A) → A) y : A))
    (h : DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } = b.toProd),
    { toProd := toProd, central := central } = b
⊢ a = b

Tactic:
cases a
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u
A : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd : (A →L[𝕜] A) × (A →L[𝕜] A)
central :
  ∀ (x y : A),
    HMul.hMul (α := A) ((toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd.1 : (a : A) → A) y : A)
h : DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } = b.toProd
mk :
  ∀ (toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A))
    (central_1 :
      ∀ (x y : A),
        HMul.hMul (α := A) ((toProd_1.2 : (a : A) → A) x : A) y =
          HMul.hMul (β := A) x ((toProd_1.1 : (a : A) → A) y : A))
    (h :
      DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } =
        DoubleCentralizer.toProd { toProd := toProd_1, central := central_1 }),
    Eq (α := 𝓜(𝕜, A)) { toProd := toProd, central := central } { toProd := toProd_1, central := central_1 }
⊢ { toProd := toProd, central := central } = b

Tactic:
cases b
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u
A : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : SMulCommClass 𝕜 A A
inst_4 : IsScalarTower 𝕜 A A
toProd : (A →L[𝕜] A) × (A →L[𝕜] A)
central :
  ∀ (x y : A),
    HMul.hMul (α := A) ((toProd.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd.1 : (a : A) → A) y : A)
toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A)
central_1 :
  ∀ (x y : A),
    HMul.hMul (α := A) ((toProd_1.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((toProd_1.1 : (a : A) → A) y : A)
h :
  DoubleCentralizer.toProd { toProd := toProd, central := central : 𝓜(𝕜, A) } =
    DoubleCentralizer.toProd { toProd := toProd_1, central := central_1 }
⊢ Eq (α := 𝓜(𝕜, A)) { toProd := toProd, central := central } { toProd := toProd_1, central := central_1 }

Tactic:
simpa using h
-- 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) ((lr.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((lr.1 : (a : A) → A) y : A)}
    a.toProd

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) ((lr.2 : (a : A) → A) x : A) y = HMul.hMul (β := A) x ((lr.1 : (a : A) → A) y : A)}
    a.toProd

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
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.add_apply, mul_add, add_mul, central]

Premises used: add_mul, DoubleCentralizer.central, ContinuousLinearMap.add_apply, mul_add