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 : E ⊗[𝕜] F
⊢ x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y

Tactic:
simpa only [← inner_conj_symm x, ← inner_conj_symm y, starRingEnd_apply, star_inj] using
    TensorProduct.ext_iff_inner_right (x := x) (y := y)

Premises used: TensorProduct.ext_iff_inner_right, starRingEnd_apply, star_inj, inner_conj_symm
-- 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 = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) = inner 𝕜 y (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c)

Tactic:
⟨fun h _ _ _ ↦ h ▸ rfl, fun h ↦ innerSL_inj.mp (ContinuousLinearMap.coe_inj.mp (ext_threefold h))⟩

Premises used: ContinuousLinearMap.coe_inj, innerSL_inj, Eq.rec, Iff.intro, Iff.mp, TensorProduct.ext_threefold, 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 y : E ⊗[𝕜] F ⊗[𝕜] G
⊢ x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) x = inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) y

Tactic:
simpa only [← inner_conj_symm x, ← inner_conj_symm y, starRingEnd_apply, star_inj] using
    ext_iff_inner_right_threefold (x := x) (y := y)

Premises used: starRingEnd_apply, star_inj, inner_conj_symm, TensorProduct.ext_iff_inner_right_threefold
-- 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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x : E ⊗[𝕜] F
⊢ Eq (α := G ⊗[𝕜] H) ((mapIsometry f g : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H)
    ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H)

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
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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
⊢ (mapIsometry f g).toLinearMap = map f.toLinearMap g.toLinearMap

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- 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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x : E ⊗[𝕜] F
⊢ norm (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H) = ‖x‖

Tactic:
mapIsometry f g |>.norm_map x

Premises used: LinearIsometry.norm_map, TensorProduct.mapIsometry
-- 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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x : E ⊗[𝕜] F
⊢ nnnorm (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H) = ‖x‖₊

Tactic:
mapIsometry f g |>.nnnorm_map x

Premises used: TensorProduct.mapIsometry, LinearIsometry.nnnorm_map
-- 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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x : E ⊗[𝕜] F
⊢ enorm (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H) = ‖x‖ₑ

Tactic:
mapIsometry f g |>.enorm_map x

