awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
x y : E
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x,
      HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) y : E) ((V.projection U ⋯ : (a : E) → E) y : E)⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫

Tactic:
simp [inner_add_right, inner_add_left, h, inner_eq_zero_symm]

Premises used: inner_add_left, inner_add_right, inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
⊢ (U.projection V hUV).IsSymmetricProjection ↔ U ⟂ V

Tactic:
simp [isSymmetricProjection_iff, isSymmetric_projection_iff, isIdempotentElem_projection]

Premises used: Submodule.isSymmetric_projection_iff, LinearMap.isSymmetricProjection_iff, Submodule.isIdempotentElem_projection
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
rw : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ (T.range.projection T.ker ⋯).IsSymmetric
rw₁ rw₂ : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ T.range ⟂ T.ker

Tactic:
rw [← isSymmetric_projection_iff hT.isProj_range.isCompl, ← hT.eq_projection]

Premises used: LinearMap.IsProj.isCompl, LinearMap.IsIdempotentElem.eq_projection, Submodule.isSymmetric_projection_iff, LinearMap.IsIdempotentElem.isProj_range
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : ∀ (x : E), x ∈ T.rangeᗮ ↔ x ∈ T.ker
⊢ T.rangeᗮ = T.ker

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
h : x ∈ T.rangeᗮ → x ∈ T.ker
h₁ : x ∈ T.ker → x ∈ T.rangeᗮ
⊢ x ∈ T.rangeᗮ ↔ x ∈ T.ker

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ x ∈ T.rangeᗮ → x ∈ T.ker

Tactic:
simpa [Submodule.mem_orthogonal, hT _ x] using ext_inner_left 𝕜 (x := T x) (y := 0)

Premises used: Submodule.mem_orthogonal, ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ x ∈ T.ker → x ∈ T.rangeᗮ

Tactic:
simp_all [Submodule.mem_orthogonal, hT _ x]

Premises used: Submodule.mem_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
h : IsIdempotentElem T
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ T.rangeᗮ = T.ker

Tactic:
⟨fun hT => hT.orthogonal_range, fun hT =>
    h.isSymmetric_iff_isOrtho_range_ker.eq ▸ hT.symm ▸ isOrtho_orthogonal_right _⟩

Premises used: Submodule.isOrtho_orthogonal_right, Eq.rec, LinearMap.range, LinearMap.IsIdempotentElem.isSymmetric_iff_isOrtho_range_ker, Iff.intro, LinearMap.IsSymmetric.orthogonal_range, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ S = T ↔ S.range = T.range

Tactic:
⟨fun h => h ▸ rfl, fun h => ?_⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
refine : ∀ (h : S.range = T.range), S = T
⊢ S = T ↔ S.range = T.range

Tactic:
refine ⟨fun h => h ▸ rfl, fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range = T.range
rw : S.range = T.range ∧ S.rangeᗮ = T.rangeᗮ
⊢ S = T

Tactic:
rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem,
    ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric,
    ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric]

Premises used: LinearMap.IsIdempotentElem.ext_iff, LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.IsSymmetricProjection.isSymmetric, LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range = T.range
⊢ S.range = T.range ∧ S.rangeᗮ = T.rangeᗮ

Tactic:
simp [h]
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : p.range ≤ q.range
⊢ q ∘ₗ p = p

Tactic:
rw [← hq.isIdempotentElem.comp_eq_right_iff] at hqp

Premises used: LinearMap.IsIdempotentElem.comp_eq_right_iff, LinearMap.IsSymmetricProjection.isIdempotentElem
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)

Tactic:
⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜
    fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩

Premises used: LinearMap.ext, LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.IsSymmetricProjection.mk, LinearMap.IsSymmetricProjection.isSymmetric, LinearMap.IsSymmetric.sub, ext_inner_left, IsIdempotentElem.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
refine : ∀ (x y : E), ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)

Tactic:
refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜
    fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
x y : E
simp_rw : ⟪y, (p : (a : E) → E) ((q : (a : E) → E) x : E)⟫ = ⟪y, (p : (a : E) → E) x⟫
simp_rw₁ : inner 𝕜 (E := E) ((p : (a : E) → E) y : E) ((q : (a : E) → E) x : E) = ⟪(p : (a : E) → E) y, x⟫
simp_rw₂ : ⟪(q : (a : E) → E) ((p : (a : E) → E) y : E), x⟫ = ⟪(p : (a : E) → E) y, x⟫
simp_rw₃ : ⟪(q ∘ₗ p : (a : E) → E) y, x⟫ = ⟪(p : (a : E) → E) y, x⟫
⊢ ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫

Tactic:
simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp]

Premises used: LinearMap.comp_apply, LinearMap.IsSymmetricProjection.isSymmetric, Module.End.mul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
hf' : f ≠ 0
α : 𝕜
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f) ↔ IsSelfAdjoint α

Tactic:
⟨fun h ↦ ?_, hf.smul⟩

Premises used: LinearMap.IsSymmetric.smul, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
hf' : f ≠ 0
α : 𝕜
refine : ∀ (h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f)), IsSelfAdjoint α
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f) ↔ IsSelfAdjoint α

Tactic:
refine ⟨fun h ↦ ?_, hf.smul⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
hf' : f ≠ 0
α : 𝕜
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f)
⊢ ¬∀ (x v : E), ⟪v, (f : (a : E) → E) x⟫ = 0

