awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
hh :
  ∀ {T : E →ₗ[𝕜] E} (hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T),
    (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
h2 : ‖a‖ ≤ norm (E := E) ((q : (a : E) → E) a : E)
⊢ a ∈ q.range
have obtain : ∀ (U : Submodule 𝕜 E) (w : U.HasOrthogonalProjection)
  (hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U.starProjection : E →ₗ[𝕜] E)),
  p ≤ (↑U.starProjection : E →ₗ[𝕜] E) →
    ∀ (h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((↑U.starProjection : E →ₗ[𝕜] E) - p))
      (h2 : ‖a‖ ≤ norm (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) a : E)),
      a ∈ (↑U.starProjection : E →ₗ[𝕜] E).range
Tactic: obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_coe_starProjection.mp hq
Cleared hypotheses: q, hq, h, h1, h2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
have unfold : LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
  ((if H : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 sorry.some else 0 : (a : E →ₗ[𝕜] E) → 𝕜) f :
    𝕜)
Tactic: unfold trace
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((if H : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 ⋯.some else 0 : (a : E →ₗ[𝕜] E) → 𝕜) f :
      𝕜)
have pos : ∀ (h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)),
  LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 sorry.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
pos :
  ∀ (h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)),
    LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((if H : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 ⋯.some else 0 : (a : E →ₗ[𝕜] E) → 𝕜) f :
      𝕜)
have neg : ∀ (h : ¬∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)),
  LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((0 : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := Module.Finite.of_basis h.choose_spec.some
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
have pos : LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
  ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
Tactic: simp_rw [traceAux_eq 𝕜 _ (stdOrthonormalBasis 𝕜 E).toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
have pos : LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
  ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
Tactic: classical
    simp_rw [traceAux_eq 𝕜 _ (stdOrthonormalBasis 𝕜 E).toBasis]
    exact posSemidef_toMatrix_iff (stdOrthonormalBasis 𝕜 E) |>.mpr hf |>.trace_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : T.IsPositive
S : E →L[𝕜] F
⊢ IsPositive (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))
have refine : ∀ (x : F), 0 ≤ reApplyInnerSelf (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S)) x
Tactic: refine isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ reApplyInnerSelf (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S)) x
have rw : LE.le (α := ℝ) (0 : ℝ)
  ((re : (a : 𝕜) → ℝ)
      (inner.{u_1, u_2} 𝕜 (E := E)
        ((T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) : (a : F) → E) x : E)
        ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S : F →L[𝕜] E) : (a : F) → E) x : E)) :
    ℝ)
Tactic: rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : T.IsPositive
S : F →L[𝕜] E
⊢ IsPositive (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S))
have h : S = (adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S)
Tactic: convert! hT.conj_adjoint (S†)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : T.IsPositive
S : F →L[𝕜] E
⊢ S = (adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S)
have h : S = S
Tactic: rw [adjoint_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
⊢ LinearMap.IsPositive (S ∘ₗ T ∘ₗ (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S)
have this : CompleteSpace E
Tactic: have := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
this : CompleteSpace E
⊢ LinearMap.IsPositive (S ∘ₗ T ∘ₗ (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S)
have this₁ : CompleteSpace F
Tactic: have := FiniteDimensional.complete 𝕜 F
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
⊢ LinearMap.IsPositive ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S ∘ₗ T ∘ₗ S)
have h : S = (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S)
Tactic: convert! hT.conj_adjoint S.adjoint
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (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 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
⊢ S = (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S)
have h : S = S
Tactic: rw [LinearMap.adjoint_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
⊢ (U.starProjection ∘SL T ∘SL U.starProjection).IsPositive
have simp : (∀ (x y : E),
    ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
      ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
  ∀ (x : E), 0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
Tactic: simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, coe_comp']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw : (∀ (x y : E),
    ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
        y⟫ =
      ⟪x,
        ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
  ∀ (x : E),
    0 ≤
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
        x⟫
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : E),
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          y⟫ =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          x⟫
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw₁ : (∀ (x y : E),
    inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
        (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) =
      ⟪x,
        ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
  ∀ (x : E),
    0 ≤
      inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
        (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : E),
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          y⟫ =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          x⟫
simp_rw₁ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw₂ : (∀ (x y : E),
    inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
        (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E) =
      ⟪x,
        ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
  ∀ (x : E),
    0 ≤
      inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
        (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : E),
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          y⟫ =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          x⟫
simp_rw₁ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
simp_rw₂ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw₃ : (∀ (x y : E), True) ∧
  ∀ (x : E),
    0 ≤
      ⟪x,
        ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)⟫
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : E),
      ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          y⟫ =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        ⟪((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E),
          x⟫
simp_rw₁ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
          (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
simp_rw₂ :
  (∀ (x y : E),
      inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E) =
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤
        inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
simp_rw₃ :
  (∀ (x y : E), True) ∧
    ∀ (x : E),
      0 ≤
        ⟪x,
          ((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E)
            (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)⟫
⊢ (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
have simp_rw₄ : (∀ (x y : E), True) ∧
  ∀ (x : E),
    0 ≤
      inner 𝕜 (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E)
        (((↑T : E →ₗ[𝕜] E) : (a : E) → E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) : E)
Tactic: simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := ↥U) (U.orthogonalProjection ∘SL T ∘SL U.subtypeL)
have simp : (∀ (x y : ↥U),
    ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
      ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
  ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
Tactic: simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, coe_comp']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw : (∀ (x y : ↥U),
    ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
      ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
  ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]