awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
S : E →L[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ S = T ↔ (↑S : E →ₗ[𝕜] E).range = (↑T : E →ₗ[𝕜] E).range

Tactic:
simpa using hS.isSymmetricProjection.ext_iff hT.isSymmetricProjection

Premises used: LinearMap.IsSymmetricProjection.ext_iff, ContinuousLinearMap.IsStarProjection.isSymmetricProjection
-- 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 : CompleteSpace E
x : E
hx : ‖x‖ = 1
⊢ IsStarProjection (R := E →L[𝕜] E)
    ((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) x : E →L[𝕜] E)

Tactic:
(isSymmetricProjection_rankOne_self hx).isStarProjection

Premises used: InnerProductSpace.isSymmetricProjection_rankOne_self, ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjection
-- 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 : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
h :
  Membership.mem (γ := Sublattice (Submodule 𝕜 E))
    (invtSubmodule (↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E)) U
simp :
  ∀
    (h :
      ∀ x ∈ U,
        Membership.mem (α := E) U ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E))
    (x : E), (∀ u ∈ U, ⟪u, x⟫_𝕜 = 0) → ∀ u ∈ U, ⟪u, (T : (a : E) → E) x⟫_𝕜 = 0
⊢ Uᗮ ∈ invtSubmodule (↑T : E →ₗ[𝕜] E)

Tactic:
simp only [mem_invtSubmodule_iff_forall_mem_of_mem, coe_coe, mem_orthogonal] at h ⊢

Premises used: ContinuousLinearMap.coe_coe, Submodule.mem_orthogonal, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem
-- 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 : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
h : ∀ x ∈ U, Membership.mem (α := E) U ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E)
⊢ ∀ (x : E), (∀ u ∈ U, ⟪u, x⟫_𝕜 = 0) → ∀ u ∈ U, ⟪u, (T : (a : E) → E) x⟫_𝕜 = 0

Tactic:
grind [T.adjoint_inner_left]

Premises used: ContinuousLinearMap.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 : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ Uᗮ ∈ invtSubmodule (↑T : E →ₗ[𝕜] E) →
    Membership.mem (γ := Sublattice (Submodule 𝕜 E))
      (invtSubmodule (↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E)) U

Tactic:
simpa using orthogonal_mem_invtSubmodule (T := T.adjoint) (U := Uᗮ)

Premises used: ContinuousLinearMap.orthogonal_mem_invtSubmodule
-- 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 : CompleteSpace E
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ IsStarProjection U.starProjection

Tactic:
⟨U.isIdempotentElem_starProjection, isSelfAdjoint_starProjection U⟩

Premises used: Submodule.isIdempotentElem_starProjection, IsStarProjection.mk, isSelfAdjoint_starProjection
-- 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 : CompleteSpace E
p : E →L[𝕜] E
simp_rw :
  LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔
    ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
simp_rw₁ :
  (∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection),
      (↑p : E →ₗ[𝕜] E) = (↑(↑p : E →ₗ[𝕜] E).range.starProjection : E →ₗ[𝕜] E)) ↔
    ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
⊢ IsStarProjection p ↔ ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection

Tactic:
simp_rw [p.isStarProjection_iff_isSymmetricProjection.eq,
    LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj]

Premises used: ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection, ContinuousLinearMap.coe_inj, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, Iff.eq
-- 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 : CompleteSpace E
w : Submodule 𝕜 E
w_1 : w.HasOrthogonalProjection
⊢ IsStarProjection w.starProjection

