awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h :
  ∀ (a : ℝ), HSMul.hSMul (β := H) a ((ContinuousLinearEquiv.symm (scalarSMulCLE H UnitI) : (a : H) → H) x : H) ∈ S.mulI
⊢ x ∈ S

Tactic:
simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

Premises used: smul_assoc, Units.smul_def, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : x ∈ S
⊢ ∀ (a : ℝ), a • x ∈ S

Tactic:
rw [← SetLike.forall_smul_mem_iff] at h

Premises used: SetLike.forall_smul_mem_iff
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : ∀ (a : ℝ), a • x ∈ S
⊢ x ∈ S.mulI.mulI

Tactic:
simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

Premises used: smul_assoc, Units.smul_def, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ Function.Involutive.{u_1 + 1} (α := ClosedSubmodule ℝ H) mulI

Tactic:
mulI_mulI_eq

Premises used: Function.Involutive, ClosedSubmodule.mulI_mulI_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst_1 : CompleteSpace H
S : ClosedSubmodule ℝ H
⊢ S.symplComp.symplComp = S

Tactic:
simp [symplComp]

Premises used: ClosedSubmodule.symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
rw : (mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊔ T) = S.mulI ⊔ T.mulI
rw₁ rw₂ :
  Eq (α := ClosedSubmodule ℝ H)
    ((mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊔ T) : ClosedSubmodule ℝ H)
    ((mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊔ T) : ClosedSubmodule ℝ H)
⊢ (S ⊔ T).mulI = S.mulI ⊔ T.mulI

Tactic:
rw [mulI, ← mapEquiv_sup_eq]

Premises used: ClosedSubmodule.mapEquiv_sup_eq, ClosedSubmodule.mulI
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
rw : (mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊓ T) = S.mulI ⊓ T.mulI
rw₁ rw₂ :
  Eq (α := ClosedSubmodule ℝ H)
    ((mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊓ T) : ClosedSubmodule ℝ H)
    ((mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊓ T) : ClosedSubmodule ℝ H)
⊢ (S ⊓ T).mulI = S.mulI ⊓ T.mulI

Tactic:
rw [mulI, ← mapEquiv_inf_eq]

Premises used: ClosedSubmodule.mulI, ClosedSubmodule.mapEquiv_inf_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
rw : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊔ T.mulI)ᗮ (S.mulIᗮ ⊓ T.mulIᗮ)
⊢ (S ⊔ T).symplComp = S.symplComp ⊓ T.symplComp

Tactic:
rw [symplComp, symplComp, symplComp, mulI_sup]

Premises used: ClosedSubmodule.mulI_sup, ClosedSubmodule.symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊔ T.mulI)ᗮ (S.mulIᗮ ⊓ T.mulIᗮ)

Tactic:
Eq.symm (inf_orthogonal S.mulI T.mulI)

Premises used: ClosedSubmodule.inf_orthogonal, ClosedSubmodule.mulI, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊔ T.mulI)ᗮ (S.mulIᗮ ⊓ T.mulIᗮ)

Tactic:
exact Eq.symm (inf_orthogonal S.mulI T.mulI)

Premises used: ClosedSubmodule.inf_orthogonal, ClosedSubmodule.mulI, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst_1 : CompleteSpace H
S T : ClosedSubmodule ℝ H
rw : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊓ T.mulI)ᗮ (S.mulIᗮ ⊔ T.mulIᗮ)
⊢ (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp

Tactic:
rw [symplComp, symplComp, symplComp, mulI_inf]

Premises used: ClosedSubmodule.mulI_inf, ClosedSubmodule.symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst_1 : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊓ T.mulI)ᗮ (S.mulIᗮ ⊔ T.mulIᗮ)

Tactic:
Eq.symm (sup_orthogonal S.mulI T.mulI)

Premises used: ClosedSubmodule.mulI, ClosedSubmodule.sup_orthogonal, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst_1 : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊓ T.mulI)ᗮ (S.mulIᗮ ⊔ T.mulIᗮ)

Tactic:
exact Eq.symm (sup_orthogonal S.mulI T.mulI)

Premises used: ClosedSubmodule.mulI, ClosedSubmodule.sup_orthogonal, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
S T : StandardSubspace H
⊢ S.toClosedSubmodule = T.toClosedSubmodule ↔ S = T

Tactic:
StandardSubspace.ext_iff.symm

Premises used: StandardSubspace.ext_iff, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := StandardSubspace H) toClosedSubmodule

Tactic:
fun _ _ ↦ toClosedSubmodule_inj.mp

