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

Tactic:
rw [adjointAux_inner_right, adjointAux_inner_left]

Premises used: ContinuousLinearMap.adjointAux_inner_left, ContinuousLinearMap.adjointAux_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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) = ‖A‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
refine_1 : norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖
refine_2 : ‖A‖ ≤ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) = ‖A‖

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
refine_1 :
  ∀ (x : F),
    norm.{u_2} (E := E) ((((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) x : E) ≤ ‖A‖ * ‖x‖
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : F
refine_1 :
  norm (E := StrongDual 𝕜 E)
      ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) x :
        E →L[𝕜] 𝕜) ≤
    ‖A‖ * ‖x‖
⊢ norm.{u_2} (E := E) ((((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) x : E) ≤ ‖A‖ * ‖x‖

Tactic:
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, ContinuousLinearMap.adjointAux_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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ norm (E := StrongDual 𝕜 E)
      ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) x :
        E →L[𝕜] 𝕜) ≤
    ‖A‖ * ‖x‖

Tactic:
toSesqForm_apply_norm_le

Premises used: ContinuousLinearMap.toSesqForm_apply_norm_le
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ norm (E := StrongDual 𝕜 E)
      ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) x :
        E →L[𝕜] 𝕜) ≤
    ‖A‖ * ‖x‖

Tactic:
exact toSesqForm_apply_norm_le

Premises used: ContinuousLinearMap.toSesqForm_apply_norm_le
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
refine_2 :
  norm (E := E →L[𝕜] F)
      ((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
⊢ ‖A‖ ≤ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)

Tactic:
nth_rw 1 [← adjointAux_adjointAux A]

Premises used: ContinuousLinearMap.adjointAux_adjointAux
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := E →L[𝕜] F)
      ((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
refine_2 :
  ∀ (x : E),
    norm.{u_3} (E := F)
        ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
              (a : E) → F)
            x :
          F) ≤
      norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖
⊢ norm (E := E →L[𝕜] F)
      ((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
refine_2 :
  norm (E := StrongDual 𝕜 F)
      ((((toSesqForm : (a : F →L[𝕜] E) → E →L⋆[𝕜] F →L[𝕜] 𝕜) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) :
              E →L⋆[𝕜] F →L[𝕜] 𝕜) :
            (a : E) → F →L[𝕜] 𝕜)
          x :
        F →L[𝕜] 𝕜) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖
⊢ norm.{u_3} (E := F)
      ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
            (a : E) → F)
          x :
        F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖

Tactic:
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, ContinuousLinearMap.adjointAux_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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ norm (E := StrongDual 𝕜 F)
      ((((toSesqForm : (a : F →L[𝕜] E) → E →L⋆[𝕜] F →L[𝕜] 𝕜) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) :
              E →L⋆[𝕜] F →L[𝕜] 𝕜) :
            (a : E) → F →L[𝕜] 𝕜)
          x :
        F →L[𝕜] 𝕜) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖

Tactic:
toSesqForm_apply_norm_le

Premises used: ContinuousLinearMap.toSesqForm_apply_norm_le
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ norm (E := StrongDual 𝕜 F)
      ((((toSesqForm : (a : F →L[𝕜] E) → E →L⋆[𝕜] F →L[𝕜] 𝕜) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) :
              E →L⋆[𝕜] F →L[𝕜] 𝕜) :
            (a : E) → F →L[𝕜] 𝕜)
          x :
        F →L[𝕜] 𝕜) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖

Tactic:
exact toSesqForm_apply_norm_le

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

Tactic:
adjointAux_inner_left A x y

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

Tactic:
adjointAux_inner_right A x y

Premises used: ContinuousLinearMap.adjointAux_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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) = A

Tactic:
adjointAux_adjointAux A

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.adjointAux_adjointAux
-- 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 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
h :
  ∀ (v : G),
    Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v : E)
      ((comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
              ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
            (a : G) → E)
          v :
        E)
⊢ Eq (α := G →L[𝕜] E) ((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E)
    (comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
        ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
      G →L[𝕜] 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 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v : E)
    ((comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] 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 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
h :
  ∀ (w : E),
    ⟪w, (((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v⟫_𝕜 =
      ⟪w,
        (comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
              ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
            (a : G) → E)
          v⟫_𝕜
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v : E)
    ((comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] 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 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : E
⊢ ⟪w, (((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v⟫_𝕜 =
    ⟪w,
      (comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
          (a : G) → E)
        v⟫_𝕜

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

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.adjoint_inner_right, 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
rw :
  ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F), x⟫_𝕜
⊢ ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)

Tactic:
rw [← adjoint_inner_left]

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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F), x⟫_𝕜

Tactic:
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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)

Tactic:
have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
rw :
  HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
rw₁ rw₂ :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
    ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜

Tactic:
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

Premises used: inner_self_eq_norm_sq
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
rw :
  norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √(HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2)
rw₁ rw₂ : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = norm.{u_3} (E := F) ((A : (a : E) → F) x : F)
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜)

Tactic:
rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]

Premises used: ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq, norm_nonneg
-- 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
rw :
  ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    ⟪x, (((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F)⟫_𝕜
⊢ ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)

Tactic:
rw [← adjoint_inner_right]

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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    ⟪x, (((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F)⟫_𝕜

Tactic:
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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)

Tactic:
have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; 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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
rw :
  HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
rw₁ rw₂ :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
    ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜

Tactic:
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

Premises used: inner_self_eq_norm_sq