awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y x_1 x_2 : E ⊗[𝕜] F
h1 :
  inner 𝕜 (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x_1 : F ⊗[𝕜] E)
      ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) y : F ⊗[𝕜] E) =
    inner 𝕜 x_1 y
h2 :
  inner 𝕜 (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x_2 : F ⊗[𝕜] E)
      ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) y : F ⊗[𝕜] E) =
    inner 𝕜 x_2 y
⊢ inner 𝕜 (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) (x_1 + x_2) : F ⊗[𝕜] E)
      ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) y : F ⊗[𝕜] E) =
    inner 𝕜 (x_1 + x_2) y

Tactic:
simp only [inner_add_left, map_add, h1, h2]

Premises used: map_add, inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
⊢ Eq (α := F ⊗[𝕜] E) ((commIsometry 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x : F ⊗[𝕜] E)
    ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x : F ⊗[𝕜] E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
⊢ Eq (α := F ⊗[𝕜] E ≃ₗᵢ[𝕜] E ⊗[𝕜] F) (LinearIsometryEquiv.symm (commIsometry 𝕜 E F)) (commIsometry 𝕜 F E)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, LinearEquiv.isometryOfInner, TensorProduct.commIsometry, TensorProduct, TensorProduct.lift, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
⊢ Eq (α := E ⊗[𝕜] F ≃ₗ[𝕜] F ⊗[𝕜] E) (LinearIsometryEquiv.toLinearEquiv (commIsometry 𝕜 E F)) (TensorProduct.comm 𝕜 E F)

Tactic:
rfl

Premises used: TensorProduct.comm, LinearEquiv.ofLinear, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
⊢ norm (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x : F ⊗[𝕜] E) = ‖x‖

Tactic:
commIsometry 𝕜 E F |>.norm_map x

Premises used: LinearIsometryEquiv.norm_map, TensorProduct.commIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
⊢ nnnorm (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x : F ⊗[𝕜] E) = ‖x‖₊

Tactic:
commIsometry 𝕜 E F |>.nnnorm_map x

Premises used: LinearIsometryEquiv.nnnorm_map, TensorProduct.commIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
⊢ enorm (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) x : F ⊗[𝕜] E) = ‖x‖ₑ

Tactic:
commIsometry 𝕜 E F |>.toLinearIsometry.enorm_map x

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.enorm_map, TensorProduct.commIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) 0 : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) y : E) =
    inner 𝕜 0 y

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x_1 : 𝕜
x_2 : E
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 ⊗ₜ[𝕜] x_2) : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) 0 : E) =
    inner 𝕜 (E := 𝕜 ⊗[𝕜] E) (x_1 ⊗ₜ[𝕜] x_2) 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x_1 : 𝕜
x_2 : E
⊢ ∀ (x : 𝕜) (y : E),
    inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 ⊗ₜ[𝕜] x_2) : E)
        ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x ⊗ₜ[𝕜] y) : E) =
      inner 𝕜 (E := 𝕜 ⊗[𝕜] E) (x_1 ⊗ₜ[𝕜] x_2) (x ⊗ₜ[𝕜] y)

Tactic:
simp [inner_smul_left, inner_smul_right, mul_assoc]

Premises used: mul_assoc, inner_smul_right, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x_1 : 𝕜
x_2 : E
x_3 x_4 : 𝕜 ⊗[𝕜] E
h1 :
  inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 ⊗ₜ[𝕜] x_2) : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x_3 : E) =
    inner 𝕜 (x_1 ⊗ₜ[𝕜] x_2) x_3
h2 :
  inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 ⊗ₜ[𝕜] x_2) : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x_4 : E) =
    inner 𝕜 (x_1 ⊗ₜ[𝕜] x_2) x_4
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 ⊗ₜ[𝕜] x_2) : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_3 + x_4) : E) =
    inner 𝕜 (x_1 ⊗ₜ[𝕜] x_2) (x_3 + x_4)

Tactic:
simp only [inner_add_right, map_add, h1, h2]

Premises used: map_add, inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y x_1 x_2 : 𝕜 ⊗[𝕜] E
h1 :
  inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x_1 : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) y : E) =
    inner 𝕜 x_1 y
h2 :
  inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x_2 : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) y : E) =
    inner 𝕜 x_2 y
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) (x_1 + x_2) : E)
      ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) y : E) =
    inner 𝕜 (x_1 + x_2) y

Tactic:
simp only [inner_add_left, map_add, h1, h2]

