𝕜 : Type ?u.285201
E : Type ?u.285204
F : Type ?u.285207
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ ((∀ (v : E'), ↑(↑re (inner (↑↑T v) v)) = inner (↑↑T v) v) ∧ ∀ (x : E'), 0 ≤ reApplyInnerSelf T x) ↔
    (∀ (x : E'), ↑(↑re (inner (↑T x) x)) = inner (↑T x) x) ∧ ∀ (x : E'), 0 ≤ ↑re (inner (↑T x) x)
𝕜 : Type ?u.285201
E : Type ?u.285204
F : Type ?u.285207
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ IsPositive T ↔ ∀ (x : E'), ↑(↑re (inner (↑T x) x)) = inner (↑T x) x ∧ 0 ≤ ↑re (inner (↑T x) x)
simp_rw [IsPositive, forall_and, isSelfAdjoint_iff_isSymmetric,
  LinearMap.isSymmetric_iff_inner_map_self_real, conj_eq_iff_re]
no goals
𝕜 : Type ?u.285201
E : Type ?u.285204
F : Type ?u.285207
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ ((∀ (v : E'), ↑(↑re (inner (↑↑T v) v)) = inner (↑↑T v) v) ∧ ∀ (x : E'), 0 ≤ reApplyInnerSelf T x) ↔
    (∀ (x : E'), ↑(↑re (inner (↑T x) x)) = inner (↑T x) x) ∧ ∀ (x : E'), 0 ≤ ↑re (inner (↑T x) x)
rfl