awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ StarModule.{u_1, u_2} 𝕜 (E →L[𝕜] E)

Tactic:
⟨map_smulₛₗ adjoint⟩

Premises used: MulActionSemiHomClass.map_smulₛₗ, StarModule.mk, ContinuousLinearMap.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 : CompleteSpace E
A : E →L[𝕜] E
⊢ star A = (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] 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 : CompleteSpace E
A : E →L[𝕜] E
⊢ IsSelfAdjoint A ↔ (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] 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 : CompleteSpace E
⊢ Membership.mem (γ := Submonoid (E →L[𝕜] E)) (unitary (E →L[𝕜] E)) (ContinuousLinearMap.id 𝕜 E)

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 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = ‖A‖ * ‖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 := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤ ‖A‖ * ‖A‖
refine_2 : ‖A‖ * ‖A‖ ≤ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)
⊢ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = ‖A‖ * ‖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 := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤
    norm (E := F →L[𝕜] E) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖A‖

Tactic:
opNorm_comp_le _ _

Premises used: ContinuousLinearMap.opNorm_comp_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
rw rw₁ : ‖A‖ * ‖A‖ = ‖A‖ * ‖A‖
⊢ norm (E := F →L[𝕜] E) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖A‖ = ‖A‖ * ‖A‖

Tactic:
rw [LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map
-- 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
opNorm_comp_le : norm (E := F →L[𝕜] E) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖A‖ = ‖A‖ * ‖A‖
⊢ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤ ‖A‖ * ‖A‖

Tactic:
calc
      ‖A† ∘L A‖ ≤ ‖A†‖ * ‖A‖ := opNorm_comp_le _ _
      _ = ‖A‖ * ‖A‖ := by rw [LinearIsometryEquiv.norm_map]

Premises used: ContinuousLinearMap.opNorm_comp_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 : ‖A‖ ≤ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A))
⊢ ‖A‖ * ‖A‖ ≤ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)

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

Premises used: Real.sqrt_le_sqrt_iff, sq, 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
⊢ ‖A‖ ≤ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A))

Tactic:
opNorm_le_bound _ (Real.sqrt_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, Real.sqrt_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) ((A : (a : E) → F) x : F) ≤
      √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
⊢ ‖A‖ ≤ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A))

Tactic:
refine opNorm_le_bound _ (Real.sqrt_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, Real.sqrt_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
hbc :
  norm (E := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖
⊢ norm (E := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) * ‖x‖ ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖

Tactic:
gcongr
-- 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 := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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 := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖

Tactic:
exact le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
⊢ (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖

Tactic:
have :=
      calc
        re ⟪(A† ∘L A) x, x⟫ ≤ ‖(A† ∘L A) x‖ * ‖x‖ := re_inner_le_norm _ _
        _ ≤ ‖A† ∘L A‖ * ‖x‖ * ‖x‖ := by gcongr; exact le_opNorm _ _
-- 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
this :
  (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
rw rw₁ :
  √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜) =
    √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜)
⊢ 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_eq_sqrt_inner_adjoint_left]

Premises used: ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_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
this :
  (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
⊢ √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜) ≤
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖)

Tactic:
Real.sqrt_le_sqrt this

Premises used: Real.sqrt_le_sqrt
-- 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
this :
  (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
simp_rw :
  √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * (‖x‖ * ‖x‖)) =
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
simp_rw₁ :
  √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * √(‖x‖ * ‖x‖) =
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
⊢ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖) =
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖

Tactic:
simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]

Premises used: Norm.norm, HMul.hMul, mul_assoc, Real.sqrt_mul_self, Real.sqrt_mul, 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
this :
  (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
by :
  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⟫_𝕜)
by₁ :
  √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖) =
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) ≤
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖

Tactic:
calc
      ‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫) := by rw [apply_norm_eq_sqrt_inner_adjoint_left]
      _ ≤ √(‖A† ∘L A‖ * ‖x‖ * ‖x‖) := Real.sqrt_le_sqrt this
      _ = √‖A† ∘L A‖ * ‖x‖ := by
        simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]

Premises used: ContinuousLinearMap.comp, Norm.norm, HMul.hMul, Real.sqrt_le_sqrt, ContinuousLinearMap.adjoint, DFunLike.coe
-- 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
rw : norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = 0 ↔ A = 0
⊢ Eq (α := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) 0 ↔ A = 0

Tactic:
rw [← norm_eq_zero]

Premises used: norm_eq_zero
-- 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[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = 0 ↔ A = 0

Tactic:
simp [norm_adjoint_comp_self]

Premises used: ContinuousLinearMap.norm_adjoint_comp_self
-- 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
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((LinearMap.flip (innerₛₗ 𝕜) : (a : F) → F →ₗ⋆[𝕜] 𝕜) ((A : (a : E) → F) x) : F →ₗ⋆[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
    ((((LinearMap.flip (innerₛₗ 𝕜) : (a : E) → E →ₗ⋆[𝕜] 𝕜) x : E →ₗ⋆[𝕜] 𝕜) : (a : E) → 𝕜)
        ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) y : E) :
      𝕜)

Tactic:
simp [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
x x_1 : E
⊢ ⟪x_1,
      (((adjoint : (a : E →L[𝕜] 𝕜) → 𝕜 →L[𝕜] E) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1⟫_𝕜 =
    ⟪x_1, (toSpanSingleton 𝕜 x : (a : 𝕜) → E) 1⟫_𝕜

Tactic:
simp [adjoint_inner_right]

Premises used: ContinuousLinearMap.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 : CompleteSpace E
x : E
⊢ Eq (α := E →L[𝕜] 𝕜) ((adjoint : (a : 𝕜 →L[𝕜] E) → E →L[𝕜] 𝕜) (toSpanSingleton 𝕜 x) : E →L[𝕜] 𝕜)
    ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)

Tactic:
simp [← adjoint_innerSL_apply]

Premises used: ContinuousLinearMap.adjoint_innerSL_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
x : F
f : E →L[𝕜] F
h :
  ∀ (x_1 : E),
    Eq.{u_1 + 1} (α := 𝕜) ((comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x) f : (a : E) → 𝕜) x_1 : 𝕜)
      ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) f : F →L[𝕜] E) : (a : F) → E) x) :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x_1 :
        𝕜)