Tactic:
simp
-- 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 : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (↑(↑hT.toSelfAdjoint : E →L[𝕜] E) : E →ₗ[𝕜] E) = T

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 : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ Eq (α := E) (((↑(↑hT.toSelfAdjoint : E →L[𝕜] E) : E →ₜ+ E) : (a : E) → E) x : E) ((T : (a : E) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := F →L[𝕜] E)
    (((toContinuousLinearMap : (F →ₗ[𝕜] E) ≃ₗ[𝕜] F →L[𝕜] E) : (a : F →ₗ[𝕜] E) → F →L[𝕜] E)
        ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) :
      F →L[𝕜] E)
    ((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
        (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
      F →L[𝕜] E)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- 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
⊢ Eq (α := F →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E)
    ((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
            (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A)) :
        F →ₗ[𝕜] E) :
      F →ₗ[𝕜] E)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ CompleteSpace E

Tactic:
have := FiniteDimensional.complete 𝕜 E
-- 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
this : CompleteSpace E
⊢ CompleteSpace F

Tactic:
have := FiniteDimensional.complete 𝕜 F
-- 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
this_1 : CompleteSpace E
this : CompleteSpace F
rw :
  ⟪((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y,
      x⟫_𝕜 =
    ⟪y,
      ((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x⟫_𝕜
⊢ ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜

Tactic:
rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]

Premises used: LinearMap.adjoint_eq_toCLM_adjoint, LinearMap.coe_toContinuousLinearMap
-- 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
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y,
      x⟫_𝕜 =
    ⟪y,
      ((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x⟫_𝕜

Tactic:
ContinuousLinearMap.adjoint_inner_left _ x y

Premises used: ContinuousLinearMap.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
A : E →ₗ[𝕜] F
x : E
y : F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y,
      x⟫_𝕜 =
    ⟪y,
      ((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x⟫_𝕜

Tactic:
exact ContinuousLinearMap.adjoint_inner_left _ x y

Premises used: ContinuousLinearMap.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
A : E →ₗ[𝕜] F
x : E
y : F
this_1 : CompleteSpace E
this : CompleteSpace F
rw :
  ⟪x,
      ((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y⟫_𝕜 =
    ⟪((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x,
      y⟫_𝕜
⊢ ⟪x, (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜

Tactic:
rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]

Premises used: LinearMap.adjoint_eq_toCLM_adjoint, LinearMap.coe_toContinuousLinearMap
-- 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
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x,
      ((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y⟫_𝕜 =
    ⟪((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x,
      y⟫_𝕜

Tactic:
ContinuousLinearMap.adjoint_inner_right _ x y

Premises used: ContinuousLinearMap.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
A : E →ₗ[𝕜] F
x : E
y : F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x,
      ((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
                (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                  (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                    E →ₗ[𝕜] F))) :
            F →ₗ[𝕜] E) :
          (a : F) → E)
        y⟫_𝕜 =
    ⟪((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
          (a : E) → F)
        x,
      y⟫_𝕜

Tactic:
exact ContinuousLinearMap.adjoint_inner_right _ x y

Premises used: ContinuousLinearMap.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
A : E →ₗ[𝕜] F
h :
  ∀ (v : E),
    Eq.{u_3 + 1} (α := F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
          v :
        F)
      ((A : (a : E) → F) v : F)
⊢ (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) = A

Tactic:
ext v
-- 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
v : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v :
      F)
    ((A : (a : E) → F) v : F)

Tactic:
ext_inner_left 𝕜 fun w => ?_

Premises used: ext_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
A : E →ₗ[𝕜] F
v : E
h :
  ∀ (w : F),
    ⟪w,
        (((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) :
            (a : E) → F)
          v⟫_𝕜 =
      ⟪w, (A : (a : E) → F) v⟫_𝕜
⊢ Eq.{u_3 + 1} (α := F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v :
      F)
    ((A : (a : E) → F) v : F)

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Premises used: ext_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
A : E →ₗ[𝕜] F
v : E
w : F
h : ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) w, v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
h₁ h₂ : ⟪w, (A : (a : E) → F) v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
⊢ ⟪w,
      (((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜

Tactic:
rw [adjoint_inner_right, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_right, LinearMap.adjoint_inner_left
-- 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
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
h :
  ∀ (v : G),
    Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v : E)
      (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v : E)
⊢ Eq (α := G →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E)
    ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : G →ₗ[𝕜] E)

Tactic:
ext v
-- 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
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v : E)
    (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v : E)

Tactic:
ext_inner_left 𝕜 fun w => ?_

Premises used: ext_inner_left
-- 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
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
h :
  ∀ (w : E),
    ⟪w, (((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v⟫_𝕜 =
      ⟪w, ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v⟫_𝕜
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v : E)
    (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v : E)

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Premises used: ext_inner_left
-- 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
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
w : E
⊢ ⟪w, (((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v⟫_𝕜 =
    ⟪w, ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v⟫_𝕜

Tactic:
simp only [adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply]

Premises used: LinearMap.adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply
-- 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
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : E
y : F
rw : ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
rw₁ rw₂ : ⟪x, (B : (a : F) → E) y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜

Tactic:
rw [h, 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
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
refine :
  ∀ (h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜),
    A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- 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
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
h₁ :
  ∀ (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)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B

Tactic:
ext x
-- 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
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
x : E
y : F
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x, y⟫_𝕜

Tactic:
simp only [adjoint_inner_left, h x y]

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
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
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 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

Premises used: ext_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
A : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
rwa : A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (x y : E), ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
⊢ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A

Tactic:
rwa [eq_comm, eq_adjoint_iff A A]

Premises used: eq_comm, LinearMap.eq_adjoint_iff