Premises used: TensorProduct.mapIsometry, LinearIsometry.enorm_map
-- 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
h :
  ∀ (x : E ⊗[𝕜] F),
    Eq (α := E ⊗[𝕜] F) ((mapIsometry LinearIsometry.id LinearIsometry.id : (a : E ⊗[𝕜] F) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
      ((LinearIsometry.id : (a : E ⊗[𝕜] F) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
⊢ Eq (α := E ⊗[𝕜] F →ₗᵢ[𝕜] E ⊗[𝕜] F) (mapIsometry LinearIsometry.id LinearIsometry.id) LinearIsometry.id

Tactic:
ext
-- 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 (α := E ⊗[𝕜] F) ((mapIsometry LinearIsometry.id LinearIsometry.id : (a : E ⊗[𝕜] F) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
    ((LinearIsometry.id : (a : E ⊗[𝕜] F) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)

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
f : F →ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] F →ₗᵢ[𝕜] E ⊗[𝕜] G) (LinearIsometry.lTensor E f) (mapIsometry LinearIsometry.id f)

Tactic:
rfl

Premises used: LinearIsometry.lTensor, 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
f : E →ₗᵢ[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G →ₗᵢ[𝕜] F ⊗[𝕜] G) (LinearIsometry.rTensor G f) (mapIsometry f LinearIsometry.id)

Tactic:
rfl

Premises used: LinearIsometry.rTensor, 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
f : F →ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] G) (LinearIsometry.toLinearMap (LinearIsometry.lTensor E f))
    (LinearMap.lTensor E f.toLinearMap)

Tactic:
rfl

Premises used: LinearMap.lTensor, TensorProduct.map, TensorProduct.lift, 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
f : E →ₗᵢ[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G →ₗ[𝕜] F ⊗[𝕜] G) (LinearIsometry.toLinearMap (LinearIsometry.rTensor G f))
    (LinearMap.rTensor G f.toLinearMap)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl, LinearMap.rTensor
-- 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
f : F →ₗᵢ[𝕜] G
x : E ⊗[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G) ((LinearIsometry.lTensor E f : (a : E ⊗[𝕜] F) → E ⊗[𝕜] G) x : E ⊗[𝕜] G)
    ((LinearMap.lTensor E f.toLinearMap : (a : E ⊗[𝕜] F) → E ⊗[𝕜] G) x : E ⊗[𝕜] 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
f : E →ₗᵢ[𝕜] F
x : E ⊗[𝕜] G
⊢ Eq (α := F ⊗[𝕜] G) ((LinearIsometry.rTensor G f : (a : E ⊗[𝕜] G) → F ⊗[𝕜] G) x : F ⊗[𝕜] G)
    ((LinearMap.rTensor G f.toLinearMap : (a : E ⊗[𝕜] G) → F ⊗[𝕜] G) x : 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
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
f : E ≃ₗᵢ[𝕜] G
g : F ≃ₗᵢ[𝕜] H
x : E ⊗[𝕜] F
⊢ Eq (α := G ⊗[𝕜] H) ((congrIsometry f g : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H)
    ((congr (↑(↑f : E ≃L[𝕜] G) : E ≃ₗ[𝕜] G) (↑(↑g : F ≃L[𝕜] H) : F ≃ₗ[𝕜] H) : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H)

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
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
f : E ≃ₗᵢ[𝕜] G
g : F ≃ₗᵢ[𝕜] H
⊢ (congrIsometry f g).symm = congrIsometry f.symm g.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.congr, LinearEquiv.isometryOfInner, TensorProduct.map, TensorProduct, TensorProduct.lift, rfl, TensorProduct.congrIsometry
-- 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
f : E ≃ₗᵢ[𝕜] G
g : F ≃ₗᵢ[𝕜] H
⊢ (congrIsometry f g).toLinearEquiv = congr f.toLinearEquiv g.toLinearEquiv

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.congr, 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
a :
  ∀ (x : E) (x_1 : F),
    Eq (α := E ⊗[𝕜] F)
      (((((AlgebraTensorModule.curry
                      (↑(LinearIsometryEquiv.toLinearEquiv
                            (congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F))) :
                        E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                    E →ₗ[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                  (a : E) → F →ₗ[𝕜] E ⊗[𝕜] F)
                x :
              F →ₗ[𝕜] E ⊗[𝕜] F) :
            (a : F) → E ⊗[𝕜] F)
          x_1 :
        E ⊗[𝕜] F)
      (((((AlgebraTensorModule.curry
                      (↑(LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl 𝕜 (E ⊗[𝕜] F))) :
                        E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                    E →ₗ[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                  (a : E) → F →ₗ[𝕜] E ⊗[𝕜] F)
                x :
              F →ₗ[𝕜] E ⊗[𝕜] F) :
            (a : F) → E ⊗[𝕜] F)
          x_1 :
        E ⊗[𝕜] F)
⊢ Eq (α := E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F)
    (↑(LinearIsometryEquiv.toLinearEquiv
          (congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F))) :
      E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F)
    (↑(LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl 𝕜 (E ⊗[𝕜] F))) : E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F)

Tactic:
ext
-- 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
x_1 : F
⊢ Eq (α := E ⊗[𝕜] F)
    (((((AlgebraTensorModule.curry
                    (↑(LinearIsometryEquiv.toLinearEquiv
                          (congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F))) :
                      E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                  E →ₗ[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                (a : E) → F →ₗ[𝕜] E ⊗[𝕜] F)
              x :
            F →ₗ[𝕜] E ⊗[𝕜] F) :
          (a : F) → E ⊗[𝕜] F)
        x_1 :
      E ⊗[𝕜] F)
    (((((AlgebraTensorModule.curry
                    (↑(LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl 𝕜 (E ⊗[𝕜] F))) :
                      E ⊗[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                  E →ₗ[𝕜] F →ₗ[𝕜] E ⊗[𝕜] F) :
                (a : E) → F →ₗ[𝕜] E ⊗[𝕜] F)
              x :
            F →ₗ[𝕜] E ⊗[𝕜] F) :
          (a : F) → E ⊗[𝕜] F)
        x_1 :
      E ⊗[𝕜] F)

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
f : F ≃ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] F ≃ₗᵢ[𝕜] E ⊗[𝕜] G) (LinearIsometryEquiv.lTensor E f) (congrIsometry (LinearIsometryEquiv.refl 𝕜 E) f)

Tactic:
rfl

Premises used: LinearIsometryEquiv.lTensor, 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
f : E ≃ₗᵢ[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G ≃ₗᵢ[𝕜] F ⊗[𝕜] G) (LinearIsometryEquiv.rTensor G f) (congrIsometry f (LinearIsometryEquiv.refl 𝕜 G))

Tactic:
rfl

Premises used: LinearIsometryEquiv.rTensor, 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
f : F ≃ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] G ≃ₗᵢ[𝕜] E ⊗[𝕜] F) (LinearIsometryEquiv.symm (LinearIsometryEquiv.lTensor E f))
    (LinearIsometryEquiv.lTensor E f.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.congr, LinearEquiv.isometryOfInner, TensorProduct.map, LinearIsometryEquiv.lTensor, TensorProduct, TensorProduct.lift, rfl, TensorProduct.congrIsometry
-- 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
f : E ≃ₗᵢ[𝕜] F
⊢ Eq (α := F ⊗[𝕜] G ≃ₗᵢ[𝕜] E ⊗[𝕜] G) (LinearIsometryEquiv.symm (LinearIsometryEquiv.rTensor G f))
    (LinearIsometryEquiv.rTensor G f.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.congr, LinearEquiv.isometryOfInner, TensorProduct.map, TensorProduct, LinearIsometryEquiv.rTensor, TensorProduct.lift, rfl, TensorProduct.congrIsometry
-- 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
f : F ≃ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] F ≃ₗ[𝕜] E ⊗[𝕜] G) (LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.lTensor E f))
    (LinearEquiv.lTensor E f.toLinearEquiv)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.congr, LinearEquiv.lTensor, 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
f : F ≃ₗᵢ[𝕜] G
⊢ Eq (α := E ⊗[𝕜] F →ₗᵢ[𝕜] E ⊗[𝕜] G) (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.lTensor E f))
    (LinearIsometry.lTensor E f.toLinearIsometry)

Tactic:
rfl

Premises used: LinearIsometryEquiv.toLinearIsometry, TensorProduct.mapIsometry, LinearIsometry.lTensor, TensorProduct.map, LinearMap.isometryOfInner, TensorProduct.lift, 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
f : E ≃ₗᵢ[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G ≃ₗ[𝕜] F ⊗[𝕜] G) (LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.rTensor G f))
    (LinearEquiv.rTensor G f.toLinearEquiv)

Tactic:
rfl

Premises used: LinearEquiv.rTensor, LinearEquiv.ofLinear, TensorProduct.congr, 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
f : E ≃ₗᵢ[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G →ₗᵢ[𝕜] F ⊗[𝕜] G) (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.rTensor G f))
    (LinearIsometry.rTensor G f.toLinearIsometry)

Tactic:
rfl

Premises used: LinearIsometryEquiv.toLinearIsometry, TensorProduct.mapIsometry, TensorProduct.map, LinearMap.isometryOfInner, LinearIsometry.rTensor, TensorProduct.lift, 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
f : F ≃ₗᵢ[𝕜] G
x : E ⊗[𝕜] F
⊢ Eq (α := E ⊗[𝕜] G) ((LinearIsometryEquiv.lTensor E f : (a : E ⊗[𝕜] F) → E ⊗[𝕜] G) x : E ⊗[𝕜] G)
    ((LinearEquiv.lTensor E f.toLinearEquiv : (a : E ⊗[𝕜] F) → E ⊗[𝕜] G) x : E ⊗[𝕜] 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
f : E ≃ₗᵢ[𝕜] F
x : E ⊗[𝕜] G
⊢ Eq (α := F ⊗[𝕜] G) ((LinearIsometryEquiv.rTensor G f : (a : E ⊗[𝕜] G) → F ⊗[𝕜] G) x : F ⊗[𝕜] G)
    ((LinearEquiv.rTensor G f.toLinearEquiv : (a : E ⊗[𝕜] G) → F ⊗[𝕜] G) x : F ⊗[𝕜] G)

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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
x : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
⊢ Eq (α := E ⊗[𝕜] F) ((mapInclIsometry E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
    ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) x : E ⊗[𝕜] F)

Tactic:
rfl

Premises used: Set.Mem, 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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
⊢ (mapInclIsometry E' F').toLinearMap = mapIncl E' F'

Tactic:
rfl

Premises used: Set.Mem, TensorProduct.map, 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
x y : E ⊗[𝕜] F
⊢ inner 𝕜 (E := F ⊗[𝕜] E) ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) 0 : F ⊗[𝕜] E)
      ((TensorProduct.comm 𝕜 E F : (a : E ⊗[𝕜] F) → F ⊗[𝕜] E) y : F ⊗[𝕜] E) =
    inner 𝕜 0 y

Tactic:
simp
-- 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 : E ⊗[𝕜] F
x_1 : E
x_2 : F
⊢ 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) 0 : F ⊗[𝕜] E) =
    inner 𝕜 (E := E ⊗[𝕜] F) (x_1 ⊗ₜ[𝕜] x_2) 0

Tactic:
simp
-- 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 : E ⊗[𝕜] F
x_1 : E
x_2 : F
⊢ ∀ (x : E) (y : F),
    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) (x ⊗ₜ[𝕜] y) : F ⊗[𝕜] E) =
      inner 𝕜 (E := E ⊗[𝕜] F) (x_1 ⊗ₜ[𝕜] x_2) (x ⊗ₜ[𝕜] y)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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 : E ⊗[𝕜] F
x_1 : E
x_2 : F
x_3 x_4 : E ⊗[𝕜] F
h1 :
  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) x_3 : F ⊗[𝕜] E) =
    inner 𝕜 (x_1 ⊗ₜ[𝕜] x_2) x_3
h2 :
  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) x_4 : F ⊗[𝕜] E) =
    inner 𝕜 (x_1 ⊗ₜ[𝕜] x_2) x_4
⊢ 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) (x_3 + x_4) : F ⊗[𝕜] 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