awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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‖
⊢ 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⟫_𝕜)
have 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⟫_𝕜)
Tactic: rw [apply_norm_eq_sqrt_inner_adjoint_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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‖
⊢ √(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‖
have 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‖
Tactic: simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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‖
⊢ √(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‖
have 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‖
Tactic: simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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‖
⊢ 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‖
have 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⟫_𝕜)
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)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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⟫_𝕜)
⊢ 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‖
have 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‖
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)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ Eq (α := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) 0 ↔ A = 0
have rw : norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = 0 ↔ A = 0
Tactic: rw [← norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ 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))
have 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 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ Eq (α := E →L[𝕜] 𝕜) (comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x) f)
    ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) ((f : (a : E) → E) x))
have 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 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ 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))
have 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)))
Tactic: simp_rw [rankOne_def', comp_assoc, innerSL_apply_comp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)))
⊢ 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))
have 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)))
Tactic: simp_rw [rankOne_def', comp_assoc, innerSL_apply_comp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ ⟪((↑A : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫_𝕜 = ⟪x, ((↑A : E →ₗ[𝕜] E) : (a : E) → E) y⟫_𝕜
have rw_mod_cast : ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
Tactic: rw_mod_cast [← A.adjoint_inner_right, hA.adjoint_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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⟫_𝕜
⊢ ⟪((↑A : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫_𝕜 = ⟪x, ((↑A : E →ₗ[𝕜] E) : (a : E) → E) y⟫_𝕜
have 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⟫_𝕜
Tactic: rw_mod_cast [← A.adjoint_inner_right, hA.adjoint_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ IsSelfAdjoint (R := F →L[𝕜] F) (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))
have 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)
Tactic: rw [isSelfAdjoint_iff'] at hT ⊢
Cleared hypotheses: hT, S
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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 : (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)
have simp : Eq (α := F →L[𝕜] F) ((S ∘SL T).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))
  (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))
Tactic: simp only [hT, adjoint_comp, adjoint_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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 : F →L[𝕜] E
⊢ IsSelfAdjoint (R := F →L[𝕜] F) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S))
have rw : ∀ (hT : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T) (S : F →L[𝕜] E),
  Eq (α := F →L[𝕜] F)
    ((adjoint : (a : F →L[𝕜] F) → F →L[𝕜] F)
        (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S)) :
      F →L[𝕜] F)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S) : F →L[𝕜] F)
Tactic: rw [isSelfAdjoint_iff'] at hT ⊢
Cleared hypotheses: hT, S
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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 : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
S : F →L[𝕜] E
⊢ Eq (α := F →L[𝕜] F)
    ((adjoint : (a : F →L[𝕜] F) → F →L[𝕜] F)
        (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S)) :
      F →L[𝕜] F)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S) : F →L[𝕜] F)
have simp : Eq (α := F →L[𝕜] F) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) T ∘SL S)
  (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S))
Tactic: simp only [hT, adjoint_comp, adjoint_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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 : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑A : E →ₗ[𝕜] E)
⊢ IsSelfAdjoint A
have rwa : ∀ (hA : IsSelfAdjoint A), IsSelfAdjoint A
Tactic: rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ IsSelfAdjoint (U.starProjection ∘SL T ∘SL U.starProjection)
have rw : IsSelfAdjoint (U.starProjection * T * U.starProjection)
Tactic: rw [← mul_def, ← mul_def, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ IsStarNormal T ↔
    ∀ (v : E),
      norm (E := E) ((T : (a : E) → E) v : E) =
        norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E)
have rw : star T * T - T * star T = 0 ↔
  ∀ (v : E),
    norm (E := E) ((T : (a : E) → E) v : E) =
      norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E)
Tactic: rw [isStarNormal_iff, Commute, SemiconjBy, ← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ star T * T - T * star T = 0 ↔
    ∀ (v : E),
      norm (E := E) ((T : (a : E) → E) v : E) =
        norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E)
have simp_rw : (↑(star T * T) : E →ₗ[𝕜] E) - (↑(T * star T) : E →ₗ[𝕜] E) = 0 ↔
  ∀ (v : E),
    norm (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) v : E) =
      norm (E := E) (((↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E) : (a : E) → E) v : E)
