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
T : E →L[𝕜] E
hT : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
S : E →L[𝕜] F
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))
⊢ 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:
simp only [hT, adjoint_comp, adjoint_adjoint]

Premises used: ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : 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) ((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:
ContinuousLinearMap.comp_assoc _ _ _

Premises used: ContinuousLinearMap.comp_assoc
-- 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 : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
S : E →L[𝕜] F
⊢ 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:
exact ContinuousLinearMap.comp_assoc _ _ _

Premises used: ContinuousLinearMap.comp_assoc
-- 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 : F →L[𝕜] E
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)
⊢ IsSelfAdjoint (R := F →L[𝕜] F) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S))

Tactic:
rw [isSelfAdjoint_iff'] at hT ⊢

Premises used: ContinuousLinearMap.isSelfAdjoint_iff'
-- 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 : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
S : F →L[𝕜] E
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))
⊢ 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:
simp only [hT, adjoint_comp, adjoint_adjoint]

Premises used: ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : 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) (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:
ContinuousLinearMap.comp_assoc _ _ _

Premises used: ContinuousLinearMap.comp_assoc
-- 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 : (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
S : F →L[𝕜] E
⊢ 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:
exact ContinuousLinearMap.comp_assoc _ _ _

Premises used: ContinuousLinearMap.comp_assoc
-- 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 ↔ LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑A : E →ₗ[𝕜] E)

Tactic:
⟨fun hA => hA.isSymmetric, fun hA =>
    ext fun x => ext_inner_right 𝕜 fun y => (A.adjoint_inner_left y x).symm ▸ (hA x y).symm⟩

Premises used: IsSelfAdjoint.isSymmetric, ext_inner_right, Iff.intro, ContinuousLinearMap.ext
-- 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 : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑A : E →ₗ[𝕜] E)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hA : IsSelfAdjoint A), IsSelfAdjoint A
⊢ IsSelfAdjoint A

Tactic:
rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ IsSelfAdjoint U.starProjection

Tactic:
U.starProjection_isSymmetric.isSelfAdjoint

Premises used: LinearMap.IsSymmetric.isSelfAdjoint, Submodule.starProjection_isSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
rw : IsSelfAdjoint (U.starProjection * T * U.starProjection)
⊢ IsSelfAdjoint (U.starProjection ∘SL T ∘SL U.starProjection)

Tactic:
rw [← mul_def, ← mul_def, ← mul_assoc]

Premises used: mul_assoc, ContinuousLinearMap.mul_def
-- 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
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ IsSelfAdjoint (U.starProjection * T * U.starProjection)

Tactic:
hT.conjugate_self <| isSelfAdjoint_starProjection U

Premises used: isSelfAdjoint_starProjection, IsSelfAdjoint.conjugate_self
-- 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
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst_4 : U.HasOrthogonalProjection
⊢ IsSelfAdjoint (U.starProjection * T * U.starProjection)

Tactic:
exact hT.conjugate_self <| isSelfAdjoint_starProjection U

Premises used: isSelfAdjoint_starProjection, IsSelfAdjoint.conjugate_self
-- 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
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)
⊢ 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)

Tactic:
rw [isStarNormal_iff, Commute, SemiconjBy, ← sub_eq_zero]

Premises used: sub_eq_zero, isStarNormal_iff, SemiconjBy, Commute
-- 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
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)
⊢ 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:
simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, coe_sub, ← LinearMap.ext_iff, coe_zero]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.ext_iff, ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_sub, ContinuousLinearMap.coe_zero
-- 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
⊢ 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
-- 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
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))
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
⊢ (↑(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 [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 _)]

Premises used: inner_self_eq_norm_sq_to_K, sub_eq_zero, ContinuousLinearMap.mul_apply, LinearMap.IsSymmetric.inner_map_self_eq_zero, ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.coe_coe, inner_sub_left, ContinuousLinearMap.star_eq_adjoint, LinearMap.sub_apply, ContinuousLinearMap.adjoint_inner_right, sq_eq_sq₀, norm_nonneg
-- 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
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))
norm_cast norm_cast₁ norm_cast₂ 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
⊢ (∀ (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
-- 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
hT : IsStarNormal T
x : E
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
⊢ 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)

Tactic:
simp_rw [← norm_eq_zero (E := E), ← isStarNormal_iff_norm_eq_adjoint.mp hT]

Premises used: norm_eq_zero, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, Iff.mp
-- 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
hT : IsStarNormal T
⊢ LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜) (↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E) =
    (↑T : E →ₗ[𝕜] E).ker

