awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
x : H
rw : ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
⊢ ‖x‖ ≤ (↑c⁻¹ : ℝ) * norm (E := H) ((f : (a : H) → H) x : H)

Tactic:
rw [NNReal.coe_inv, inv_mul_eq_div, le_div_iff₀ (by exact_mod_cast hc)]

Premises used: inv_mul_eq_div, NNReal.coe_inv, le_div_iff₀
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
x : H
⊢ ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖

Tactic:
simp_rw [sq, mul_assoc] at h

Premises used: mul_assoc, sq
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
pos : ∀ (hx0 : x = 0), ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
neg : ∀ (hx0 : ¬x = 0), ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
hx0 : x = 0
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)

Tactic:
simp [hx0]
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
hx0 : ¬x = 0
neg :
  LE.le (α := ℝ) ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (‖x‖ * (↑c : ℝ)) : ℝ)
    ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (norm (E := H) ((f : (a : H) → H) x : H)) : ℝ)
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)

Tactic:
apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp

Premises used: OrderIsoClass.map_le_map_iff, Iff.mpr, Norm.norm, norm_pos_iff, OrderIso.mulLeft₀, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
hx0 : ¬x = 0
⊢ LE.le (α := ℝ) ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (‖x‖ * (↑c : ℝ)) : ℝ)
    ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (norm (E := H) ((f : (a : H) → H) x : H)) : ℝ)

Tactic:
(h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le

Premises used: Eq.le, mul_comm, LE.le.trans, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
hx0 : ¬x = 0
⊢ LE.le (α := ℝ) ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (‖x‖ * (↑c : ℝ)) : ℝ)
    ((OrderIso.mulLeft₀ ‖x‖ ⋯ : (a : ℝ) → ℝ) (norm (E := H) ((f : (a : H) → H) x : H)) : ℝ)

Tactic:
exact (h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le

Premises used: Eq.le, mul_comm, LE.le.trans, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
rw :
  (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)
⊢ IsUnit f

Tactic:
rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]

Premises used: ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, ContinuousLinearMap.isUnit_iff_bijective
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
⊢ AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)

Tactic:
have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)

Tactic:
⟨?_, ⟨_, h_anti⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
refine : (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)

Tactic:
refine ⟨?_, ⟨_, h_anti⟩⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
rw : ∀ x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ, x = 0
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤

Tactic:
rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]

Premises used: Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
x : E
hx : x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ 0

Tactic:
simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x

Premises used: norm_zero, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
x : E
hx : x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
x : E
hx : x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) = 0

Tactic:
have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
    (by positivity)
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
x : E
hx : x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ
this : HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) = 0
⊢ x = 0

Tactic:
aesop
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →L[ℂ] E'
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)

Tactic:
simp [← isPositive_toLinearMap_iff, LinearMap.isPositive_iff_complex]

Premises used: ContinuousLinearMap.isPositive_toLinearMap_iff, LinearMap.isPositive_iff_complex
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
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
x : E →L[𝕜] E
⊢ (x - x).IsPositive

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
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
x x_1 x_2 : E →L[𝕜] E
h₁ : (x_1 - x).IsPositive
h₂ : (x_2 - x_1).IsPositive
⊢ (x_2 - x).IsPositive

Tactic:
simpa using h₁.add h₂

Premises used: ContinuousLinearMap.IsPositive.add
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f g : E →L[𝕜] E
⊢ f ≤ g ↔ (g - f).IsPositive

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f g : E →L[𝕜] E
⊢ (↑f : E →ₗ[𝕜] E) ≤ (↑g : E →ₗ[𝕜] E) ↔ f ≤ g

Tactic:
isPositive_toLinearMap_iff (g - f)

Premises used: HSub.hSub, ContinuousLinearMap.isPositive_toLinearMap_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →L[𝕜] E
⊢ 0 ≤ f ↔ f.IsPositive

Tactic:
simpa using le_def 0 f

Premises used: ContinuousLinearMap.le_def, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
rw : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔ IsSelfAdjoint p
⊢ p.IsPositive ↔ IsSelfAdjoint p

Tactic:
rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap]

Premises used: ContinuousLinearMap.IsIdempotentElem.toLinearMap, ContinuousLinearMap.isPositive_toLinearMap_iff, LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔ IsSelfAdjoint p

Tactic:
isSelfAdjoint_iff_isSymmetric.symm

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔ IsSelfAdjoint p

Tactic:
exact isSelfAdjoint_iff_isSymmetric.symm

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsStarProjection p
⊢ p.IsPositive

Tactic:
hp.isIdempotentElem.isPositive_iff_isSelfAdjoint.mpr hp.isSelfAdjoint

