awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (x : E),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
      ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜
x : E
⊢ Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x : F)

Tactic:
exact ext_inner_right_basis b fun i => by simp only [h i, adjoint_inner_left]

Premises used: InnerProductSpace.ext_inner_right_basis
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
inst_7 : FiniteDimensional 𝕜 E
inst_8 : FiniteDimensional 𝕜 F
inst_9 : FiniteDimensional 𝕜 G
⊢ StarModule.{u_1, u_2} 𝕜 (E →ₗ[𝕜] E)

Tactic:
⟨map_smulₛₗ adjoint⟩

Premises used: MulActionSemiHomClass.map_smulₛₗ, StarModule.mk, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ star A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ IsSelfAdjoint A ↔ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, Iff.rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
rw : A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A ↔ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A ↔ IsSelfAdjoint A

Tactic:
rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]

Premises used: LinearMap.isSelfAdjoint_iff', LinearMap.eq_adjoint_iff, LinearMap.IsSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A ↔ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A

Tactic:
eq_comm

Premises used: eq_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A ↔ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A

Tactic:
exact eq_comm

Premises used: eq_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ Membership.mem (γ := Submonoid (E →ₗ[𝕜] E)) (unitary (E →ₗ[𝕜] E)) id

Tactic:
one_mem _

Premises used: Set.Mem, setOf, OneMemClass.one_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((flip (innerₛₗ 𝕜) : (a : F) → F →ₗ⋆[𝕜] 𝕜) ((A : (a : E) → F) x) : F →ₗ⋆[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
    ((((flip (innerₛₗ 𝕜) : (a : E) → E →ₗ⋆[𝕜] 𝕜) x : E →ₗ⋆[𝕜] 𝕜) : (a : E) → 𝕜)
        ((((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y : E) :
      𝕜)

Tactic:
simp [adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
S : E →ₗ[𝕜] F
x x_1 : F
⊢ ⟪(S ∘ₗ T ∘ₗ (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S : (a : F) → F) x, x_1⟫_𝕜 =
    ⟪x, (S ∘ₗ T ∘ₗ (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S : (a : F) → F) x_1⟫_𝕜

Tactic:
simp [← adjoint_inner_right, hT]

Premises used: LinearMap.adjoint_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ IsSymmetric.{u_1, u_3} (𝕜 := 𝕜) (E := F) (T ∘ₗ (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T)

Tactic:
simpa using LinearMap.IsSymmetric.id.conj_adjoint T

Premises used: LinearMap.IsSymmetric.conj_adjoint, LinearMap.IsSymmetric.id
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
S : F →ₗ[𝕜] E
⊢ IsSymmetric.{u_1, u_3} (𝕜 := 𝕜) (E := F) ((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S ∘ₗ T ∘ₗ S)

Tactic:
simpa using hT.conj_adjoint S.adjoint

Premises used: LinearMap.IsSymmetric.conj_adjoint, DFunLike.coe, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)

Tactic:
simpa using LinearMap.IsSymmetric.id.adjoint_conj T

Premises used: LinearMap.IsSymmetric.adjoint_conj, LinearMap.IsSymmetric.id
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x y : E
⊢ ⟪(HMul.hMul (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) T : (a : E) → E) x, y⟫_𝕜 =
    ⟪x, (HMul.hMul (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) T : (a : E) → E) y⟫_𝕜

Tactic:
simp [adjoint_inner_left, adjoint_inner_right]

Premises used: LinearMap.adjoint_inner_right, LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
simp :
  LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪x, (HMul.hMul (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) T : (a : E) → E) x⟫_𝕜 :
      ℝ)

Tactic:
simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Premises used: inner_self_eq_norm_sq_to_K, LinearMap.adjoint_inner_right, Module.End.mul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
norm_cast : 0 ≤ HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2

Tactic:
sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2

Tactic:
exact sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
simp :
  Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
    (0 : ℝ)
⊢ Eq (α := ℝ)
    ((im : (a : 𝕜) → ℝ)
        ⟪x, (((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) : (a : E) → E) ((T : (a : E) → E) x : E)⟫_𝕜 :
      ℝ)
    (0 : ℝ)

Tactic:
simp only [adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Premises used: inner_self_eq_norm_sq_to_K, LinearMap.adjoint_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
    (0 : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ have this : CompleteSpace E := ⋯;
  IsSelfAdjoint (R := E →L[𝕜] E)
      (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) ↔
    IsSelfAdjoint T

Tactic:
simp [IsSelfAdjoint, star, adjoint,
    ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]

Premises used: IsSelfAdjoint, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap, LinearMap.adjoint, Star.star
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
simp :
  Eq (α := E →L[𝕜] E)
      ((LinearIsometryEquiv.toLinearEquiv.{u_1, u_1, u_2, u_2} (E := E →L[𝕜] E) ContinuousLinearMap.adjoint :
            (a : E →L[𝕜] E) → E →L[𝕜] E)
          (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
            E →L[𝕜] E) :
        E →L[𝕜] E)
      (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
        E →L[𝕜] E) ↔
    (ContinuousLinearMap.adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
⊢ have this : CompleteSpace E := ⋯;
  IsSelfAdjoint (↑T : E →ₗ[𝕜] E) ↔ IsSelfAdjoint T

Tactic:
simp only [IsSelfAdjoint, star, adjoint, LinearEquiv.trans_apply,
    coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]

Premises used: IsSelfAdjoint, LinearEquiv.trans_apply, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap, LinearMap.coe_toContinuousLinearMap_symm, LinearMap.adjoint, Star.star
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ Eq (α := E →L[𝕜] E)
      ((LinearIsometryEquiv.toLinearEquiv.{u_1, u_1, u_2, u_2} (E := E →L[𝕜] E) ContinuousLinearMap.adjoint :
            (a : E →L[𝕜] E) → E →L[𝕜] E)
          (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
            E →L[𝕜] E) :
        E →L[𝕜] E)
      (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
        E →L[𝕜] E) ↔
    (ContinuousLinearMap.adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ have this : CompleteSpace E := ⋯;
  IsStarProjection (R := E →L[𝕜] E)
      (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) ↔
    IsStarProjection T

Tactic:
simp [isStarProjection_iff, isSelfAdjoint_toContinuousLinearMap_iff,
    ← ContinuousLinearMap.isIdempotentElem_toLinearMap_iff]

Premises used: LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, ContinuousLinearMap.isIdempotentElem_toLinearMap_iff, isStarProjection_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ IsStarProjection T ↔ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T

Tactic:
simp [← isStarProjection_toContinuousLinearMap_iff,
    ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection]

Premises used: ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection, LinearMap.isStarProjection_toContinuousLinearMap_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ CompleteSpace E

Tactic:
have := FiniteDimensional.complete 𝕜 E
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
this : CompleteSpace E
⊢ S = T ↔ S.range = T.range

Tactic:
simpa using ContinuousLinearMap.IsStarProjection.ext_iff
    (S.isStarProjection_toContinuousLinearMap_iff.mpr hS)
    (T.isStarProjection_toContinuousLinearMap_iff.mpr hT)

Premises used: Iff.mpr, ContinuousLinearMap.IsStarProjection.ext_iff, LinearMap.isStarProjection_toContinuousLinearMap_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
x : E
⊢ Eq (α := 𝕜 →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) : 𝕜 →ₗ[𝕜] E)
    (toSpanSingleton 𝕜 E x : 𝕜 →ₗ[𝕜] E)

Tactic:
have := FiniteDimensional.complete 𝕜 E
  ext fun _ ↦ congr($(ContinuousLinearMap.adjoint_innerSL_apply x) _)

Premises used: LinearMap.ext, congrArg, id, FiniteDimensional.complete, DFunLike.coe, ContinuousLinearMap.adjoint_innerSL_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
x : E
⊢ Eq (α := E →ₗ[𝕜] 𝕜) ((adjoint : (a : 𝕜 →ₗ[𝕜] E) → E →ₗ[𝕜] 𝕜) (toSpanSingleton 𝕜 E x) : E →ₗ[𝕜] 𝕜)
    ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜)

Tactic:
simp [← adjoint_innerₛₗ_apply]

Premises used: LinearMap.adjoint_innerₛₗ_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
U : Submodule 𝕜 E
⊢ Membership.mem (γ := Sublattice (Submodule 𝕜 E)) (invtSubmodule ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T)) U ↔
    Uᗮ ∈ invtSubmodule T

Tactic:
have := FiniteDimensional.complete 𝕜 E
  ContinuousLinearMap.mem_invtSubmodule_adjoint_iff

Premises used: Set.Mem, setOf, FiniteDimensional.complete, ContinuousLinearMap.mem_invtSubmodule_adjoint_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
⊢ (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1

Tactic:
⟨fun h ↦ ext fun x ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, ContinuousLinearMap.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
refine_1 :
  ∀ (h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜)
    (x : H),
    Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
      ((1 : (a : H) → H) x : H)
refine_2 :
  ∀ (h : Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1) (x y : H),
    inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
⊢ (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1

Tactic:
refine ⟨fun h ↦ ext fun x ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
x : H
⊢ Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)

Tactic:
ext_inner_right 𝕜 fun y ↦ ?_

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
x : H
refine_1 :
  ∀ (y : H),
    ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x, y⟫_𝕜 =
      ⟪(1 : (a : H) → H) x, y⟫_𝕜
⊢ Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)

Tactic:
refine ext_inner_right 𝕜 fun y ↦ ?_

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
x y : H
⊢ ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x, y⟫_𝕜 =
    ⟪(1 : (a : H) → H) x, y⟫_𝕜

Tactic:
simpa [star_eq_adjoint, adjoint_inner_left] using h x y

Premises used: ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.star_eq_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
h : Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
⊢ ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜

Tactic:
simp [← adjoint_inner_left, ← comp_apply, h]

Premises used: ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
rw :
  (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
rw₁ rw₂ :
  Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1 ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
⊢ (∀ (x : H), norm.{u_6} (E := K) ((u : (a : H) → K) x : K) = ‖x‖) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1

Tactic:
rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_map_iff_adjoint_comp_self]

Premises used: ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, LinearMap.norm_map_iff_inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
u : H →L[𝕜] K
rw :
  (∀ (x : H), norm.{u_6} (E := K) ((u : (a : H) → K) x : K) = ‖x‖) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
rw₁ rw₂ :
  Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1 ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
⊢ Isometry.{u_5, u_6} (α := H) (β := K) (⇑u : (a : H) → K) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1

Tactic:
rw [AddMonoidHomClass.isometry_iff_norm, norm_map_iff_adjoint_comp_self]

Premises used: AddMonoidHomClass.isometry_iff_norm, ContinuousLinearMap.norm_map_iff_adjoint_comp_self
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
⊢ Eq (α := K →L[𝕜] H) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K) : K →L[𝕜] H)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K))
        ((↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K) ∘SL (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)) :
      K →L[𝕜] H)

Tactic:
simp