awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := G ⊗[𝕜] F →ₗ[𝕜] G ⊗[𝕜] E)
    ((adjoint : (a : G ⊗[𝕜] E →ₗ[𝕜] G ⊗[𝕜] F) → G ⊗[𝕜] F →ₗ[𝕜] G ⊗[𝕜] E) (lTensor G f) : G ⊗[𝕜] F →ₗ[𝕜] G ⊗[𝕜] E)
    (lTensor G ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) f) : G ⊗[𝕜] F →ₗ[𝕜] G ⊗[𝕜] E)

Tactic:
simp [lTensor]

Premises used: LinearMap.lTensor
-- 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)
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))
⊢ x = y ↔ ∀ (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]

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.inner_map_eq_flip, Function.Injective.eq_iff, LinearIsometryEquiv.injective, TensorProduct.assocIsometry, 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
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) (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
-- 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: TensorProduct.ext_iff_inner_right_threefold', starRingEnd_apply, star_inj, inner_conj_symm
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
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

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
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:
simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]

Premises used: and_comm, Iff.mp, orthonormal_iff_ite, ite_and
-- 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
ι₁ : 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
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
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) fun (i : ι₁ × ι₂) ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

Tactic:
classical
  rw [orthonormal_iff_ite]
  rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]

Premises used: and_comm, Iff.mp, orthonormal_iff_ite, ite_and
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal.{u_1, u_2, u_6} 𝕜 (E := E) (ι := ι₁) (⇑b₁ : (a : ι₁) → E)
hb₂ : Orthonormal.{u_1, u_3, u_7} 𝕜 (E := F) (ι := ι₂) (⇑b₂ : (a : ι₂) → F)
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) fun (i : ι₁ × ι₂) ↦ (b₁ : (a : ι₁) → E) i.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) i.2

Tactic:
hb₁.tmul hb₂

