awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
hx : inner 𝕜 x x = 0
⊢ x = 0
have 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))), x = 0
Tactic: obtain ⟨E', F', iE', iF', hz⟩ := exists_finite_submodule_of_setFinite {x} (Set.finite_singleton x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
hx : inner 𝕜 x x = 0
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))
⊢ x = 0
have obtain : ∀ (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))),
  Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
Tactic: obtain ⟨y : E' ⊗ F', rfl : mapIncl E' F' y = x⟩ := Set.singleton_subset_iff.mp hz
Cleared hypotheses: x, hx, hz
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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))
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have obtain : ∀ (e : OrthonormalBasis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥E')) 𝕜 ↥E'),
  Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
Tactic: obtain e := stdOrthonormalBasis 𝕜 E'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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'
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have obtain : ∀ (f : OrthonormalBasis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥F')) 𝕜 ↥F'),
  Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
Tactic: obtain f := stdOrthonormalBasis 𝕜 F'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (hypothesis)
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'
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have 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 : 𝕜)
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)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (hypothesis)
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 : 𝕜)
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have this₁ : y = 0
Tactic: have : y = 0 := by simp [(e.toBasis.tensorProduct f.toBasis).ext_elem_iff, this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have rw : Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) 0) 0
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : E ⊗[𝕜] F)
have rw₁ : Eq (α := E ⊗[𝕜] F) 0 0
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)
have 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) : ℝ)
Tactic: obtain ⟨E', F', iE', iF', hz⟩ := exists_finite_submodule_of_setFinite {x} (Set.finite_singleton x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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))
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)
have 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)) :
      ℝ)
Tactic: obtain ⟨y, rfl⟩ := Set.singleton_subset_iff.mp hz
Cleared hypotheses: x, hz
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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))
⊢ 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)) :
      ℝ)
have 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)) :
      ℝ)
Tactic: obtain e := stdOrthonormalBasis 𝕜 E'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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'
⊢ 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)) :
      ℝ)
have 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)) :
      ℝ)
Tactic: obtain f := stdOrthonormalBasis 𝕜 F'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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 : ℝ)
    ((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)) :
      ℝ)
have 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)
Tactic: rw [inner_mapIncl_mapIncl, inner_self y e f, RCLike.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ dist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
have grw : norm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + norm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
Tactic: grw [dist_eq_norm, norm_sub_le]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ nndist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
have grw : nnnorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + nnnorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
Tactic: grw [nndist_eq_nnnorm, nnnorm_sub_le]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
⊢ edist (α := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ
have grw : enorm (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) + enorm (E := E ⊗[𝕜] F) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ
Tactic: grw [edist_eq_enorm_sub, enorm_sub_le]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a b c d : 𝕜
⊢ inner 𝕜 (E := 𝕜 ⊗[𝕜] 𝕜) (a ⊗ₜ[𝕜] b) (c ⊗ₜ[𝕜] d) = inner 𝕜 (a * b) (c * d)
have simp : HMul.hMul (β := 𝕜) c ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) *
    HMul.hMul (β := 𝕜) d ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜) =
  c * d * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) b : 𝕜)
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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 →ₗᵢ[𝕜] E ⊗[𝕜] F) (mapIsometry LinearIsometry.id LinearIsometry.id) LinearIsometry.id
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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 →ₗ[𝕜] 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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))
have simp : (∀ (a : E) (b : F) (c : G),
    inner 𝕜 x
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (assocIsometry 𝕜 E F G)) :
            (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G))
          (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c)) =
      inner 𝕜 y
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (assocIsometry 𝕜 E F G)) :
            (a : E ⊗[𝕜] F ⊗[𝕜] G) → E ⊗[𝕜] (F ⊗[𝕜] G))
          (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c))) ↔
  ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) = inner 𝕜 y (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c))
Tactic: simp only [← (assocIsometry 𝕜 E F G).symm.injective.eq_iff,
    ext_iff_inner_right_threefold, LinearIsometryEquiv.inner_map_eq_flip]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) fun (i : ι₁ × ι₂) ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
have rw : ∀ (i j : ι₁ × ι₂), inner 𝕜 (E := E ⊗[𝕜] F) (b₁ i.1 ⊗ₜ[𝕜] b₂ i.2) (b₁ j.1 ⊗ₜ[𝕜] b₂ j.2) = if i = j then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) fun (i : ι₁ × ι₂) ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
have rw : ∀ (i j : ι₁ × ι₂), inner 𝕜 (E := E ⊗[𝕜] F) (b₁ i.1 ⊗ₜ[𝕜] b₂ i.2) (b₁ j.1 ⊗ₜ[𝕜] b₂ j.2) = if i = j then 1 else 0
Tactic: classical
  rw [orthonormal_iff_ite]
  rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
rw rw₁ rw₂ :
  ∀ (i j : ι₁ × ι₂), inner 𝕜 (E := E ⊗[𝕜] F) (b₁ i.1 ⊗ₜ[𝕜] b₂ i.2) (b₁ j.1 ⊗ₜ[𝕜] b₂ j.2) = if i = j then 1 else 0
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) fun (i : ι₁ × ι₂) ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
have rw₃ : ∀ (i₁ : ι₁) (i₂ : ι₂) (j₁ : ι₁) (j₂ : ι₂),
  inner 𝕜 (E := E ⊗[𝕜] F) (b₁ (i₁, i₂).1 ⊗ₜ[𝕜] b₂ (i₁, i₂).2) (b₁ (j₁, j₂).1 ⊗ₜ[𝕜] b₂ (j₁, j₂).2) =
    if (i₁, i₂) = (j₁, j₂) then 1 else 0
Tactic: classical
  rw [orthonormal_iff_ite]
  rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]