Premises used: StandardSubspace.toClosedSubmodule_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
S : StandardSubspace H
⊢ S.toClosedSubmodule.mulI ⊓ S.toClosedSubmodule.mulI.mulI = ⊥

Tactic:
simpa [mulI_mulI_eq, inf_comm] using S.IsSeparating

Premises used: StandardSubspace.IsSeparating, inf_comm, ClosedSubmodule.mulI_mulI_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
S : StandardSubspace H
⊢ S.toClosedSubmodule.mulI ⊔ S.toClosedSubmodule.mulI.mulI = ⊤

Tactic:
simpa [mulI_mulI_eq, sup_comm] using S.IsCyclic

Premises used: StandardSubspace.IsCyclic, sup_comm, ClosedSubmodule.mulI_mulI_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : StandardSubspace H
⊢ S.toClosedSubmodule.symplComp ⊓ S.toClosedSubmodule.symplComp.mulI = ⊥

Tactic:
simp [mulI_symplComp, ClosedSubmodule.inf_orthogonal, sup_comm, S.IsCyclic]

Premises used: ClosedSubmodule.inf_orthogonal, StandardSubspace.IsCyclic, sup_comm, ClosedSubmodule.mulI_symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : StandardSubspace H
⊢ S.toClosedSubmodule.symplComp ⊔ S.toClosedSubmodule.symplComp.mulI = ⊤

Tactic:
simp [mulI_symplComp, ClosedSubmodule.sup_orthogonal, inf_comm, S.IsSeparating]

Premises used: StandardSubspace.IsSeparating, ClosedSubmodule.sup_orthogonal, inf_comm, ClosedSubmodule.mulI_symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : StandardSubspace H
⊢ S.symplComp.symplComp = S

Tactic:
toClosedSubmodule_inj.mp ClosedSubmodule.symplComp_symplComp_eq

Premises used: StandardSubspace.toClosedSubmodule_inj, Iff.mp, ClosedSubmodule.symplComp_symplComp_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
⊢ Function.Involutive.{u_1 + 1} (α := StandardSubspace H) symplComp

Tactic:
symplComp_symplComp_eq

Premises used: StandardSubspace.symplComp_symplComp_eq, Function.Involutive
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
rw : ∀ x ∈ spectrum ℝ f, 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) f (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [SpectrumRestricts.nnreal_iff]

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c ∈ spectrum ℝ f
contrapose! : ∀ (hc : c < 0), c ∉ spectrum ℝ f
⊢ 0 ≤ c

Tactic:
contrapose! hc
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c < 0
rw : IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) (-c) : H →L[𝕜] H))
⊢ c ∉ spectrum ℝ f

Tactic:
rw [spectrum.notMem_iff, IsUnit.sub_iff, sub_eq_add_neg, ← map_neg]

Premises used: sub_eq_add_neg, IsUnit.sub_iff, map_neg, spectrum.notMem_iff
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c < 0
⊢ 0 < -c

Tactic:
rw [← neg_pos] at hc

Premises used: neg_pos
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : 0 < -c
set :
  let c := -c;
  ∀ (hc : 0 < c), IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H))
⊢ IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) (-c) : H →L[𝕜] H))

Tactic:
set c := -c
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c_1 : ℝ
c : ℝ := -c_1
hc : 0 < c
x : H
rw : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪(HSMul.hSMul (β := H →L[𝕜] H) c 1 : (a : H) → H) x, x⟫_𝕜
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪(HSMul.hSMul (α := 𝕜) (β := H →L[𝕜] H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) 1 : (a : H) → H) x, x⟫_𝕜
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪HSMul.hSMul (α := 𝕜) (β := (a : H) → H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) (⇑1 : (a : H) → H) x, x⟫_𝕜
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪HSMul.hSMul (α := 𝕜) (β := H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) ((1 : (a : H) → H) x : H), x⟫_𝕜
rw₄ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) x, x⟫_𝕜
rw₅ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) : 𝕜) ⟪x, x⟫_𝕜)
rw₆ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑c : 𝕜) : 𝕜) ⟪x, x⟫_𝕜)
rw₇ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ((↑c : 𝕜) * ⟪x, x⟫_𝕜)
rw₈ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
rw₉ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = c * HPow.hPow (β := ℕ) ‖x‖ 2
rw₁₀ rw₁₁ : c * HPow.hPow (β := ℕ) ‖x‖ 2 = c * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), coe_smul',
        Pi.smul_apply, one_apply, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal,
        re_ofReal_mul, inner_self_eq_norm_sq, mul_comm]