Premises used: Orthonormal.tmul
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal.{u_1, u_2, u_6} 𝕜 (E := E) (ι := ι₁) (⇑b₁ : (a : ι₁) → E)
hb₂ : Orthonormal.{u_1, u_3, u_7} 𝕜 (E := F) (ι := ι₂) (⇑b₂ : (a : ι₂) → F)
h :
  ∀ (x : ι₁ × ι₂),
    Eq (α := E ⊗[𝕜] F) (((b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
      ((b₁ : (a : ι₁) → E) x.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) x.2 : E ⊗[𝕜] F)
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) (ι := ι₁ × ι₂)
    (⇑(b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F)

Tactic:
convert! hb₁.tmul hb₂

Premises used: Orthonormal.tmul
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal.{u_1, u_2, u_6} 𝕜 (E := E) (ι := ι₁) (⇑b₁ : (a : ι₁) → E)
hb₂ : Orthonormal.{u_1, u_3, u_7} 𝕜 (E := F) (ι := ι₂) (⇑b₂ : (a : ι₂) → F)
x : ι₁ × ι₂
⊢ Eq (α := E ⊗[𝕜] F) (((b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
    ((b₁ : (a : ι₁) → E) x.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) x.2 : E ⊗[𝕜] F)

Tactic:
b₁.tensorProduct_apply' b₂ _

Premises used: Module.Basis.tensorProduct_apply'
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal.{u_1, u_2, u_6} 𝕜 (E := E) (ι := ι₁) (⇑b₁ : (a : ι₁) → E)
hb₂ : Orthonormal.{u_1, u_3, u_7} 𝕜 (E := F) (ι := ι₂) (⇑b₂ : (a : ι₂) → F)
x : ι₁ × ι₂
⊢ Eq (α := E ⊗[𝕜] F) (((b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
    ((b₁ : (a : ι₁) → E) x.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) x.2 : E ⊗[𝕜] F)

Tactic:
exact b₁.tensorProduct_apply' b₂ _

Premises used: Module.Basis.tensorProduct_apply'
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
b₁ : OrthonormalBasis ι₁ 𝕜 E
b₂ : OrthonormalBasis ι₂ 𝕜 F
i : ι₁
j : ι₂
⊢ Eq (α := E ⊗[𝕜] F) ((b₁.tensorProduct b₂ : (a : ι₁ × ι₂) → E ⊗[𝕜] F) (i, j) : E ⊗[𝕜] F)
    ((b₁ : (a : ι₁) → E) i ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) j : E ⊗[𝕜] F)

Tactic:
simp [OrthonormalBasis.tensorProduct]

Premises used: OrthonormalBasis.tensorProduct
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
b₁ : OrthonormalBasis ι₁ 𝕜 E
b₂ : OrthonormalBasis ι₂ 𝕜 F
i : ι₁ × ι₂
⊢ Eq (α := E ⊗[𝕜] F) ((b₁.tensorProduct b₂ : (a : ι₁ × ι₂) → E ⊗[𝕜] F) i : E ⊗[𝕜] F)
    ((b₁ : (a : ι₁) → E) i.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) i.2 : E ⊗[𝕜] F)

Tactic:
tensorProduct_apply _ _ _ _

Premises used: OrthonormalBasis.tensorProduct_apply
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
b₁ : OrthonormalBasis ι₁ 𝕜 E
b₂ : OrthonormalBasis ι₂ 𝕜 F
x : E
y : F
i : ι₁
j : ι₂
⊢ WithLp.ofLp (p := 2) (((b₁.tensorProduct b₂).repr : (a : E ⊗[𝕜] F) → EuclideanSpace 𝕜 (ι₁ × ι₂)) (x ⊗ₜ[𝕜] y)) (i, j) =
    HMul.hMul (α := (fun (x : ι₂) ↦ 𝕜) j) (WithLp.ofLp (p := 2) ((b₂.repr : (a : F) → EuclideanSpace 𝕜 ι₂) y) j)
      (WithLp.ofLp (p := 2) ((b₁.repr : (a : E) → EuclideanSpace 𝕜 ι₁) x) i)

Tactic:
simp [OrthonormalBasis.tensorProduct]

Premises used: OrthonormalBasis.tensorProduct
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
b₁ : OrthonormalBasis ι₁ 𝕜 E
b₂ : OrthonormalBasis ι₂ 𝕜 F
x : E
y : F
i : ι₁ × ι₂
⊢ WithLp.ofLp (p := 2) (((b₁.tensorProduct b₂).repr : (a : E ⊗[𝕜] F) → EuclideanSpace 𝕜 (ι₁ × ι₂)) (x ⊗ₜ[𝕜] y)) i =
    HMul.hMul (α := (fun (x : ι₂) ↦ 𝕜) i.2) (WithLp.ofLp (p := 2) ((b₂.repr : (a : F) → EuclideanSpace 𝕜 ι₂) y) i.2)
      (WithLp.ofLp (p := 2) ((b₁.repr : (a : E) → EuclideanSpace 𝕜 ι₁) x) i.1)

Tactic:
tensorProduct_repr_tmul_apply _ _ _ _ _ _

Premises used: OrthonormalBasis.tensorProduct_repr_tmul_apply
-- 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
ι₁ : Type u_6
ι₂ : Type u_7
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
b₁ : OrthonormalBasis ι₁ 𝕜 E
b₂ : OrthonormalBasis ι₂ 𝕜 F
⊢ (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis

Tactic:
simp [OrthonormalBasis.tensorProduct]

Premises used: OrthonormalBasis.tensorProduct
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜)
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) :
      𝕜)

Tactic:
rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]

Premises used: LinearMap.trace_eq_matrix_trace, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (a : ι),
    Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) a =
      inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) a : E) ((T : (a : E) → E) ((b : (a : ι) → E) a : E) : E)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))

Tactic:
apply Fintype.sum_congr

Premises used: Fintype.sum_congr
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
h :
  (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₁ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜)
      i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₂ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₃ :
  WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((T : (a : E) → E) ((b : (a : ι) → E) i : E))) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₄ h₅ :
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)

Tactic:
rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]

Premises used: OrthonormalBasis.repr_apply_apply, OrthonormalBasis.coe_toBasis, Matrix.diag_apply, OrthonormalBasis.coe_toBasis_repr_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
rw rw₁ rw₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
h h₁ :
  ∀ (i : ι),
    Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
      inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜)
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) :
      𝕜)

Tactic:
classical
  rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
  apply Fintype.sum_congr
  intro i
  rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]

Premises used: Fintype.sum_congr, OrthonormalBasis.repr_apply_apply, OrthonormalBasis.coe_toBasis, Matrix.diag_apply, OrthonormalBasis.coe_toBasis_repr_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜) ((↑(∑ i : Fin n, hT.eigenvalues hn i) : 𝕜) : 𝕜)

Tactic:
simp [Module.End.trace_eq_sum_roots_charpoly_of_splits hT.splits_charpoly,
    hT.roots_charpoly_eq_eigenvalues hn, List.sum_ofFn]

