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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hx :
  inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
      ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) =
    0
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
⊢ ∀ (i : Fin (finrank.{u_1, u_2} 𝕜 ↥E')) (j : Fin (finrank.{u_1, u_3} 𝕜 ↥F')),
    Eq.{u_1 + 1} (α := 𝕜)
      (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                    TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                      Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                  (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                y :
              Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
            (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
          (i, j) :
        𝕜)
      (0 : 𝕜)

Tactic:
have (i) (j) : (e.toBasis.tensorProduct f.toBasis).repr y (i, j) = 0 := by
    rw [inner_mapIncl_mapIncl, inner_self y e f, RCLike.ofReal_eq_zero,
      Finset.sum_eq_zero_iff_of_nonneg fun _ _ => sq_nonneg _] at hx
    simpa using hx (i, j)
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hx :
  inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
      ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) =
    0
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
this :
  ∀ (i : Fin (finrank.{u_1, u_2} 𝕜 ↥E')) (j : Fin (finrank.{u_1, u_3} 𝕜 ↥F')),
    Eq.{u_1 + 1} (α := 𝕜)
      (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                    TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                      Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                  (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                y :
              Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
            (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
          (i, j) :
        𝕜)
      (0 : 𝕜)
⊢ y = 0

Tactic:
simp [(e.toBasis.tensorProduct f.toBasis).ext_elem_iff, this]

Premises used: Module.Basis.tensorProduct, Module.Basis.ext_elem_iff, OrthonormalBasis.toBasis
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hx :
  inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
      ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) =
    0
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
this :
  ∀ (i : Fin (finrank.{u_1, u_2} 𝕜 ↥E')) (j : Fin (finrank.{u_1, u_3} 𝕜 ↥F')),
    Eq.{u_1 + 1} (α := 𝕜)
      (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                    TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                      Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                  (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                y :
              Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
            (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
          (i, j) :
        𝕜)
      (0 : 𝕜)
⊢ y = 0

Tactic:
have : y = 0 := by simp [(e.toBasis.tensorProduct f.toBasis).ext_elem_iff, this]
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hx :
  inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
      ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) =
    0
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
this_1 :
  ∀ (i : Fin (finrank.{u_1, u_2} 𝕜 ↥E')) (j : Fin (finrank.{u_1, u_3} 𝕜 ↥F')),
    Eq.{u_1 + 1} (α := 𝕜)
      (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                    TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                      Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                  (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                y :
              Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
            (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
          (i, j) :
        𝕜)
      (0 : 𝕜)
this : y = 0
rw : Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) 0) 0
rw₁ rw₂ : Eq (α := E ⊗[𝕜] F) 0 0
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)

Tactic:
rw [this, map_zero]

Premises used: map_zero
-- 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
obtain :
  ∀ (E' : Submodule 𝕜 E) (F' : Submodule 𝕜 F) (iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E')
    (iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F') (hz : {x} ⊆ (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))),
    LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)

Tactic:
obtain ⟨E', F', iE', iF', hz⟩ := exists_finite_submodule_of_setFinite {x} (Set.finite_singleton x)

Premises used: TensorProduct.exists_finite_submodule_of_setFinite, Singleton.singleton, Set.finite_singleton
-- 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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
hz : {x} ⊆ (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
obtain :
  ∀ (y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F')
    (hz :
      singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
        (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ)
          (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
            ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)

Tactic:
obtain ⟨y, rfl⟩ := Set.singleton_subset_iff.mp hz

Premises used: Set.singleton_subset_iff, Iff.mp, 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
obtain :
  ∀ (e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ)
          (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
            ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
          ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
      ℝ)

Tactic:
obtain e := stdOrthonormalBasis 𝕜 E'

Premises used: Membership.mem, Subtype, stdOrthonormalBasis
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
obtain :
  ∀ (f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ)
          (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
            ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
          ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
      ℝ)

Tactic:
obtain f := stdOrthonormalBasis 𝕜 F'

Premises used: Membership.mem, Subtype, stdOrthonormalBasis
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
rw :
  LE.le (α := ℝ) 0
    (∑ i : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F'),
      HPow.hPow (β := ℕ)
        (norm.{u_1} (E := 𝕜)
          (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                        TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                          Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                      (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                    y :
                  Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
              i :
            𝕜))
        2)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ)
        (inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)
          ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F)) :
      ℝ)

Tactic:
rw [inner_mapIncl_mapIncl, inner_self y e f, RCLike.ofReal_re]

Premises used: RCLike.ofReal_re, _private.0.TensorProduct.inner_self, TensorProduct.inner_mapIncl_mapIncl
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
⊢ LE.le (α := ℝ) 0
    (∑ i : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F'),
      HPow.hPow (β := ℕ)
        (norm.{u_1} (E := 𝕜)
          (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                        TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                          Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                      (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                    y :
                  Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
              i :
            𝕜))
        2)

Tactic:
Finset.sum_nonneg fun _ _ ↦ sq_nonneg _

Premises used: Norm.norm, Finset.sum_nonneg, Module.Basis.repr, Module.Basis.tensorProduct, sq_nonneg, DFunLike.coe, OrthonormalBasis.toBasis
-- 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
iE' : Module.Finite.{u_1, u_2} 𝕜 ↥E'
iF' : Module.Finite.{u_1, u_3} 𝕜 ↥F'
y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
hz :
  singleton (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) ⊆
    (↑(mapIncl E' F').range : Set (E ⊗[𝕜] F))
e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'
⊢ LE.le (α := ℝ) 0
    (∑ i : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F'),
      HPow.hPow (β := ℕ)
        (norm.{u_1} (E := 𝕜)
          (((((Basis.repr (e.toBasis.tensorProduct f.toBasis) :
                        TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F' ≃ₗ[𝕜]
                          Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                      (a : ↥E' ⊗[𝕜] ↥F') → Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F') →₀ 𝕜)
                    y :
                  Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F') →₀ 𝕜) :
                (a : Fin (finrank 𝕜 ↥E') × Fin (finrank 𝕜 ↥F')) → 𝕜)
              i :
            𝕜))
        2)

Tactic:
exact Finset.sum_nonneg fun _ _ ↦ sq_nonneg _

Premises used: Finset.sum_nonneg, sq_nonneg
-- 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
x y : E ⊗[𝕜] F
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 y 0) = inner 𝕜 0 y

Tactic:
simp [inner]

Premises used: Inner.inner
-- 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
x y : E ⊗[𝕜] F
⊢ ∀ (x : E) (y : F),
    (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 (E := E ⊗[𝕜] F) 0 (x ⊗ₜ[𝕜] y)) = inner 𝕜 (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) 0

Tactic:
simp [inner]

Premises used: Inner.inner
-- 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
x y : E ⊗[𝕜] F
⊢ ∀ (x : E) (y : F) (x_1 : E) (y_1 : F),
    (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x_1 ⊗ₜ[𝕜] y_1)) =
      inner 𝕜 (E := E ⊗[𝕜] F) (x_1 ⊗ₜ[𝕜] y_1) (x ⊗ₜ[𝕜] y)

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

Tactic:
simp_all [inner]

Premises used: Inner.inner
-- 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
x y : E ⊗[𝕜] F
⊢ ∀ (x y_1 : E ⊗[𝕜] F),
    (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 y x) = inner 𝕜 x y →
      (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 y y_1) = inner 𝕜 y_1 y →
        (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 y (x + y_1)) = inner 𝕜 (x + y_1) y

Tactic:
simp_all [inner]

Premises used: Inner.inner
-- 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
y : F
⊢ norm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) = ‖x‖ * ‖y‖

Tactic:
simpa using congr(√(RCLike.re $(inner_tmul 𝕜 x x y y)))
-- 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
y : F
⊢ nnnorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) = ‖x‖₊ * ‖y‖₊

Tactic:
simp [← NNReal.coe_inj]

Premises used: NNReal.coe_inj
-- 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
y : F
⊢ nnnorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) = ‖x‖₊ * ‖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 x' : E
y y' : F
grw : norm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + norm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
⊢ dist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖

Tactic:
grw [dist_eq_norm, norm_sub_le]

Premises used: dist_eq_norm, norm_sub_le
-- 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 x' : E
y y' : F
⊢ norm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + norm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖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 x' : E
y y' : F
grw : nnnorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + nnnorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
⊢ nndist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊

Tactic:
grw [nndist_eq_nnnorm, nnnorm_sub_le]

Premises used: nndist_eq_nnnorm, nnnorm_sub_le
-- 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 x' : E
y y' : F
⊢ nnnorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + nnnorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖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 x' : E
y y' : F
grw : enorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + enorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ
⊢ edist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ

Tactic:
grw [edist_eq_enorm_sub, enorm_sub_le]

Premises used: edist_eq_enorm_sub, enorm_sub_le
-- 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 x' : E
y y' : F
⊢ enorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + enorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a b c d : 𝕜
simp :
  HMul.hMul (β := 𝕜) c ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) *
      HMul.hMul (β := 𝕜) d ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜) =
    c * d * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜)
⊢ inner 𝕜 (E := 𝕜 ⊗[𝕜] 𝕜) (a ⊗ₜ[𝕜] b) (c ⊗ₜ[𝕜] d) = inner 𝕜 (a * b) (c * d)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a b c d : 𝕜
⊢ HMul.hMul (β := 𝕜) c ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) *
      HMul.hMul (β := 𝕜) d ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜) =
    c * d * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜)

Tactic:
ring
-- 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 𝕜 x (a ⊗ₜ[𝕜] b) = inner 𝕜 y (a ⊗ₜ[𝕜] b)

Tactic:
⟨fun h _ _ ↦ h ▸ rfl, fun h ↦ innerSL_inj.mp <| ContinuousLinearMap.coe_inj.mp <| ext' h⟩

Premises used: ContinuousLinearMap.coe_inj, innerSL_inj, Eq.rec, Iff.intro, Iff.mp, TensorProduct.ext', rfl