Premises used: RCLike.algebraMap_eq_ofReal, ContinuousLinearMap.coe_smul', RCLike.conj_ofReal, algebraMap_smul, ContinuousLinearMap.one_apply, inner_self_eq_norm_sq, Algebra.algebraMap_eq_smul_one, mul_comm, RCLike.re_ofReal_mul, OfNat.ofNat, inner_smul_left, Pi.smul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c_1 : ℝ
c : ℝ := -c_1
hc : 0 < c
x : H
⊢ LE.le (α := ℝ)
    ((re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪(HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H)
            x,
          x⟫_𝕜 :
      ℝ)

Tactic:
simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
        using hf.re_inner_nonneg_left x

Premises used: map_add, ContinuousLinearMap.add_apply, inner_add_left, ContinuousLinearMap.IsPositive.re_inner_nonneg_left, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c_1 : ℝ
c : ℝ := -c_1
hc : 0 < c
⊢ IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H))

Tactic:
exact isUnit_of_forall_le_norm_inner_map _ (c := ⟨c, hc.le⟩) hc fun x ↦ calc
    ‖x‖ ^ 2 * c = re ⟪algebraMap ℝ (H →L[𝕜] H) c x, x⟫_𝕜 := by
      rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), coe_smul',
        Pi.smul_apply, one_apply, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal,
        re_ofReal_mul, inner_self_eq_norm_sq, mul_comm]
    _ ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 := by
      simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
        using hf.re_inner_nonneg_left x
    _ ≤ ‖⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜‖ := RCLike.re_le_norm _

Premises used: Real, Trans.trans, Algebra.algebraMap, Inner.inner, ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map, ContinuousLinearMap, HAdd.hAdd, RCLike.re_le_norm, RingHom.id, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
mp :
  f ≤ g →
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p
mpr :
  (∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p) →
    f ≤ g
⊢ f ≤ g ↔
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : f ≤ g
⊢ (g - f).IsPositive

Tactic:
rw [le_def] at h

Premises used: ContinuousLinearMap.le_def
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
mp :
  ∀ (p : H →L[𝕜] H) (hp₁ : IsSelfAdjoint p) (hp₃ : p * p = g - f),
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p
⊢ ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p

Tactic:
obtain ⟨p, hp₁, -, hp₃⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts
        h.isSelfAdjoint h.spectrumRestricts

Premises used: CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, ContinuousLinearMap.IsPositive.spectrumRestricts, ContinuousLinearMap.IsPositive.isSelfAdjoint
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
symm : f + HPow.hPow (β := ℕ) p 2 = g
⊢ g = f + HPow.hPow (β := ℕ) p 2

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
rwa : HPow.hPow (β := ℕ) p 2 + f = g
rwa₁ rwa₂ rwa₃ rwa₄ : HPow.hPow (β := ℕ) p 2 = g - f
⊢ f + HPow.hPow (β := ℕ) p 2 = g

Tactic:
rwa [add_comm, ← eq_sub_iff_add_eq]

Premises used: eq_sub_iff_add_eq, add_comm
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
mp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
    (HPow.hPow (β := ℕ) p 2)
⊢ ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p

Tactic:
refine ⟨p ^ 2, ?_, by symm; rwa [add_comm, ← eq_sub_iff_add_eq]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ (fun (s : H →L[𝕜] H) ↦ star s * s) p = HPow.hPow (β := ℕ) p 2

Tactic:
simp only [hp₁.star_eq, sq]

Premises used: sq, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
    (HPow.hPow (β := ℕ) p 2)

Tactic:
exact AddSubmonoid.subset_closure ⟨p, by simp only [hp₁.star_eq, sq]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
mpr : p.IsPositive
⊢ f ≤ f + p

Tactic:
rw [le_def, add_sub_cancel_left]

Premises used: add_sub_cancel_left, ContinuousLinearMap.le_def
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p x : H →L[𝕜] H
hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x
mpr : ∀ (f : H →L[𝕜] H), IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) ((fun (s : H →L[𝕜] H) ↦ star s * s) f)
⊢ x.IsPositive

Tactic:
obtain ⟨f, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f_1 p f : H →L[𝕜] H
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) ((fun (s : H →L[𝕜] H) ↦ star s * s) f)

Tactic:
simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f

Premises used: ContinuousLinearMap.IsPositive.adjoint_conj, ContinuousLinearMap.isPositive_one
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) 0

Tactic:
isPositive_zero

Premises used: ContinuousLinearMap.isPositive_zero
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) 0

Tactic:
exact isPositive_zero

Premises used: ContinuousLinearMap.isPositive_zero