Premises used: map_add, inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : 𝕜 ⊗[𝕜] E
⊢ Eq.{u_2 + 1} (α := E) ((lidIsometry 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x : E)
    ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Eq (α := 𝕜 ⊗[𝕜] E) ((LinearIsometryEquiv.symm (lidIsometry 𝕜 E) : (a : E) → 𝕜 ⊗[𝕜] E) x : 𝕜 ⊗[𝕜] E)
    (1 ⊗ₜ[𝕜] x : 𝕜 ⊗[𝕜] E)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq (α := 𝕜 ⊗[𝕜] E ≃ₗ[𝕜] E) (LinearIsometryEquiv.toLinearEquiv (E := 𝕜 ⊗[𝕜] E) (lidIsometry 𝕜 E))
    (TensorProduct.lid 𝕜 E)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.lid, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : 𝕜 ⊗[𝕜] E
⊢ norm.{u_2} (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x : E) = ‖x‖

Tactic:
lidIsometry 𝕜 E |>.norm_map x

Premises used: LinearIsometryEquiv.norm_map, TensorProduct.lidIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : 𝕜 ⊗[𝕜] E
⊢ nnnorm.{u_2} (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x : E) = ‖x‖₊

Tactic:
lidIsometry 𝕜 E |>.nnnorm_map x

Premises used: LinearIsometryEquiv.nnnorm_map, TensorProduct.lidIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : 𝕜 ⊗[𝕜] E
⊢ enorm.{u_2} (E := E) ((TensorProduct.lid 𝕜 E : (a : 𝕜 ⊗[𝕜] E) → E) x : E) = ‖x‖ₑ

Tactic:
lidIsometry 𝕜 E |>.toLinearIsometry.enorm_map x

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.enorm_map, TensorProduct.lidIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) 0 : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) y : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 0 y

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (a ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) 0 : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (a ⊗ₜ[𝕜] x_1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
c : E ⊗[𝕜] F
x_2 : G
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (0 ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (c ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (0 ⊗ₜ[𝕜] x_1) (c ⊗ₜ[𝕜] x_2)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
c : E ⊗[𝕜] F
x_2 : G
x_3 : E
x_4 : F
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) :
        E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (0 ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) (0 ⊗ₜ[𝕜] x_2)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
c : E ⊗[𝕜] F
x_2 : G
x_3 : E
x_4 : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
        ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) :
          E ⊗[𝕜] (F ⊗[𝕜] G))
        ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x_2) :
          E ⊗[𝕜] (F ⊗[𝕜] G)) =
      inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x_2)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
c : E ⊗[𝕜] F
x_2 : G
x_3 : E
x_4 : F
x_5 x_6 : E ⊗[𝕜] F
h1 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) :
        E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_5 ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) (x_5 ⊗ₜ[𝕜] x_2)
h2 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) :
        E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_6 ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) (x_6 ⊗ₜ[𝕜] x_2)
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) :
        E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) ((x_5 + x_6) ⊗ₜ[𝕜] x_2) :
        E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_4 ⊗ₜ[𝕜] x_1) ((x_5 + x_6) ⊗ₜ[𝕜] x_2)

Tactic:
simp only [add_tmul, inner_add_right, map_add, h1, h2]

Premises used: map_add, inner_add_right, TensorProduct.add_tmul
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
c : E ⊗[𝕜] F
x_2 : G
x_3 x_4 : E ⊗[𝕜] F
h1 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_3 ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (c ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_3 ⊗ₜ[𝕜] x_1) (c ⊗ₜ[𝕜] x_2)
h2 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_4 ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (c ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) (x_4 ⊗ₜ[𝕜] x_1) (c ⊗ₜ[𝕜] x_2)
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) ((x_3 + x_4) ⊗ₜ[𝕜] x_1) :
        E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (c ⊗ₜ[𝕜] x_2) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (E := E ⊗[𝕜] F ⊗[𝕜] G) ((x_3 + x_4) ⊗ₜ[𝕜] x_1) (c ⊗ₜ[𝕜] x_2)

Tactic:
simp only [add_tmul, inner_add_left, map_add, h1, h2]

Premises used: map_add, inner_add_left, TensorProduct.add_tmul
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x_1 : G
x_2 x_3 : E ⊗[𝕜] F ⊗[𝕜] G
h1 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (a ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x_2 : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (a ⊗ₜ[𝕜] x_1) x_2
h2 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (a ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x_3 : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (a ⊗ₜ[𝕜] x_1) x_3
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (a ⊗ₜ[𝕜] x_1) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_2 + x_3) : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (a ⊗ₜ[𝕜] x_1) (x_2 + x_3)

Tactic:
simp only [inner_add_right, map_add, h1, h2]

Premises used: map_add, inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
x_1 x_2 : E ⊗[𝕜] F ⊗[𝕜] G
h1 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x_1 : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) y : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 x_1 y
h2 :
  inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x_2 : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) y : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 x_2 y
⊢ inner 𝕜 (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) (x_1 + x_2) : E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) y : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    inner 𝕜 (x_1 + x_2) y