Tactic:
simp only [ne_eq, LinearMap.ext_iff, zero_apply, ext_iff_inner_left 𝕜 (E := E),
    inner_zero_right] at hf'

Premises used: LinearMap.zero_apply, LinearMap.ext_iff, ne_eq, ext_iff_inner_left, inner_zero_right
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
α : 𝕜
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f)
hf' : ¬∀ (x v : E), ⟪v, (f : (a : E) → E) x⟫ = 0
⊢ IsSelfAdjoint α

Tactic:
simpa [IsSymmetric, inner_smul_left, inner_smul_right, hf _ _, forall_or_left,
    (forall_comm.eq ▸ hf')] using h

Premises used: inner_smul_right, forall_or_left, LinearMap.IsSymmetric, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.TensorProduct
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
⊢ inner 𝕜 x y = (((inner_ : (a : E ⊗[𝕜] F) → E ⊗[𝕜] F →ₗ[𝕜] 𝕜) x : E ⊗[𝕜] F →ₗ[𝕜] 𝕜) : (a : E ⊗[𝕜] F) → 𝕜) y

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
x x' : E
y y' : F
⊢ inner 𝕜 (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y'

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, 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 y : E ⊗[𝕜] F
⊢ inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) 0 : G ⊗[𝕜] H)
      ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y : G ⊗[𝕜] H) =
    inner 𝕜 0 y

Tactic:
simp [inner_def]

Premises used: _private.0.TensorProduct.inner_def
-- 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 y : E ⊗[𝕜] F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x ⊗ₜ[𝕜] y) : G ⊗[𝕜] H)
        ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) 0 : G ⊗[𝕜] H) =
      inner 𝕜 (E := E ⊗[𝕜] F) (x ⊗ₜ[𝕜] y) 0

Tactic:
simp [inner_def]

Premises used: _private.0.TensorProduct.inner_def
-- 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 y : E ⊗[𝕜] F
⊢ ∀ (x : E) (y : F) (x_1 : E) (y_1 : F),
    inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x_1 ⊗ₜ[𝕜] y_1) : G ⊗[𝕜] H)
        ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x ⊗ₜ[𝕜] y) : G ⊗[𝕜] H) =
      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
f : E →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x y : E ⊗[𝕜] F
⊢ ∀ (x y : E ⊗[𝕜] F),
    (∀ (x_1 : E) (y : F),
        inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x_1 ⊗ₜ[𝕜] y) : G ⊗[𝕜] H)
            ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H) =
          inner 𝕜 (x_1 ⊗ₜ[𝕜] y) x) →
      (∀ (x : E) (y_1 : F),
          inner 𝕜 (E := G ⊗[𝕜] H)
              ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x ⊗ₜ[𝕜] y_1) : G ⊗[𝕜] H)
              ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y : G ⊗[𝕜] H) =
            inner 𝕜 (x ⊗ₜ[𝕜] y_1) y) →
        ∀ (x_1 : E) (y_1 : F),
          inner 𝕜 (E := G ⊗[𝕜] H)
              ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x_1 ⊗ₜ[𝕜] y_1) : G ⊗[𝕜] H)
              ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x + y) : G ⊗[𝕜] H) =
            inner 𝕜 (x_1 ⊗ₜ[𝕜] y_1) (x + y)

Tactic:
simp_all [inner_def]

Premises used: _private.0.TensorProduct.inner_def
-- 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 y : E ⊗[𝕜] F
⊢ ∀ (x y_1 : E ⊗[𝕜] F),
    inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) x : G ⊗[𝕜] H)
          ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y : G ⊗[𝕜] H) =
        inner 𝕜 x y →
      inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y_1 : G ⊗[𝕜] H)
            ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y : G ⊗[𝕜] H) =
          inner 𝕜 y_1 y →
        inner 𝕜 (E := G ⊗[𝕜] H) ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) (x + y_1) : G ⊗[𝕜] H)
            ((map f.toLinearMap g.toLinearMap : (a : E ⊗[𝕜] F) → G ⊗[𝕜] H) y : G ⊗[𝕜] H) =
          inner 𝕜 (x + y_1) y

Tactic:
simp_all [inner_def]

Premises used: _private.0.TensorProduct.inner_def
-- 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 y : TensorProduct.{u_1, u_2, u_3} 𝕜 ↥E' ↥F'
⊢ inner 𝕜 (E := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
      ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) =
    inner 𝕜 x y

Tactic:
inner_map_map E'.subtypeₗᵢ F'.subtypeₗᵢ x y

Premises used: Set.Mem, Submodule.subtypeₗᵢ, TensorProduct.inner_map_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
x : E ⊗[𝕜] F
hx : inner 𝕜 x x = 0
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
⊢ x = 0

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
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))
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)
⊢ x = 0

Tactic:
obtain ⟨y : E' ⊗ F', rfl : mapIncl E' F' y = x⟩ := 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'
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))
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)
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : 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'
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'
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)
⊢ Eq (α := E ⊗[𝕜] F) ((mapIncl E' F' : (a : ↥E' ⊗[𝕜] ↥F') → E ⊗[𝕜] F) y : E ⊗[𝕜] F) (0 : 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'
hx :
  ∀ (i : Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F')),
    Membership.mem (γ := Finset (Fin (finrank.{u_1, u_2} 𝕜 ↥E') × Fin (finrank.{u_1, u_3} 𝕜 ↥F'))) Finset.univ i →
      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 =
        0
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:
simpa using hx (i, j)

Premises used: Prod.mk