awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
rw : mulI S.mulIᗮ = S.mulI.symplComp
⊢ S.symplComp.mulI = S.mulI.symplComp
have rw₁ : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (mulI S.mulIᗮ) S.mulI.mulIᗮ
Tactic: rw [symplComp, symplComp, mulI_orthogonal_eq_symplComp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
rw : mulI S.mulIᗮ = S.mulI.symplComp
rw₁ : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (mulI S.mulIᗮ) S.mulI.mulIᗮ
⊢ S.symplComp.mulI = S.mulI.symplComp
have rw₂ : S.mulI.symplComp = S.mulI.mulIᗮ
Tactic: rw [symplComp, symplComp, mulI_orthogonal_eq_symplComp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulI.mulI = S
have carrier : ∀ (x : H), x ∈ (↑S.mulI.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S : Submodule ℝ H).carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S.mulI.mulI ↔ x ∈ S
have carrier : x ∈ S.mulI.mulI → x ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
carrier : x ∈ S.mulI.mulI → x ∈ S
⊢ x ∈ S.mulI.mulI ↔ x ∈ S
have carrier₁ : x ∈ S → x ∈ S.mulI.mulI
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (hypothesis)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : x ∈ S.mulI.mulI
⊢ x ∈ S
have h₁ : ∀ (a : ℝ), HSMul.hSMul (β := H) a ((ContinuousLinearEquiv.symm (scalarSMulCLE H UnitI) : (a : H) → H) x : H) ∈ S.mulI
Tactic: rw [mem_mapEquiv_iff (scalarSMulCLE H UnitI), ← SetLike.forall_smul_mem_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (hypothesis)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : x ∈ S
⊢ x ∈ S.mulI.mulI
have h₁ : ∀ (a : ℝ), a • x ∈ S
Tactic: rw [← SetLike.forall_smul_mem_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulI = S.mulI ⊔ T.mulI
have rw : (mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊔ T) = S.mulI ⊔ T.mulI
Tactic: rw [mulI, ← mapEquiv_sup_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
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
⊢ (S ⊔ T).mulI = S.mulI ⊔ T.mulI
have 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)
Tactic: rw [mulI, ← mapEquiv_sup_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).mulI = S.mulI ⊓ T.mulI
have rw : (mapEquiv (scalarSMulCLE H UnitI) : (a : ClosedSubmodule ℝ H) → ClosedSubmodule ℝ H) (S ⊓ T) = S.mulI ⊓ T.mulI
Tactic: rw [mulI, ← mapEquiv_inf_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
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
⊢ (S ⊓ T).mulI = S.mulI ⊓ T.mulI
have 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)
Tactic: rw [mulI, ← mapEquiv_inf_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).symplComp = S.symplComp ⊓ T.symplComp
have rw : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊔ T.mulI)ᗮ (S.mulIᗮ ⊓ T.mulIᗮ)
Tactic: rw [symplComp, symplComp, symplComp, mulI_sup]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst_1 : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp
have rw : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (S.mulI ⊓ T.mulI)ᗮ (S.mulIᗮ ⊔ T.mulIᗮ)
Tactic: rw [symplComp, symplComp, symplComp, mulI_inf]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) f (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have rw : ∀ x ∈ spectrum ℝ f, 0 ≤ x
Tactic: rw [SpectrumRestricts.nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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
⊢ 0 ≤ c
have contrapose! : ∀ (hc : c < 0), c ∉ spectrum ℝ f
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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
⊢ c ∉ spectrum ℝ f
have rw : IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) (-c) : H →L[𝕜] H))
Tactic: rw [spectrum.notMem_iff, IsUnit.sub_iff, sub_eq_add_neg, ← map_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (hypothesis)
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
⊢ IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) (-c) : H →L[𝕜] H))
have hc₁ : 0 < -c
Tactic: rw [← neg_pos] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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
⊢ IsUnit (HAdd.hAdd (β := H →L[𝕜] H) f ((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) (-c) : H →L[𝕜] H))
have 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))
Tactic: set c := -c
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪(HSMul.hSMul (β := H →L[𝕜] H) c 1 : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 * c =
  (re : (a : 𝕜) → ℝ)
    ⟪(HSMul.hSMul (α := 𝕜) (β := H →L[𝕜] H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) 1 : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 * c =
  (re : (a : 𝕜) → ℝ)
    ⟪HSMul.hSMul (α := 𝕜) (β := (a : H) → H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) (⇑1 : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 * c =
  (re : (a : 𝕜) → ℝ)
    ⟪HSMul.hSMul (α := 𝕜) (β := H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) ((1 : (a : H) → H) x : H), 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₄ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₅ : HPow.hPow (β := ℕ) ‖x‖ 2 * c =
  (re : (a : 𝕜) → ℝ)
    (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) : 𝕜) ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₆ : HPow.hPow (β := ℕ) ‖x‖ 2 * c =
  (re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑c : 𝕜) : 𝕜) ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₇ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ((↑c : 𝕜) * ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₈ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
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⟫_𝕜 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₉ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = c * HPow.hPow (β := ℕ) ‖x‖ 2
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]