Tactic:
simp only [inner_add_left, map_add, h1, h2]

Premises used: map_add, inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E ⊗[𝕜] F ⊗[𝕜] G
⊢ Eq (α := E ⊗[𝕜] (F ⊗[𝕜] G))
    ((assocIsometry 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x : E ⊗[𝕜] (F ⊗[𝕜] G))
    ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x : E ⊗[𝕜] (F ⊗[𝕜] G))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E ⊗[𝕜] (F ⊗[𝕜] G)
⊢ Eq (α := E ⊗[𝕜] F ⊗[𝕜] G)
    ((LinearIsometryEquiv.symm (assocIsometry 𝕜 E F G) : (a : E ⊗[𝕜] (F ⊗[𝕜] G)) → E ⊗[𝕜] F ⊗[𝕜] G) x : E ⊗[𝕜] F ⊗[𝕜] G)
    ((LinearEquiv.symm (TensorProduct.assoc 𝕜 E F G) : (a : E ⊗[𝕜] (F ⊗[𝕜] G)) → E ⊗[𝕜] F ⊗[𝕜] G) x : E ⊗[𝕜] F ⊗[𝕜] G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
⊢ Eq (α := E ⊗[𝕜] F ⊗[𝕜] G ≃ₗ[𝕜] E ⊗[𝕜] (F ⊗[𝕜] G)) (LinearIsometryEquiv.toLinearEquiv (assocIsometry 𝕜 E F G))
    (TensorProduct.assoc 𝕜 E F G)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.assoc, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E ⊗[𝕜] F ⊗[𝕜] G
⊢ norm (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    ‖x‖

Tactic:
assocIsometry 𝕜 E F G |>.norm_map x

Premises used: LinearIsometryEquiv.norm_map, TensorProduct.assocIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E ⊗[𝕜] F ⊗[𝕜] G
⊢ nnnorm (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    ‖x‖₊

Tactic:
assocIsometry 𝕜 E F G |>.nnnorm_map x

Premises used: LinearIsometryEquiv.nnnorm_map, TensorProduct.assocIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E ⊗[𝕜] F ⊗[𝕜] G
⊢ enorm (E := E ⊗[𝕜] (F ⊗[𝕜] G))
      ((TensorProduct.assoc 𝕜 E F G : (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G)) x : E ⊗[𝕜] (F ⊗[𝕜] G)) =
    ‖x‖ₑ

Tactic:
assocIsometry 𝕜 E F G |>.toLinearIsometry.enorm_map x

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.enorm_map, TensorProduct.assocIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
inst_11 : FiniteDimensional 𝕜 G
inst_12 : FiniteDimensional 𝕜 H
f : E →ₗ[𝕜] F
g : G →ₗ[𝕜] H
x : F
x_1 : H
⊢ Eq (α := E ⊗[𝕜] G)
    ((((LinearMap.adjoint : (a : E ⊗[𝕜] G →ₗ[𝕜] F ⊗[𝕜] H) → F ⊗[𝕜] H →ₗ[𝕜] E ⊗[𝕜] G) (map f g) :
            F ⊗[𝕜] H →ₗ[𝕜] E ⊗[𝕜] G) :
          (a : F ⊗[𝕜] H) → E ⊗[𝕜] G)
        (x ⊗ₜ[𝕜] x_1) :
      E ⊗[𝕜] G)
    ((map ((LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) f) ((LinearMap.adjoint : (a : G →ₗ[𝕜] H) → H →ₗ[𝕜] G) g) :
          (a : F ⊗[𝕜] H) → E ⊗[𝕜] G)
        (x ⊗ₜ[𝕜] x_1) :
      E ⊗[𝕜] G)

Tactic:
simp [TensorProduct.ext_iff_inner_right, LinearMap.adjoint_inner_left]

Premises used: TensorProduct.ext_iff_inner_right, LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
inst_7 : FiniteDimensional 𝕜 E
inst_8 : FiniteDimensional 𝕜 F
inst_9 : FiniteDimensional 𝕜 G
f : E →ₗ[𝕜] F
⊢ Eq (α := F ⊗[𝕜] G →ₗ[𝕜] E ⊗[𝕜] G)
    ((adjoint : (a : E ⊗[𝕜] G →ₗ[𝕜] F ⊗[𝕜] G) → F ⊗[𝕜] G →ₗ[𝕜] E ⊗[𝕜] G) (rTensor G f) : F ⊗[𝕜] G →ₗ[𝕜] E ⊗[𝕜] G)
    (rTensor G ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) f) : F ⊗[𝕜] G →ₗ[𝕜] E ⊗[𝕜] G)

Tactic:
simp [rTensor]

Premises used: LinearMap.rTensor