Premises used: LinearMap.IsSymmetric.splits_charpoly, List.sum_ofFn, Module.End.trace_eq_sum_roots_charpoly_of_splits, LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
rw :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ i : Fin n, hT.eigenvalues hn i) : 𝕜) : ℝ)
    (∑ i : Fin n, hT.eigenvalues hn i : ℝ)
rw₁ : Module.finrank 𝕜 E = n
rw₂ : ℕ
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜) : ℝ)
    (∑ i : Fin n, hT.eigenvalues hn i : ℝ)

Tactic:
rw [hT.trace_eq_sum_eigenvalues]

Premises used: LinearMap.IsSymmetric.trace_eq_sum_eigenvalues
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ i : Fin n, hT.eigenvalues hn i) : 𝕜) : ℝ)
    (∑ i : Fin n, hT.eigenvalues hn i : ℝ)

Tactic:
RCLike.ofReal_re_ax _

Premises used: RCLike.ofReal_re_ax
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
x y : E
rw :
  (trace 𝕜 𝕜 : (a : 𝕜 →ₗ[𝕜] 𝕜) → 𝕜)
      ((↑(ContinuousLinearMap.toSpanSingleton 𝕜 ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) y : E →L[𝕜] 𝕜) : (a : E) → 𝕜) x)) :
          𝕜 →ₗ[𝕜] 𝕜) :
        𝕜 →ₗ[𝕜] 𝕜) =
    ⟪y, x⟫_𝕜
⊢ (trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜)
      (↑((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) y) : E →ₗ[𝕜] E) =
    ⟪y, x⟫_𝕜

Tactic:
rw [rankOne_def', ContinuousLinearMap.coe_comp, trace_comp_comm',
    ← ContinuousLinearMap.coe_comp, ContinuousLinearMap.comp_toSpanSingleton]

Premises used: ContinuousLinearMap.coe_comp, InnerProductSpace.rankOne_def', LinearMap.trace_comp_comm', ContinuousLinearMap.comp_toSpanSingleton
-- Module: Mathlib.Analysis.InnerProductSpace.Trace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 𝕜 : (a : 𝕜 →ₗ[𝕜] 𝕜) → 𝕜)
      ((↑(ContinuousLinearMap.toSpanSingleton 𝕜 ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) y : E →L[𝕜] 𝕜) : (a : E) → 𝕜) x)) :
          𝕜 →ₗ[𝕜] 𝕜) :
        𝕜 →ₗ[𝕜] 𝕜) =
    ⟪y, x⟫_𝕜

Tactic:
simp [trace_eq_sum_inner _ (OrthonormalBasis.singleton Unit 𝕜)]

Premises used: LinearMap.trace_eq_sum_inner, OrthonormalBasis.singleton, Unit
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z : E [⋀^Fin 0]→ₗ[ℝ] ℝ ≃ₗ[ℝ] ℝ := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
y : E [⋀^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
  (LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ :
        (a : E [⋀^Fin 0]→ₗ[ℝ] ℝ →ₗ[ℝ] ℝ) → (E →ₗ[ℝ] E [⋀^Fin 0]→ₗ[ℝ] ℝ) →ₗ[ℝ] E →ₗ[ℝ] ℝ)
      (↑z : E [⋀^Fin 0]→ₗ[ℝ] ℝ →ₗ[ℝ] ℝ) ∘ₗ
    AlternatingMap.curryLeftLinearMap
⊢ E →ₗ[ℝ] E →ₗ[ℝ] ℝ

Tactic:
exact y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm

Premises used: AlternatingMap.curryLeftLinearMap, DFunLike.coe, Orientation.volumeForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ)

Tactic:
simp [areaForm]

Premises used: Orientation.areaForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
rw : Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rw [areaForm_to_volumeForm]

Premises used: Orientation.areaForm_to_volumeForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)

Tactic:
o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)

Premises used: AlternatingMap.map_eq_zero_of_eq, Matrix.vecEmpty, Matrix.vecCons, Orientation.volumeForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
refine_1 : ![x, x] 0 = ![x, x] 1
refine_2 : Ne (α := Fin 2) 0 1
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)

Tactic:
refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)

Premises used: AlternatingMap.map_eq_zero_of_eq, Matrix.vecEmpty, Matrix.vecCons, Orientation.volumeForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ![x, x] 0 = ![x, x] 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Ne (α := Fin 2) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
simp :
  Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ) (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)

Tactic:
simp only [areaForm_to_volumeForm]

Premises used: Orientation.areaForm_to_volumeForm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) : ℝ)
    (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)

Tactic:
o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)

Premises used: Matrix.vecEmpty, AlternatingMap.map_swap, Matrix.vecCons, Orientation.volumeForm