Tactic:
Submodule.ext hT.adjoint_apply_eq_zero_iff

Premises used: ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, Submodule.ext
-- 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
hT : IsStarNormal T
⊢ (↑T : E →ₗ[𝕜] E).rangeᗮ = (↑T : E →ₗ[𝕜] E).ker

Tactic:
T.orthogonal_range ▸ hT.ker_adjoint_eq_ker

Premises used: Eq.rec, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, ContinuousLinearMap.orthogonal_range, Eq.symm
-- 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
hT : IsIdempotentElem T
h : IsSelfAdjoint T
rw : Commute (star T) T
rw₁ rw₂ : Commute T T
⊢ IsStarNormal T

Tactic:
rw [isStarNormal_iff, h]

Premises used: isStarNormal_iff
-- 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
hT : IsIdempotentElem T
refine : ∀ (h : IsStarNormal T), IsSelfAdjoint T
⊢ IsSelfAdjoint T ↔ IsStarNormal T

Tactic:
refine ⟨fun h => by rw [isStarNormal_iff, h], fun h => ?_⟩
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
suffices : T = star T * T
⊢ IsSelfAdjoint T

Tactic:
suffices T = star T * T from this ▸ IsSelfAdjoint.star_mul_self _
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
rw : ∀ (x : E), Eq (α := E) ((T - star T * T : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
⊢ T = star T * T

Tactic:
rw [← sub_eq_zero, ContinuousLinearMap.ext_iff]

Premises used: sub_eq_zero, ContinuousLinearMap.ext_iff
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
simp_rw : ∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0
⊢ ∀ (x : E), Eq (α := E) ((T - star T * T : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)

Tactic:
simp_rw [zero_apply, ← norm_eq_zero (E := E)]

Premises used: norm_eq_zero, ContinuousLinearMap.zero_apply
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0) ↔
    ∀ (x : E),
      norm (E := E)
          ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) (1 - T) : E →L[𝕜] E) : (a : E) → E) ((T : (a : E) → E) x : E) :
            E) =
        0

Tactic:
simp [star_eq_adjoint, one_def]

Premises used: ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.one_def
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E),
      norm (E := E)
          ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) (1 - T) : E →L[𝕜] E) : (a : E) → E) ((T : (a : E) → E) x : E) :
            E) =
        0) ↔
    ∀ (x : E), norm (E := E) ((1 - T : (a : E) → E) ((T : (a : E) → E) x : E) : E) = 0

Tactic:
simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]

Premises used: IsStarNormal.one_sub, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, Iff.mp
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), norm (E := E) ((1 - T : (a : E) → E) ((T : (a : E) → E) x : E) : E) = 0) ↔
    ∀ (x : E), norm (E := E) ((T - T * T : (a : E) → E) x : E) = 0

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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), norm (E := E) ((T - T * T : (a : E) → E) x : E) = 0) ↔ T - T * T = 0

Tactic:
simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]

Premises used: norm_eq_zero, ContinuousLinearMap.ext_iff, ContinuousLinearMap.zero_apply
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ T - T * T = 0 ↔ IsIdempotentElem T

Tactic:
simp only [sub_eq_zero, IsIdempotentElem, eq_comm]

Premises used: sub_eq_zero, eq_comm, IsIdempotentElem
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0) ↔ IsIdempotentElem T

Tactic:
have :=
    calc (∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
          simp [star_eq_adjoint, one_def]
      _ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by
          simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
      _ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
      _ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
      _ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
this : (∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0) ↔ IsIdempotentElem T
⊢ ∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0

Tactic:
this.mpr hT

Premises used: Iff.mpr
-- 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
hT : IsIdempotentElem T
h : IsStarNormal T
this : (∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0) ↔ IsIdempotentElem T
⊢ ∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0

Tactic:
exact this.mpr hT

Premises used: Iff.mpr
-- 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
rw : IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)
⊢ IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T

Tactic:
rw [isStarProjection_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, isStarProjection_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
⊢ IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)

Tactic:
fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h

Premises used: ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal
-- 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
⊢ IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)

Tactic:
exact fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h

Premises used: ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal
-- 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
⊢ IsStarProjection T ↔ LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)

Tactic:
simp [isStarProjection_iff, LinearMap.isSymmetricProjection_iff,
    isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def]

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, Module.End.mul_eq_comp, ContinuousLinearMap.coe_comp, isStarProjection_iff, IsIdempotentElem, LinearMap.isSymmetricProjection_iff, ContinuousLinearMap.mul_def