Tactic: simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, coe_sub, ← LinearMap.ext_iff, coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ (↑(star T * T) : E →ₗ[𝕜] E) - (↑(T * star T) : E →ₗ[𝕜] E) = 0 ↔
    ∀ (v : E),
      norm (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) v : E) =
        norm (E := E) (((↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E) : (a : E) → E) v : E)
have this : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E)
  ((↑(HMul.hMul (α := E →L[𝕜] E) ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) T) : E →ₗ[𝕜] E) -
    (↑(HMul.hMul (β := E →L[𝕜] E) T ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E)) : E →ₗ[𝕜] E))
Tactic: have := star_eq_adjoint T ▸ coe_sub (star _ * T) _ ▸
    ((IsSelfAdjoint.star_mul_self T).sub (IsSelfAdjoint.mul_star_self T)).isSymmetric
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
this :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E)
    ((↑(HMul.hMul (α := E →L[𝕜] E) ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) T) : E →ₗ[𝕜] E) -
      (↑(HMul.hMul (β := E →L[𝕜] E) T ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E)) : E →ₗ[𝕜] E))
⊢ (↑(star T * T) : E →ₗ[𝕜] E) - (↑(T * star T) : E →ₗ[𝕜] E) = 0 ↔
    ∀ (v : E),
      norm (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) v : E) =
        norm (E := E) (((↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E) : (a : E) → E) v : E)
have simp_rw : (∀ (x : E),
    HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2 =
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E)) : 𝕜) 2) ↔
  ∀ (v : E),
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) v : E)) 2 =
      HPow.hPow (β := ℕ) (norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E))
        2
Tactic: simp_rw [star_eq_adjoint, ← LinearMap.IsSymmetric.inner_map_self_eq_zero this,
    LinearMap.sub_apply, inner_sub_left, coe_coe, mul_apply, adjoint_inner_left,
    inner_self_eq_norm_sq_to_K, ← adjoint_inner_right T, inner_self_eq_norm_sq_to_K,
    sub_eq_zero, ← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
this :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E)
    ((↑(HMul.hMul (α := E →L[𝕜] E) ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) T) : E →ₗ[𝕜] E) -
      (↑(HMul.hMul (β := E →L[𝕜] E) T ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E)) : E →ₗ[𝕜] E))
⊢ (∀ (x : E),
      HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2 =
        HPow.hPow (α := 𝕜) (β := ℕ)
          (↑(norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E)) : 𝕜) 2) ↔
    ∀ (v : E),
      HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) v : E)) 2 =
        HPow.hPow (β := ℕ)
          (norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E)) 2
have norm_cast : (∀ (x : E),
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2 =
      HPow.hPow (β := ℕ) (norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E))
        2) ↔
  ∀ (v : E),
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) v : E)) 2 =
      HPow.hPow (β := ℕ) (norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) v : E))
        2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsStarNormal T
x : E
⊢ Eq (α := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E) (0 : E) ↔
    Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
have simp_rw : norm (E := E) ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E) = 0 ↔
  norm (E := E) ((T : (a : E) → E) x : E) = 0
Tactic: simp_rw [← norm_eq_zero (E := E), ← isStarNormal_iff_norm_eq_adjoint.mp hT]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsIdempotentElem T
h : IsSelfAdjoint T
⊢ IsStarNormal T
have rw : Commute (star T) T
Tactic: rw [isStarNormal_iff, h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsIdempotentElem T
h : IsSelfAdjoint T
rw : Commute (star T) T
⊢ IsStarNormal T
have rw₁ : Commute T T
Tactic: rw [isStarNormal_iff, h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsIdempotentElem T
⊢ IsSelfAdjoint T ↔ IsStarNormal T
have refine : ∀ (h : IsStarNormal T), IsSelfAdjoint T
Tactic: refine ⟨fun h => by rw [isStarNormal_iff, h], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ IsSelfAdjoint T
have suffices : T = star T * T
Tactic: suffices T = star T * T from this ▸ IsSelfAdjoint.star_mul_self _