⊢ Eq (α := E →L[𝕜] 𝕜) (comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x) f)
    ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) f : F →L[𝕜] E) : (a : F) → E) x))

Tactic:
ext
-- 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
x : F
f : E →L[𝕜] F
x_1 : E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x) f : (a : E) → 𝕜) x_1 : 𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) f : F →L[𝕜] E) : (a : F) → E) x) :
            E →L[𝕜] 𝕜) :
          (a : E) → 𝕜)
        x_1 :
      𝕜)

Tactic:
simp [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
x : E
f : E →L[𝕜] E
hf : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑f : E →ₗ[𝕜] E)
h :
  ∀ (x_1 : E),
    Eq.{u_1 + 1} (α := 𝕜) ((comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x) f : (a : E) → 𝕜) x_1 : 𝕜)
      ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((f : (a : E) → E) x) : E →L[𝕜] 𝕜) : (a : E) → 𝕜) x_1 : 𝕜)
⊢ Eq (α := E →L[𝕜] 𝕜) (comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x) f)
    ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((f : (a : E) → E) x))

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑f : E →ₗ[𝕜] E)
x_1 : E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x) f : (a : E) → 𝕜) x_1 : 𝕜)
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((f : (a : E) → E) x) : E →L[𝕜] 𝕜) : (a : E) → 𝕜) x_1 : 𝕜)

Tactic:
simp [hf]
-- 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
x : E
y : F
⊢ Eq (α := E →L[𝕜] F)
    ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F)
        ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) :
      E →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → E →L⋆[𝕜] E →L[𝕜] F) y : E →L⋆[𝕜] E →L[𝕜] F) : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F)

Tactic:
simp [rankOne_def', adjoint_comp, ← adjoint_innerSL_apply]

Premises used: InnerProductSpace.rankOne_def', ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_innerSL_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
E : Type u_5
G : Type u_6
inst_4 : SeminormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup G
inst_7 : InnerProductSpace 𝕜 G
inst_8 : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
simp_rw :
  Eq (α := G →L[𝕜] E) (comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) ∘SL f)
    (comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x)
      ((innerSL 𝕜 : (a : G) → G →L[𝕜] 𝕜) ((((adjoint : (a : G →L[𝕜] F) → F →L[𝕜] G) f : F →L[𝕜] G) : (a : F) → G) y)))
simp_rw₁ :
  Eq (α := G →L[𝕜] E) (toSpanSingleton 𝕜 x ∘SL comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) f)
    (comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x)
      ((innerSL 𝕜 : (a : G) → G →L[𝕜] 𝕜) ((((adjoint : (a : G →L[𝕜] F) → F →L[𝕜] G) f : F →L[𝕜] G) : (a : F) → G) y)))
⊢ Eq (α := G →L[𝕜] E)
    (comp (σ₂₃ := RingHom.id 𝕜)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) f)
    ((((rankOne 𝕜 : (a : E) → G →L⋆[𝕜] G →L[𝕜] E) x : G →L⋆[𝕜] G →L[𝕜] E) : (a : G) → G →L[𝕜] E)
      ((((adjoint : (a : G →L[𝕜] F) → F →L[𝕜] G) f : F →L[𝕜] G) : (a : F) → G) y))

Tactic:
simp_rw [rankOne_def', comp_assoc, innerSL_apply_comp]

Premises used: InnerProductSpace.rankOne_def', ContinuousLinearMap.comp_assoc, ContinuousLinearMap.innerSL_apply_comp
-- 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
A : E →L[𝕜] E
hA : IsSelfAdjoint A
⊢ (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A = A

Tactic:
hA

Premises used: IsSelfAdjoint
-- 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
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x y : E
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
rw_mod_cast₆ :
  ⟪x, (((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A : E →L[𝕜] E) : (a : E) → E) y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
⊢ ⟪((↑A : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫_𝕜 = ⟪x, ((↑A : E →ₗ[𝕜] E) : (a : E) → E) y⟫_𝕜

Tactic:
rw_mod_cast [← A.adjoint_inner_right, hA.adjoint_eq]

Premises used: IsSelfAdjoint.adjoint_eq, 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
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : E →L[𝕜] F
rw :
  ∀ (hT : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T) (S : E →L[𝕜] F),
    Eq (α := F →L[𝕜] F)
      ((adjoint : (a : F →L[𝕜] F) → F →L[𝕜] F)
          (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S)) :
        F →L[𝕜] F)
      (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) : F →L[𝕜] F)
⊢ IsSelfAdjoint (R := F →L[𝕜] F) (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))

Tactic:
rw [isSelfAdjoint_iff'] at hT ⊢

Premises used: ContinuousLinearMap.isSelfAdjoint_iff'