Premises used: Iff.mpr, IsStarProjection.isIdempotentElem, ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint, IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsStarNormal p

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsSelfAdjoint p

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsStarNormal p ↔ IsSelfAdjoint p

Tactic:
2 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ IsStarNormal p ↔ IsSelfAdjoint p

Tactic:
tfae_have 2 ↔ 3 := hp.isSelfAdjoint_iff_isStarNormal.symm

Premises used: ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
⊢ IsSelfAdjoint p

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
⊢ p.IsPositive

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
⊢ IsSelfAdjoint p ↔ p.IsPositive

Tactic:
3 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
⊢ IsSelfAdjoint p ↔ p.IsPositive

Tactic:
tfae_have 3 ↔ 4 := hp.isPositive_iff_isSelfAdjoint.symm

Premises used: ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ IsSelfAdjoint p

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ (↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ IsSelfAdjoint p ↔ (↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ IsSelfAdjoint p ↔ (↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker

Tactic:
tfae_have 3 ↔ 1 := p.isSelfAdjoint_iff_isSymmetric.eq ▸
    (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp.toLinearMap)
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
tfae_3_iff_1 : IsSelfAdjoint p ↔ (↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker
⊢ [(↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
simp_rw : (↑U.starProjection : E →ₗ[𝕜] E) ≤ (↑V.starProjection : E →ₗ[𝕜] E) ↔ U ≤ V
simp_rw₁ : (↑U.starProjection : E →ₗ[𝕜] E).range ≤ (↑V.starProjection : E →ₗ[𝕜] E).range ↔ U ≤ V
simp_rw₂ : (U.projection Uᗮ ⋯).range ≤ (V.projection Vᗮ ⋯).range ↔ U ≤ V
⊢ U.starProjection ≤ V.starProjection ↔ U ≤ V

Tactic:
simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _
      |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _,
    toLinearMap_starProjection_eq_isComplProjection, range_projection]

Premises used: Submodule.toLinearMap_starProjection_eq_isComplProjection, Submodule.isSymmetricProjection_starProjection, Submodule.range_projection, ContinuousLinearMap.coe_le_coe_iff, LinearMap.IsSymmetricProjection.le_iff_range_le_range
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
⊢ U.starProjection = V.starProjection ↔ U = V

Tactic:
simp only [le_antisymm_iff, ← starProjection_le_starProjection_iff]

Premises used: le_antisymm_iff, Submodule.starProjection_le_starProjection_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
⊢ (↑T.symm : E →ₗ[𝕜] E).IsPositive

Tactic:
⟨hT.isSymmetric.toLinearMap_symm, fun x ↦ ?_⟩

Premises used: LinearMap.IsSymmetric.toLinearMap_symm, LinearMap.IsPositive, LinearMap.IsPositive.isSymmetric, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
⊢ (↑T.symm : E →ₗ[𝕜] E).IsPositive

Tactic:
refine ⟨hT.isSymmetric.toLinearMap_symm, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)

Tactic:
simpa using hT.2 (T.symm.toLinearMap x)

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, And.right, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)

Tactic:
have := by simpa using hT.2 (T.symm.toLinearMap x)
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)
rwa :
  ∀ (this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, ((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x⟫ : ℝ)),
    LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)),
    LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)

Tactic:
rwa [← T.symm.coe_toLinearMap, ← hT.isSymmetric.toLinearMap_symm] at this

Premises used: LinearEquiv.symm, LinearMap.IsSymmetric.toLinearMap_symm, LinearMap.IsPositive.isSymmetric, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
⊢ (↑T.symm : E →ₗ[𝕜] E).IsPositive ↔ (↑T : E →ₗ[𝕜] E).IsPositive

Tactic:
⟨.toLinearMap_symm, .toLinearMap_symm⟩

Premises used: Iff.intro, LinearMap.IsPositive.toLinearMap_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
simp_rw : True ∧ ∀ (x_1 : E), 0 ≤ HPow.hPow (β := ℕ) ‖⟪x, x_1⟫‖ 2
⊢ ContinuousLinearMap.IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E)
    ((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) x)

Tactic:
simp_rw [ContinuousLinearMap.isPositive_iff, isSymmetric_rankOne_self, rankOne_apply,
    inner_smul_left, RCLike.conj_mul, ← RCLike.ofReal_pow, RCLike.ofReal_nonneg]

Premises used: InnerProductSpace.rankOne_apply, RCLike.ofReal_nonneg, RCLike.conj_mul, RCLike.ofReal_pow, InnerProductSpace.isSymmetric_rankOne_self, ContinuousLinearMap.isPositive_iff, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ HPow.hPow (β := ℕ) ‖⟪x, x_1⟫‖ 2

Tactic:
simp